High-Assurance Post-Quantum Cryptography

Recent years have seen several landmark results in the formal verification of high-performance cryptographic libraries, leading to verified crypto code being adopted by mainstream projects like Chrome, Firefox, and Linux, including encryption algorithms and elliptic curves from the HACL* library. More recently, formally verified post-quantum cryptography developed by Cryspen within the libcrux library has been integrated into Firefox, OpenSSH, and Signal. Furthermore, as classical Diffie-Hellman based protocol frameworks like TLS and Signal begin to incorporate post-quantum cryptography, they require new formal analysis for both their design and implementation. In this talk, I will survey approaches towards the formal verification of production-ready cryptographic software by drawing from several successful projects and discussing their limitations. I will then describe my long-term vision of how formal verification of modern high-performance multi-platform libraries like OpenSSL can go hand-in-hand with open-source software development, and how this process can provide higher assurance as well as support the long-term maintainability of cryptographic software.