一句话：通过改造 CompCert 并增强中间语言语义，机器化证明其编译保持密码学常数时间，从而消除计时侧信道。
计时侧信道是密码实现的主要漏洞来源。密码学常数时间要求程序不执行依赖秘密的分支和内存访问。本文研究：现实编译器为常数时间源程序生成的代码是否可证明仍为常数时间？作者轻度修改 CompCert（经形式验证且适度优化的 C 编译器）以消除潜在泄漏，并插桩其中间语言操作语义来刻画密码学常数时间。随后证明修改后的 CompCert 保持常数时间，并通过新证明技术尽量复用原有正确性证明。结果表明，对轻度修改的 CompCert 可给出肯定答案，所提技术在通用性与证明可处理性间形成互补权衡，具有独立价值。
Timing side-channels are arguably one of the main sources of vulnerabilities in cryptographic implementations. One effective mitigation against timing side-channels is to write programs that do not perform secret-dependent branches and memory accesses. This mitigation, known as "cryptographic constant-time", is adopted by several popular cryptographic libraries. This paper focuses on compilation of cryptographic constant-time programs, and more specifically on the following question: is the code generated by a realistic compiler for a constant-time source program itself provably constant-time? Surprisingly, we answer the question positively for a mildly modified version of the CompCert compiler, a formally verified and moderately optimizing compiler for C. Concretely, we modify the CompCert compiler to eliminate sources of potential leakage. Then, we instrument the operational semantics of CompCert intermediate languages so as to be able to capture cryptographic constant-time. Finally, we prove that the modified CompCert compiler preserves constant-time. Our mechanization maximizes reuse of the CompCert correctness proof, through the use of new proof techniques for proving preservation of constant-time. These techniques achieve complementary trade-offs between generality and tractability of proof effort, and are of independent interest.
@article{paperbot515,
title = {Formal verification of a constant-time preserving C compiler},
author = {Gilles Barthe and Sandrine Blazy and Benjamin Grégoire and Rémi Hutin and Vincent Laporte and David Pichardie and Alix Trieu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371075}
}