Modern CPUs employ speculative execution to avoid expensive pipeline stalls by predicting the outcome of branching (and other) decisions and speculatively executing the corresponding instructions. Attackers can exploit speculative execution’s side effects to leak sensitive information and violate confidentiality. The family of Spectre attacks demonstrates that this vulnerability affects all modern general-purpose CPUs and poses a serious threat against platforms with multiple tenants.

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 talk, I will present a novel, principled approach for reasoning about software defenses against Spectre-style attacks. My approach builds on speculative non-interference, the first semantic notion of security against speculative execution attacks. I will also present Spectector, an algorithm based on symbolic execution for automatically proving speculative non-interference, or detecting violations. I will show how Spectector can be used to detect subtle leaks – and optimizations opportunities – in the way major compilers place Spectre countermeasures.