Exorcising Spectres with Secure Compilers

TL;DR

This paper develops a formal framework to analyze and verify the security of compiler-inserted countermeasures against Spectre attacks, providing the first proofs of their security and insecurity.

Contribution

It introduces a comprehensive framework for reasoning about the security guarantees of compiler-level Spectre countermeasures and performs the first formal security analysis of these measures.

Findings

Identifies which compiler countermeasures are secure against Spectre.

Provides formal proofs of security and insecurity for various countermeasures.

Establishes foundational criteria for secure compilation against speculative execution attacks.

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. 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.