Python developers have recently announced the successful completion of an initiative aimed at replacing the cryptographic algorithms implementation in the hashlib and hmac models with options backed by mathematical evidence of reliability provided by the project “hacl*”. This transition began in 2022 after the discovery of a buffer overflow in the implementation of the SHA3 algorithm used in the Hashlib Python Module.
The main repository of the SPYTHON project has now integrated new implementations of cryptographic hash functions and algorithms, such as hmac (a mechanism for message authenticity verification), replacing all default hash functions and HMAC with verified alternatives. The updated code includes the implementation of HMAC-Blake2, utilizing AVX2 SIMD instructions for faster computations. The verified code is expected to be included in the upcoming Python 3.14 release.
The new cryptographic functions implementations are sourced from the library “hacl*”, developed by researchers from the French State Institute of Research in Informatics and Automation (Inria), Microsoft Research, and Carnegie Mellon University. The HaCl* library supports standard cryptographic functions required for TLS 1.3 and offers full support for the API nacl (Networking and Cryptography Library), including algorithms like Curve25519, ED25519, AES-GCM, Chacha20, Poly1305, Sha-2, SHA-3, HMAC, and HKDF. In terms of performance, the HaCl* library is comparable to Openssl but offers additional reliability and security guarantees.
The HaCl* code is written in the functional language F*, which provides a system of dependent types and specifications to ensure accurate mathematical models and error-free implementations using SMT formulas and proof assistant tools. The reference code in F* is translated into SI language code using the Karamel compiler.