Los ataques de ejecución especulativa, como Spectre, aprovechan las vulnerabilidades críticas de los procesadores modernos para filtrar información confidencial. Marco Guarnieri, José Francisco Morales y Andrés Sánchez, del Instituto IMDEA Software, Boris Köpf, de Microsoft Research, y Jan Reineke, de la Universidad del Sarre, han creado Spectector, una herramienta para demostrar la seguridad de los programas frente a estos ataques. La investigación ha sido apoyada por una subvención de Intel Strategic Research Alliance.
Spectector implementa el primer enfoque basado en principios para razonar las filtraciones de información explotadas por los ataques al estilo Spectre. La herramienta aprovecha la ejecución simbólica y la autocomposición para probar automáticamente que los programas satisfacen una propiedad llamada no interferencia especulativa, que garantiza la ausencia de fugas especulativas o detectar violaciones.
Usando Spectector, detectaron errores sutiles en la forma en que varios compiladores importantes colocan las contramedidas de Spectre, lo que puede dar lugar a programas inseguros o contramedidas innecesarias.
Una de las evidencias del éxito de la herramienta es que este mes el trabajo ha sido aceptado en el Simposio IEEE sobre Seguridad y Privacidad 2020.
