arXiv · 1812.08639
SPECTECTOR: Principled Detection of Speculative Information Flows
Abstract
Since the advent of SPECTRE, a number of countermeasures have been proposed and deployed. Rigorously reasoning about their effectiveness, however, requires a well-defined notion of security against speculative execution attacks, which has been missing until now. In this paper (1) we put forward speculative non-interference, the first semantic notion of security against speculative execution attacks, and (2) we develop SPECTECTOR, an algorithm based on symbolic execution to automatically prove speculative non-interference, 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.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke, Andrés Sánchez. 2019-07-24. SPECTECTOR: Principled Detection of Speculative Information Flows. https://arxiv.org/abs/1812.08639
Cite the original work for its findings. Save a collection to share your selection of sources.