Get the latest tech news
15,000 lines of verified cryptography now in Python
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.
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. The presence of option types in the source compiles to tagged unions in the generated C; this is a little verbose, and we may change our definition of a piece of state to feature a has_failed run-time function that can assess whether a memory allocation failed, at the expense of more complexity and verification effort. Later on, once it became clear that the upstream code was maintainable and pretty stable, that pile of seds was eliminated, on the basis that it’s not the end of the world if a header contains a few extra definitions, and it all makes maintenance easier.
Or read this on Hacker News