Replace built-in hashlib with verified implementations from HACL* (original) (raw)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Appearance settings

Description

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.