一句话：揭示主流编译器不保持推测性常量时间，并给出经 Coq 验证保持该性质的编译器原型与类型检查器修补方案。
编译器常削弱甚至丢弃软件层面的侧信道防护措施，还可能引入新的漏洞。已有工作证明（略作修改的）CompCert 与 Jasmin 形式验证编译器保持常量时间（constant-time），这是一种抵御时间侧信道攻击的信息流策略；但对于其强化版本——抵御 Spectre-v1 攻击的推测性常量时间（speculative constant-time）是否被保持，此前尚无结论。本文首先给出反例，说明实践中该性质并不被保持：一些安全的程序经 GCC -O0、GCC -O1 与 Jasmin 编译后不再满足推测性常量时间。随后，作者抽取 Jasmin 编译器的若干关键 pass，定义了一个概念验证编译器，并在 Coq 证明助手中机器化证明了该编译器保持推测性常量时间。最后，作者修补了 Jasmin 的推测性常量时间类型检查器，并表明所有用 Jasmin 编写的密码实现都能以极小改动完成修复。
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 problemis 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 policythat 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 C oq 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.
@article{OlmosBBGL24,
title = {Preservation of Speculative Constant-Time by Compilation},
author = {Santiago Arranz Olmos and Gilles Barthe and Lionel Blatter and Benjamin Grégoire and Vincent Laporte},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704880}
}