Preservation of Speculative Constant-Time by Compilation

作     者：Arranz Olmos, Santiago Barthe, Gilles Blatter, Lionel Grégoire, Benjamin Laporte, Vincent 

作者机构：MPI-SP Bochum Germany IMDEA Software Institute Madrid Spain Inria Sophia Antipolis France Université de Lorraine Nancy France Inria Nancy France 

出 版 物：《Proceedings of the ACM on Programming Languages》 (Proc. ACM Program. Lang.)

年 卷 期：2025年第9卷第POPL期

页      面：1293-1325页

核心收录：

基　　金：This research was supported by the Deutsche Forschungsgemeinschaft (DFG, German research Foundation) as part of the Excellence Strategy of the German Federal and State Governments EXC 2092 CASA - 390781972 and by the Agence Nationale de la Recherche (French National Research Agency) as part of the France 2030 programme ANR-22-PECY-0006 

主　　题：Program compilers 

摘      要：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. © 2025 Owner/Author.