Allen School Colloquia Series
Title: Proof-driven Development of Production-quality Cryptographic Software
Speaker: Andres Erbsen (MIT)
Date: Monday, March 4, 2024

Abstract: the internet relies heavily on cryptography, but implementing it properly and with negligible performance overhead is a challenging, tedious, and error-prone task even for top specialists. Formal verification holds great promise for ruling out known and unknown bugs and vulnerabilities, but common cryptographic optimizations make it challenging to apply directly. Fiat Cryptography reimagines cryptographic code using comprehensive computer-checked proofs, algorithm-level metaprogramming, and specializing compilation. For the first time, expert-level performance is achieved without platform-and-parameter-specific manual effort: directly for C code, and relying on randomized closed-loop optimization for assembly code. Verified code generated by Fiat Cryptography is now used in popular web browsers, mobile platforms, and cloud services. The same implementations and proofs integrate into a larger ecosystem of hardware and software components with an end-to-end theorem of functional correctness about a practical demo system. Scientific takeaways from this project include lessons about proof-assistant data structures, rewriting higher-order code, formalizing programming languages with unspecified behavior, and compiler-correctness proofs as well as a systematic, general, and precise presentation of algorithms behind record-setting cryptographic arithmetic implementations.

Bio: Andres received his PhD from MIT in 2023. His research interests lie at the intersection of formal verification, computer security, and computer systems. He prefers to seek principled long-term solutions to practically important problems by formalizing successful informal practices and domain-expert intuition. His work has led to some of the largest deployments of formally verified code and was recently recognized with the PLDI distinguished paper award.

This video is closed captioned.