3 papers
cs.PL2025
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…
cs.CR2023
CryptOpt: Automatic Optimization of Straightline Code
Joel Kuepper, Andres Erbsen, Jason Gross +9
Manual engineering of high-performance implementations typically consumes many resources and requires in-depth knowledge of the hardware. Compilers try to address these problems; h…
cs.CR2022
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version)
Joel Kuepper, Andres Erbsen, Jason Gross +9
Most software domains rely on compilers to translate high-level code to multiple different machine languages, with performance not too much worse than what developers would have th…