Speculative execution attacks, such as Spectre, exploit critical vulnerabilities in modern processors to leak sensitive information. Marco Guarnieri, José Francisco Morales and Andrés Sánchez, from the IMDEA Software Institute, Boris Köpf, from Microsoft Research, and Jan Reineke, from Saarland University, have created Spectector, a tool for proving programs secure against such attacks. The research has been supported by a grant from the Intel Strategic Research Alliance.
Spectector implements the first principled approach for reasoning about the information leaks exploited by Spectre-style attacks. Spectector leverages symbolic execution and self-composition to automatically prove that programs satisfy a property called speculative non-interference, which guarantees the absence of speculative leaks, or detect violations.
Using Spectector, they detected subtle bugs in the way Spectre-countermeasures are placed by several major compilers, which may result in insecure programs or unnecessary countermeasures.
One of the evidences of the tool’s success is that this month the paper has been accepted at the IEEE Symposium on Security and Privacy 2020.
