Exorcising Spectres with Secure Compilers


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. However, the security of these countermeasures has not been ascertained: while some of them are believed to be secure, others are known to be insecure and result in vulnerable programs. In this paper, we formally prove the security (or insecurity) of compiler-level countermeasures for Spectre. To prove security, we introduce a novel, general methodology built upon recent secure compilation theory. We use this theory to derive secure compilation criteria formalizing when a compiler produces secure code against Spectre attacks. With these criteria, we formally prove that some countermeasures, such as speculative load hardening (SLH), are vulnerable to Spectre attacks and others (like speculation-barriers-insertion and variations of SLH) are secure. 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.