Security/CryptoEngineering/HACL*

HACL* is a formally verified cryptographic library in F*, developed by the Prosecco team in INRIA Paris in collaboration with Microsoft Research, as part of Project Everest.

The NSS team is working with INRIA to integrate verified algorithms from HACL* into NSS.

HACL* in NSS Releases

• NSS 3.33 is the first release containing verified cryptographic primitives from HACL*. The 64-bit Curve25519 implementation.
• NSS 3.35 contains the ChaCha20 (not vectorised) and Poly1305 (64-bit) HACL* implementation.
• NSS 3.36 contains the vectorised ChaCha20 HACL* implementation for SSSE3 and ARM NEON.
• NSS 3.37 contains the Poly1305 (32-bit) HACL* implementation

Tracked Bugs

Bugzilla query error

Array ( [type] => error [message] => http-bad-status [params] => Array ( [0] => 429 [1] => Unknown Error ) ) 1

Blog Posts

• Verified cryptography for Firefox 57
• The HACL* Approach
• Shipping HACL* in NSS