POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
Fri 24 Jan 2025 17:00 - 17:20 at Marco Polo - Speculative Execution Chair(s): Viktor Vafeiadis

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. Our analysis highlights that fence-based and retpoline-based countermeasures can be securely lifted to the strongest speculative semantics under study. In contrast, countermeasures based on speculative load hardening cannot be securely lifted to semantics supporting indirect jump speculation.

Fri 24 Jan

Displayed time zone: Mountain Time (US & Canada) change

17:00 - 18:00
Speculative ExecutionPOPL at Marco Polo
Chair(s): Viktor Vafeiadis MPI-SWS
17:00
20m
Talk
Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
POPL
Xaver Fabian CISPA, Marco Patrignani University of Trento, Marco Guarnieri IMDEA Software Institute, Michael Backes Cispa Helmholtz Center for Information Security
Link to publication
17:20
20m
Talk
Preservation of speculative constant-time by compilation
POPL
Santiago Arranz Olmos Max Planck Institute for Security and Privacy, Gilles Barthe MPI-SP; IMDEA Software Institute, Lionel Blatter Max Planck Institute for Security and Privacy, Benjamin Gregoire INRIA, Vincent Laporte Inria
17:40
20m
Talk
SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
POPL
Sören van der Wall TU Braunschweig, Roland Meyer TU Braunschweig
Link to publication DOI