SPECTECTOR: Principled Detection of Speculative Information Flows
This addresses the need for principled security verification in computer systems, particularly for compilers and hardware, though it is incremental as it builds on existing symbolic execution methods.
The paper tackles the problem of rigorously reasoning about security against speculative execution attacks like SPECTRE by proposing speculative non-interference, the first semantic notion of security, and develops SPECTECTOR, an algorithm to automatically prove or detect violations, which detected subtle leaks and optimization opportunities in major compilers' countermeasures.
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.