Preservation of speculative constant-time by compilation
This program is tentative and subject to change.
Compilers often weaken or even discard software-based countermeasures commonly used to protect programs against side-channel attacks; worse, they may also introduce vulnerabilities that attackers can exploit. The solution to this problem is to develop compilers that preserve such countermeasures. Prior work establishes that (a mildly modified version of) the CompCert and Jasmin formally verified compilers preserve constant-time, an information flow policy that ensures that programs are protected against timing side-channel attacks. However, nothing is known about preservation of speculative constant-time, a strengthening of the constant-time policy that ensures that programs are protected against Spectre v1 attacks. We first show that preservation of speculative constant-time fails in practice by providing examples of secure programs whose compilation is not speculative constant-time using GCC (GCC -O0
and GCC -O1
) and Jasmin. Then, we define a proof-of-concept compiler that distills some of the critical passes of the Jasmin compiler and use the Coq proof assistant to prove that it preserves speculative constant-time. Finally, we patch the Jasmin speculative constant-time type checker and demonstrate that all cryptographic implementations written in Jasmin can be fixed with minimal impact.
This program is tentative and subject to change.
Fri 24 JanDisplayed time zone: Mountain Time (US & Canada) change
17:00 - 18:00 | |||
17:00 20mTalk | 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 | ||
17:20 20mTalk | 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 20mTalk | SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations POPL |