Spectector: Principled Detection of Speculative Information Flows - Guarnieri, Marco; Köpf, Boris; Morales, Jose F.; Reineke, Jan; Sanchez, Andres (IEEE Symposium on Security and Privacy, 2020)
Since the advent of SPECTRE, a number of countermeasures have been proposed and deployed. Rigorously reasoning about their effectiveness, however, requires a well-deﬁned notion of security against speculative execution attacks, which has been missing until now. In this paper (1) we put forward speculative non-interference, the ﬁrst semantic notion of security against speculative execution attacks, and (2) we develop SPECTECTOR, an algorithm based on symbolic execution to automatically prove speculative noninterference, or to detect violations. We implement SPECTECTOR in a tool, which we use to detect subtle leaks and optimizations opportunities in the way major compilers place SPECTRE countermeasures. A scalability analysis indicates that checking speculative non-interference does not exhibit fundamental bottlenecks beyond those inherited by symbolic execution.