Karthik Bhargavan (Prosecco) : Verified Cryptography for Everyone
Understanding and implementing cryptographic algorithms is hard, and even expert programmers often make mistakes.
For example, OpenSSL issued 11 CVEs last year for bugs in its core cryptographic library, including 6 memory safety errors, 3 timing side-channel leaks, and 2 incorrect numerical computations. In this talk, I will describe HACL*, a new verified portable cryptographic library that implements a suite of modern cryptographic primitives.
HACL* is written and verified in the F* programming language, developed by Microsoft Research and INRIA.
After verification, the F* program is compiled to standalone C code that can be included in any software project. Verified code from HACL* has been integrated into Firefox 57, and is already being used on millions of HTTPS connections.
I will describe our verification toolchain and discuss the challenges we needed to overcome in going from research software to production-ready high-performance code that can be integrated into a mainstream web browser.