Sites Inria

Version française

Rencontres Inria Industrie

Project team Prosecco (Inria Paris) -

HACL*: Verified Cryptography for Provably Secure Applications

© INRIA Sophie Auvin - P comme Protocole

HACL* is a new verified cryptographic library that implements popular modern cryptographic primitives. Using these primitives, HACL* implements the NaCl cryptographic API and can be used as a drop-in replacement for NaCl implementations like libsodium and TweetNaCl. The source code is C generated from F*. This implies that the verified primitives can be used as part as security critical applications and their security proofs.

Keywords: Cryptography Formal Methods Secure Applications High Assurance High Performance