Skip to content

Exorcising Spectres with Secure Compilers

[Submitted on 18 Oct 2019 (v1), last revised 10 Sep 2021 (this version, v4)]

Authors: Marco Patrignani, Marco Guarnieri

Subjects: Programming Languages (cs.PL)


Attackers can access sensitive information of programs by exploiting the side-effects of speculatively-executed instructions using Spectre attacks. To mitigate theses attacks, popular compilers deployed a wide range of countermeasures. The security of these countermeasures, however, has not been ascertained: while some of them are believed to be secure, others are known to be insecure and result in vulnerable programs. To reason about the security guarantees of these compiler-inserted countermeasures, this paper presents a framework comprising several secure compilation criteria characterizing when compilers produce code resistant against Spectre attacks. With this framework, we perform a comprehensive security analysis of compiler-level countermeasures against Spectre attacks implemented in major compilers. This work provides sound foundations to formally reason about the security of compiler-level countermeasures against Spectre attacks as well as the first proofs of security and insecurity of said countermeasures.

Spectre attack:

Meltdown and Spectre:


PDF: Exorcising Spectres with Secure Compilers.pdf