Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks

TL;DR

This paper introduces a new secure compilation framework that enhances Spectre attack countermeasures in compilers by lifting security guarantees from weaker to stronger speculative semantics, enabling comprehensive security analysis.

Contribution

The paper presents a novel framework for lifting security guarantees across different speculative semantics, facilitating thorough Spectre countermeasure analysis without new proofs.

Findings

Analyzed 9 countermeasures against 5 Spectre attack classes

Proved security of countermeasures against five speculation mechanisms

Performed the most comprehensive Spectre security analysis to date

Abstract

Mainstream compilers implement different countermeasures to prevent specific classes of speculative execution attacks. Unfortunately, these countermeasures either lack formal guarantees or come with proofs restricted to speculative semantics capturing only a subset of the speculation mechanisms supported by modern CPUs, thereby limiting their practical applicability. Ideally, these security proofs should target a speculative semantics capturing the effects of all speculation mechanisms implemented in modern CPUs. However, this is impractical and requires new secure compilation proofs to support additional speculation mechanisms. In this paper, we address this problem by proposing a novel secure compilation framework that allows lifting the security guarantees provided by Spectre countermeasures from weaker speculative semantics (ignoring some speculation mechanisms) to stronger ones (accounting for the omitted mechanisms) without requiring new secure compilation proofs. Using our lifting framework, we performed the most comprehensive security analysis of Spectre countermeasures implemented in mainstream compilers to date. Our analysis spans 9 different countermeasures against 5 classes of Spectre attacks, which we proved secure against a speculative semantics accounting for five different speculation mechanisms.