CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives

Explore a groundbreaking 19-minute conference talk from PLDI 2023 that introduces CryptOpt, a novel compilation pipeline for cryptographic primitives. Discover how this innovative approach combines randomized program search and formal verification to generate assembly code that outperforms GCC and Clang compilations. Learn about the integration with the Fiat Cryptography framework and the development of a formally verified program-equivalence checker. Examine the practical applications of CryptOpt, including its success in producing the fastest-known implementations of finite-field arithmetic for Curve25519 and the Bitcoin elliptic curve secp256k1 on Intel's 12th and 13th generation processors. Gain insights into the challenges of optimizing cryptographic code and the potential for automated techniques to revolutionize the field.