It has been announced that the initiative to replace the implementations of cryptographic algorithms offered in the hashlib and hmac modules in Python with mathematically proven reliable variants prepared by the 'HACL*' project has been successfully completed. Work on transitioning to functions with mathematically proven reliability has been underway since 2022 and was initiated after a buffer overflow was discovered in the implementation of the SHA3 algorithm used in the Python hashlib module.
The main repository of the CPython project has accepted code with new implementations of cryptographic hash functions and HMAC (hash-based message authentication code) algorithms. All hash functions and HMACs provided by default in Python have been replaced with verified variants. Among other things, an HMAC-BLAKE2 implementation has been added that utilizes AVX2 SIMD instructions to accelerate computations. It is expected that the verified code will be included in the upcoming release of Python 3.14 in the fall.
New implementations of cryptographic functions have been migrated from the HACL* library, developed by researchers from the French National Institute for Research in Computer Science and Automation (INRIA), Microsoft Research, and Carnegie Mellon University. The HACL* library supports standard cryptographic functions sufficient for working with TLS 1.3 and full support of the NaCl API (Networking and Cryptography library), such as 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 unlike the latter, it provides additional reliability and security guarantees.
The HACL* code is written in a subset of the functional programming language F*, which offers a system of dependent types and refinements that allow for precise specifications (mathematical models) and guarantees the absence of errors in the implementation through SMT formulas and auxiliary proof tools. The reference code in F* is translated into C code using the KaRaMeL compiler and is available for integration with other projects.
Verification involves determining detailed specifications that describe all possible behaviors of the program and forming a mathematical proof that the written code fully complies with the prepared specifications. Verification guarantees that the program will execute only as the developers intended and that it is free from certain classes of errors, such as buffer overflows, pointer dereferencing, access to already freed memory areas, or double freeing of memory blocks. During compilation, strict type and value checking is enforced—one component will never pass parameters that do not conform to the specifications to another component, nor will it access the internal states of other components.
The process of transitioning to verified code took two and a half years and required further development of the HACL* library, which was extended with capabilities necessary for the transparent replacement of the existing functionality of hashlib. For instance, HACL* added support for HMAC streaming mode, provided additional operational modes for the Blake2 algorithms, implemented a new API for SHA3 covering all variants of the Keccak family of algorithms, ensured necessary error notification mechanisms (e.g., for memory allocation issues), and developed scripts for automating the migration of new versions of HACL* into the Python repository.
Source: opennet.ru
