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

Explore a 19-minute conference talk from POPL 2025 that presents a novel secure compilation framework for strengthening compiler security guarantees against Spectre attacks. Learn how researchers Xaver Fabian, Marco Patrignani, Marco Guarnieri, and Michael Backes developed a method to lift security guarantees from weaker speculative semantics to stronger ones without requiring new secure compilation proofs. The presentation details their comprehensive security analysis of nine different countermeasures against five classes of Spectre attacks, tested against a speculative semantics accounting for five different speculation mechanisms. Discover which countermeasures can be securely lifted to the strongest speculative semantics and which ones fail when supporting indirect jump speculation. This research represents the most thorough security analysis of Spectre countermeasures implemented in mainstream compilers to date.