A High Assurance Cryptographic Library — HACL* and EverCrypt Manual documentation (original) (raw)
HACL* is a formally verified cryptographic library written in F* and compiled to C, developed as a collaboration between the Prosecco team at INRIA Paris, Microsoft Research, andCarnegie Mellon University. The library, its applications, and the verification tools it relies on are being actively developed and maintained as part of Project Everest.
EverCrypt is a cryptographic provider that into a single library combines HACL*, described above, and ValeCrypt, a collection of verified assembly code for cryptographic primitives. This manual describes the HACL* and EverCrypt APIs. ReadHACL*, Vale, and EverCrypt for a detailed description of how they relate to each other.
HACL* is an open source project hosted at hacl-star, along with ValeCryptand EverCrypt. HACL*, Vale and EverCrypt are distributed together as a collection of C and assembly files. These can be used either as individual components, or as a full-fledged library through the EverCrypt provider.
Code from HACL*, ValeCrypt and EverCrypt is deployed in several production systems, including Mozilla Firefox's NSS, the Linux kernel, mbedTLS, the Tezos blockchain, the ElectionGuard Electronic Voting SDK, and theWireguard VPN. Still, HACL*, Vale, and EverCrypt remain ongoing research projects and should be treated as such. If you want to integrate this code into a production environment, or if you have any questions, comments, or feature requests for HACL*, Vale, or EverCrypt, initiate a conversation with the HACL* maintainers
Contents: