✳flâneur — a map of the web's best reading

Preservation of Speculative Constant-Time by Compilation

eprint.iacr.org · 378 words · saved by 1 readers

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 s

Preservation of Speculative Constant-Time by Compilation Paper 2024/1203 Preservation of Speculative Constant-Time by Compilation Santiago Arranz Olmos , Max Planck Institute for Security and Privacy Gilles Barthe , Max Planck Institute for Security and Privacy , IMDEA Software Lionel Blatter , Max Planck Institute for Security and Privacy Benjamin Grégoire , Research Centre Inria Sophia Antipolis Vincent Laporte , Centre Inria de l'Université de Lorraine Abstract Compilers often weaken or even discard software-based countermeasures commonly used to protect programs against side-channel attack

Explore this link on the map →

related reading