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攻击来利用投机性执行指令的副作用获取程序敏感信息。为了减轻这些攻击,大众汇编者采取了一系列广泛的反措施。然而,这些反措施的安全性还没有得到确定:虽然有人认为其中一些措施是安全的,但另一些措施被认为是不安全的,并导致脆弱的方案。为了说明这些编译者加入的反措施的安全保障,本文件提出了一个框架,其中包括若干安全编集标准,在编译者产生抵抗Spectre攻击的编码时,这些编码具有特征。在这个框架内,我们对主要编译者针对Spectre攻击执行的编译者级反措施进行全面的安全性分析。这项工作为正式说明对Spectre攻击的编译者一级反措施的安全性以及上述反措施的安全和不安全性初步证据提供了坚实的基础。