# SPECTECTOR: Principled Detection of Speculative Information Flows

## TL;DR

This paper introduces a formal security notion called speculative non-interference and presents SPECTECTOR, a symbolic execution tool that automatically verifies security against speculative execution attacks and identifies potential leaks.

## Contribution

It defines the first semantic security model for speculative execution attacks and provides an automated tool to verify and analyze countermeasures in real-world code.

## Key findings

- SPECTECTOR effectively detects subtle speculative leaks.
- The tool uncovers optimization opportunities in compiler countermeasures.
- Checking speculative non-interference scales reasonably with program complexity.

## 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.