CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives
CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives
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 the patience to write directly in assembly language. However, cryptography has been an exception, where many performance-critical routines have been written directly in assembly (sometimes through metaprogramming layers). Some past work has shown how to do formal verification of that assembly, and other work has shown how to generate C code automatically along with formal proof, but with consequent performance penalties vs. the best-known assembly.
We present CryptOpt, the first compilation pipeline that specializes high-level cryptographic functional programs into assembly code significantly faster than what GCC or Clang produce, with mechanized proof (in Coq) whose final theorem statement mentions little beyond the input functional program and the operational semantics of x86-64 assembly. On the optimization side, we apply randomized search through the space of assembly programs, with repeated automatic benchmarking on target CPUs. On the formal-verification side, we connect to the Fiat Cryptography framework (which translates functional programs into C-like IR code) and extend it with a new formally verified program-equivalence checker, incorporating a modest subset of known features of SMT solvers and symbolic-execution engines. The overall prototype is quite practical, e.g. producing new fastest-known implementations for the relatively new Intel i9 12G, of finite-field arithmetic for both Curve25519 (part of the TLS standard) and the Bitcoin elliptic curve secp256k1.
About the speaker
PhD Student, University of Adelaide
Joel Kuepper studied Applied Computer Science in Germany with Hewlett-Packard from 2013--2019. He came into Australia at the start of 2020 to commence his PhD with focus on automatically optimising the performance of cryptographic implementations at the University of Adelaide. So far, his tool 'CryptOpt' can generate provable correct, side-channel secure implementations for ECC primitives which outperform off-the-shelf compilers significantly, and are on par with hand-written assembly code.
Monash University values the privacy of every individual's personal information and is committed to the protection of that information from unauthorised use and disclosure except where permitted by law. For information about the handling of your personal information please see Data Protection and Privacy Procedure and the relevant Data Protection and Privacy Collection Statement that applies to you depending on the nature of your interaction with us.
If you have any questions about how Monash University is collecting and handling your personal information, please contact our Data Protection and Privacy Office at dataprotectionofficer@monash.edu.