Reasoning about speculative execution attacks

Speculative execution attacks, like the recent SPECTRE attacks, exploit the persistent micro-architectural side effects of speculatively executed instructions. These attacks affect all modern general-purpose CPUs and pose a serious threat against platforms with multiple tenants. However, we still lack a precise characterization of security against speculative execution attacks. Such a characterization is a prerequisite for reasoning about the effectiveness of countermeasures and for making principled decisions about their placement.


This project’s goals are (1) building the theoretical foundations for reasoning about speculative execution attacks, (2) developing techniques for detecting speculative leaks (or prove their absence), and (3) analyzing the security of SPECTRE’s countermeasures implemented in state-of-the-art compilers.

Marco Guarnieri
Assistant professor


. SPECTECTOR: Principled detection of speculative information flows. In S&P, 2020.

PDF Code Project Extended version (arXiv)