Spectector

Automatic detection of speculative information flows



What is it?

Spectector analyzes x64 assembly programs, and it either automatically detects information leaks introduced by speculatively executed instructions or proves the program leak-free.

In a nutshell, Spectector symbolically executes the program under analysis with respect to a semantics that accounts for the speculative execution’s effects. During the symbolic execution, Spectector derives SMT formulae characterizing leaks caused by speculatively executed instructions. It then relies on the Z3 SMT solver to determine the presence of possible leaks.

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.


Downloads

  • 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 .
    Here, we describe how one can reproduce the experimental results from the Spectector’s paper.


Publications

  • Spectector: Principled Detection of Speculative Information Flows
    Marco Guarnieri, Boris Koepf, José Francisco Morales, Jan Reineke, Andrés Sánchez
    Paper

Team

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