# SPECTECTOR: Principled Detection of Speculative Information Flows

arXiv: https://arxiv.org/abs/1812.08639 · HTML: https://mlsanity.com/paper/1812.08639/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Dec 2018.

## Built on by (most cited first, 2 of 2)

- [ZeroLeak: Using LLMs for Scalable and Cost Effective Side-Channel Patching](https://mlsanity.com/paper/2308.13062/) (2023)
- [Short Paper: Static and Microarchitectural ML-Based Approaches For Detecting Spectre Vulnerabilities and Attacks](https://mlsanity.com/paper/2210.14452/) (2022)

## Abstract (arXiv)

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.