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.
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.