Contract-aware Secure Compilation

Abstract

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 whose security, however, has not been ascertained. While some 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 countermeasures, this paper presents a framework comprising secure compilation criteria characterizing when compilers produce code resistant against Spectre attacks. With this framework, we perform a comprehensive security analysis of compiler countermeasures against Spectre attacks implemented in major compilers. This work provides sound foundations to formally reason about the security of compiler countermeasures against Spectre attacks as well as the first proofs of security and insecurity of said countermeasures.