2025-10-09 –, Prague/ Technical Deep Dive & Innovation
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.
The proposed talk draws from several research papers by the speaker and his co-authors. The most relevant works (in reverse chronolical order) that we will draw from in this talk are as follows:
* Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust. https://eprint.iacr.org/2025/980
* hax: Verifying Security-Critical Rust Software using Multiple Provers. VSTTE 2024. https://eprint.iacr.org/2025/142
* KyberSlash: Exploiting secret-dependent division timings in Kyber implementations. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2025(2): 209-234 (2025). https://eprint.iacr.org/2024/1049
* Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging. USENIX Security Symposium 2024. https://eprint.iacr.org/2024/702
* EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. IEEE S&P 2020: 983-1002, https://eprint.iacr.org/2019/757
* Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. IEEE Symposium on Security and Privacy 2017: 483-502. https://inria.hal.science/hal-01575920/document
Bhargavan is a research scientist and co-founder of Cryspen, a company that works on high-assurance security-critical software. He is on leave from Inria, where he led a team of researchers working on formal verification and applied cryptography. Bhargavan has been involved in the design and analysis of IETF standards like TLS 1.3, HPKE, and MLS, and he and his colleagues build and maintain formally verified cryptographic libraries like HACL* and libcrux.