Karthikeyan Bhargavan
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.
Session
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.