Reasoning about speculative execution attacks

Speculative execution attacks, like the recent SPECTRE attacks, exploit the persistent microarchitectural 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 and security of countermeasures.


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 (hardware and software) SPECTRE’s countermeasures.

Marco Guarnieri
Assistant professor


. Hardware-Software Contracts for Secure Speculation. In S&P, 2021.

PDF Code Project Video Extended version (arXiv)

. Exorcising Spectres with Secure Compilers. Technical report, 2020.

PDF Project Extended version (arXiv)

. Flushgeist: Cache Leaks from Beyond the Flush. Technical report, 2020.

PDF Project Extended version (arXiv)