15,000 lines of verified cryptography now in Python

Summary

In November 2022, I opened issue 99108 on Python’s GitHub repository, arguing that after a recent CVE in its implementation of SHA3, Python should embrace verified code for all of its hash-related infrastructure. As of last week, this issue is now closed, and every single hash and HMAC algorithm exposed by default in Python is now provided by HACL*, the verified cryptographic library. There was no loss of functionality, and the transition was entirely transparent for Python users. Python now vendors (includes in its repository) 15,000 lines of verified C code from HACL*. Pulling newer versions from the upstream HACL* repository is entirely automated and is done by invoking a script. HACL* was able to successfully implement new features to meet all of the requirements of Python, such as: additional modes for the Blake2 family of algorithms, a new API for SHA3 that covers all Keccak variants, strict abstraction patterns to deal with build system difficulties, proper error management (notably, allocation failures), and instantiating HACL’s generic “streaming” functionality with the HMAC algorithm, including an optimization that requires keeping two hash states at once. This is the culmination of 2.5 years of work, and could not have happened without the invaluable help of Aymeric Fromherz, who shouldered a lot of the implementation burden. Son Ho had a key contribution early on, generalizing HACL’s “streaming” functionality to be able to handle block algorithms that require a “pre-input”. This slightly obscure generalization was actually essential to implement a suitable, optimized HMAC that keeps two hash states under the hood. On the Python side, Gregory P. Smith, Bénédikt Tran, and later Chris Eibl were big champions and provided a lot of help. Finally, the HACS series of workshops created connections (hello, Paul Kehrer!) and provided sufficient momentum to make this happen. A warm thank you to both the Python and verified cryptographic communities! As I oftentimes...