Spectector is a tool for automatically detecting leaks caused by speculatively executed instructions in x64 assembly programs.
In a nutshell, Spectector symbolically executes the program under analysis with respect to a semantics that captures the effects of speculatively executed instructions. During the symbolic execution, Spectector derives SMT formulae characterizing leaks caused by speculatively executed instructions, and it relies on the Z3 SMT solver to determine the presence of possible leaks or prove their absence.
Using Spectector, we detected subtle bugs in the way Spectre-countermeasures are placed by several major compilers, which may result in insecure programs or unnecessary countermeasures.
The source code of Spectector is available on Github at the following repository
.
See the README for more information on installing and using Spectector.
The benchmarks used in the Spectector’s paper are available at the following repository
.
See the README for more information on how to reproduce the experimental results from the Spectector’s paper.
Hardware/software contracts for secure speculation
Marco Guarnieri, Boris Koepf, Jan Reineke, Pepe Vila
In: Proceedings of the 42nd IEEE Symposium on Security & Privacy, May 2021
Paper
Extended version (arXiv)
Talk
Spectector: Principled Detection of Speculative Information Flows
Marco Guarnieri, Boris Koepf, José Francisco Morales, Jan Reineke, Andrés Sánchez
In: Proceedings of the 41st IEEE Symposium on Security & Privacy, May 2020
Paper
Extended version (arXiv)
Preview video
Talk
Slides
| Marco Guarnieri IMDEA Software Institute | Boris Koepf Microsoft Research Cambridge | José F. Morales IMDEA Software Institute | |||
| Jan Reineke Saarland University | Andrés Sánchez IMDEA Software Institute | ||||