A CompCert Compiler that Preserves Cryptographic Constant-time
summary
CompCert gains a verified, branch-free selection primitive that preserves cryptographic constant-time: a new select operation with formal semantics is added to the intermediate languages, mapped to x86 CMOV (and similar target ops) by modifying two backend passes, with the transformation and correctness proofs mechanized in the CompCert Coq development. Edge cases like unsigned-to-float conversions and undefined re-evaluation of both branches are handled by arithmetic rewrites (using 0 and -C) so compiled code remains constant-time.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:54Background
- 1:39Cryptography
- 2:18Programming Policy
- 4:38Second Example
- 5:04Department Concert
- 5:45Confirmed
- 6:35Outline
- 7:04Overview
- 8:08Operation
- 13:01Optimization
- 15:01New Selection
- 16:08Solution
related talks
15mMy Journey in Secure Compilation
32mVerifying Constant-Time Implementations
29mA CompCert backend with symbolic encryption
18mPreservation of Speculative Constant-time by Compilation
58mFast Cryptographic Code via Partial Evaluation
23mSmooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs(…)
28mMemory simulations, security and optimization in a verified compiler
18mPreservation of speculative constant-time by compilation