Search code, repositories, users, issues, pull requests...
This repository contains verified code for a library of modern cryptographic algorithms, including Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC, and HKDF. This set of algorithms is enough to support the full NaCl API and several TLS 1.3 ciphersuites. The code for all of these algorithms is formally verified using the F* verification framework for memory safety, functional correctness, and secret independence (resistance to some types of timing side-channels).
Warning: This is the research home of HACL*. If you are looking for documentation, releases, language bindings and code that can be satisfactorily integrated into a production project, please check out HACL packages.
HACL* is a formally verified library of modern cryptographic algorithms written in a subset of F* called Low* and compiled to C using a compiler called KaRaMeL. The Low* source code for each primitive is verified for memory safety, functional correctness, and secret independence. The compiler generates efficient, readable, standalone C code for each algorithm that can be easily integrated into any C project. We include the current C code for various HACL* algorithms in the dist directory. HACL* can also be compiled to WebAssembly.
ValeCrypt provides formally verified high-performance cryptographic code for selected primitives in assembly language. It relies on the Vale tool to produce code and proofs in F*. Vale supports multiple platforms and proves that its implementations are memory safe, functionally correct, and that timing and memory accesses are secret independent.
