IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2019 > Principled detection of speculative information flows

Marco Guarnieri

Wednesday, April 24, 2019

10:45am Meeting room 302 (Mountain View), level 3

Marco Guarnieri, Post-doctoral Researcher, IMDEA Software Institute

Principled detection of speculative information flows


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.