Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
Owen Conoly, Andres Erbsen, Adam Chlipala
TL;DR
This paper addresses cryptographic constant-time verification for nondeterministic programs and compilers by developing an omnisemantics framework in which a program’s leakage trace is a function of its public inputs. It introduces multiple CT specification approaches—determinization via an oracle, postcondition-based oracle semantics, and predictor-based methods—and proves their equivalence and applicability to Bedrock2→RISC-V compilation. The work provides formal definitions for leakage-transformation and oracle/predictor transformation in compiler proofs, and demonstrates end-to-end CT-preserving compilation with case studies (e.g., login, stack operations, semiprime generation) proven in Coq. The result is a modular, mechanized foundation for timing-side-channel security in verified cryptographic software, enabling robust reasoning about nondeterminism at both source and machine-code levels.
Abstract
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.