Feature or enhancement

We propose to replace the non-OpenSSL cryptographic primitives in hashlib with high-assurance, verified versions from the HACL* project.

Pitch

As evidenced by the recent SHA3 buffer overflow, cryptographic primitives are tricky to implement correctly. There might be issues with memory management, exceeding lengths, incorrect buffer management, or worse, incorrect implementations in corner cases.

The HACL* project https://github.com/hacl-star/hacl-star provides verified implementations of cryptographic primitives. These implementations are mathematically shown to be:

• memory safe (no buffer overflows, no use-after-free)
• functionally correct (they always compute the right result)
• side-channel resistant (the most egregious variants of side-channels, such as memory and timing leaks, are ruled out by construction).

See https://hacl-star.github.io/Overview.html#what-is-verified-software for a longer description of how formal methods can help write high-assurance software and rule out entire classes of bugs.

The performance of HACL* is competitive with, and sometimes exceeds, that of OpenSSL. HACL* is distributed as pure C, and therefore is portable. Parts of HACL* have been adopted in Mozilla, Linux, the Tezos blockchain, and many more, thereby demonstrating that formally verified code is ready for production-time.

Previous discussion

Tagging @alex with whom I've informally discussed this.

• PR: gh-99108: Import SHA2-224 and SHA2-256 from HACL* #99109

• PR: gh-99108: Import SHA2-384/512 from HACL* #101707

• PR: gh-99108: Build the hashlib HACL* code as a static library. (fix wasm builds) #101917

• PR: gh-99108: Refactor _sha256 & _sha512 into _sha2. #101924

• PR: gh-99108: Import MD5 and SHA1 from HACL* #102089

• PR: gh-99108: Followup fix for Modules/Setup #102183

• PR: gh-99108: Add missing md5/sha1 defines to Modules/Setup #102308

• PR: gh-99108: Initial import of HACL-SHA3 into Python #103597

• PR: gh-99108: fix typo in Modules/Setup #104293

• PR: gh-99108: Refresh HACL* from upstream #104401

• PR: gh-99108: Release the GIL around hashlib built-in computation #104675

• PR: [3.12] gh-99108: Release the GIL around hashlib built-in computation (GH-104675) #104776

• PR: gh-99108: Refresh HACL* #104808

• PR: [3.12] gh-99108: Refresh HACL* (GH-104808) #104893

• PR: gh-99108: Mention HACL\* in the hashlib docs. #105634

• PR: [3.12] gh-99108: Mention HACL\* in the hashlib docs. (GH-105634) #105635

• PR: gh-99108: Refresh HACL*; update modules accordingly; fix namespacing #117237

• PR: [3.12] gh-99108: Refresh HACL*; update modules accordingly; fix namespacing (GH-117237) #117243

• PR: gh-99108: Update and check HACL* version information #117295

• PR: [3.12] gh-99108: Update and check HACL* version information (GH-117295) #117302

• PR: gh-99108: Add HACL* Blake2 implementation to hashlib #119316

• PR: gh-99108: Inform HACL when explicit_bzero is unavailable #123027

• PR: GH-99108: Fix Setup in addition to Setup.stdlib.in #123146

• PR: gh-99108: Disable HACL SIMD code on older versions of Android #124304

• PR: GH-99108: Make vectorized versions of Blake2 available on x86, too #125244

• PR: gh-99108: Cleanup references to inexisting Modules/_blake2. #126270

• PR: gh-99108: add HACL*-based 1-shot HMAC implementation  #126359

• PR: gh-99108: Implement HACL* HMAC #130157

• PR: gh-99108: add support for SIMD-accelerated HMAC-BLAKE2 #132120