Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers

Owen Conoly, Andres Erbsen, Adam Chlipala

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 l…