Proof-driven Development of Production-quality Cryptographic Software

Explore the cutting-edge approach to developing secure and efficient cryptographic software in this 57-minute talk by Andres Erbsen from MIT. Delve into the world of Fiat Cryptography, a revolutionary method that combines comprehensive computer-checked proofs, algorithm-level metaprogramming, and specializing compilation to achieve expert-level performance without platform-specific manual effort. Learn how this innovative approach has led to the deployment of verified code in popular web browsers, mobile platforms, and cloud services. Discover the scientific takeaways from this project, including insights on proof-assistant data structures, rewriting higher-order code, formalizing programming languages with unspecified behavior, and compiler-correctness proofs. Gain a deeper understanding of the systematic, general, and precise presentation of algorithms behind record-setting cryptographic arithmetic implementations. Understand the potential of formal verification in ruling out known and unknown bugs and vulnerabilities in cryptographic implementations, and how it addresses the challenges of implementing cryptography properly with negligible performance overhead.