一句话：首次用omnisemantics形式化非确定性程序的常量时间规范，并在Coq中端到端验证密码编译。
形式验证已排除大量安全缺陷，但无意信息泄漏较少受关注。形式规格常故意不指定部分系统行为以容许实现变更，但这些选择不应依赖机密信息。本文用 omnisemantics 与单副本断言形式化该概念，首次给出非确定性程序为常量时间、或更一般地不泄漏（部分）输入的定义。作者据此证明从 Bedrock2 C 编译到 RISC-V 的密码例程无数据泄漏，表明 omnisemantics 的平滑非确定性证明体验可扩展至常量时间性质。文中还分析程序-编译器契约的变体，揭示简化的陷阱；所有结果在 Coq 中整合为端到端定理。
Formal verification of software and compilers has been used to rule out large classes of security-critical issues, but risk of unintentional information leakage has received much less consideration. It is a key requirement for formal specifications to leave some details of a system’s behavior unspecified so that future implementation changes can be accommodated, and yet it is nonetheless expected that these choices would not be made based on confidential information the system handles. This paper formalizes that notion using omnisemantics and plain single-copy assertions, giving for the first time a specification of what it means for a nondeterministic program to be constant-time or more generally to avoid leaking (a part of) its inputs. We use this theory to prove data-leak-free execution of core cryptographic routines compiled from Bedrock2 C to RISC-V machine code, showing that the smooth specification and proof experience omnisemantics provides for nondeterminism extends to constant-time properties in the same setting. We also study variants of the key program-compiler contract, highlighting pitfalls of tempting simplifications and subtle consequences of how inputs to nondeterministic choices are constrained. Our results are backed by modular program-logic and compiler-correctness theorems, and they integrate into a neat end-to-end theorem in the Coq proof assistant.
@article{paperbot3082,
title = {Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers},
author = {Owen Conoly and Andres Erbsen and Adam Chlipala},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729318}
}