Security/CryptoEngineering/HACL*

From MozillaWiki
Jump to: navigation, search

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

Full Query
ID Summary Status Assigned to Whiteboard Last change time
1325335 Integrate HACL* EdDSA over Curve25519 ASSIGNED Benjamin Beurdouche [:beurdouche] 2021-04-29T09:27:33Z
1376975 Feature: Integration of HaCl* - Curve25519 (64bits) RESOLVED Franziskus Kiefer [:franziskus] 2017-11-21T10:13:24Z
1383369 Feature: Integration of HaCl* - Chacha20 (not vectorized) RESOLVED Benjamin Beurdouche (do not use this account) 2018-01-25T15:35:07Z
1390935 Review F* Curve25519 code in Hacl* RESOLVED Franziskus Kiefer [:franziskus] 2017-11-13T07:45:07Z
1391859 Review F* Chacha20 code in Hacl* RESOLVED Franziskus Kiefer [:franziskus] 2017-11-23T06:44:52Z
1395549 CI integration for HACL* code RESOLVED Franziskus Kiefer [:franziskus] 2019-08-16T22:05:28Z
1395833 Logically dead code in Curve25519 RESOLVED [CID 1417203], hacl 2017-11-23T06:47:50Z
1396301 verified/kremlib.h:204:23: error: implicit declaration of function 'le64toh' [-Werror=implicit -function-declaration] RESOLVED 2018-01-08T17:45:15Z
1399763 Integration of HaCl* - Poly1305 64-bit (not vectorized) RESOLVED Benjamin Beurdouche (do not use this account) 2018-01-25T15:34:44Z
1405268 shlibsign fails on Solaris due missing htole64 symbol RESOLVED 2017-12-21T10:27:56Z
1419009 Sigsegv at Hacl_EC_crypto_scalarmult on Solaris RESOLVED 2017-11-23T13:23:36Z
1419173 Integration of HaCl* - Track the HACL* master branch and Curve25519 RESOLVED Franziskus Kiefer [:franziskus] 2018-01-25T15:29:56Z
1419342 Add Curve 25519 F* spec RESOLVED Franziskus Kiefer [:franziskus] 2018-05-08T12:38:06Z
1420118 Add verified build flag RESOLVED 2020-01-27T14:53:30Z
1424663 Add HACL* vectorised ChaCha20 RESOLVED Franziskus Kiefer [:franziskus] 2018-03-06T09:04:44Z
1438268 Add HACL* Ed25519 RESOLVED 2018-02-23T14:56:21Z
1441219 Add HACL* Poly1305 32-bit RESOLVED Franziskus Kiefer [:franziskus] 2018-05-07T21:26:09Z
1487950 use compiler-provided 128-bit arithmetic for HACL when compiling with clang-cl RESOLVED 2020-06-08T21:13:11Z
1574643 CI integration for 2019 HACL* code RESOLVED Franziskus Kiefer [:franziskus] 2020-02-07T13:26:28Z
1609569 ChaCha/Poly not hardware accelerated on Pentium Gold processors (non-AVX) NEW 2020-02-27T16:42:27Z
1612492 Integrate HACL* SHA1 and SHA2 NEW 2020-02-05T20:00:36Z
1612493 Integrate AVX2 ChaCha20, Poly1305 and Chacha20Poly1305 from HACL* RESOLVED Benjamin Beurdouche [:beurdouche] 2020-05-11T21:05:01Z
1615555 Integration of HACL* P-256 ASSIGNED Benjamin Beurdouche [:beurdouche] [nss-fx][hacl-star] 2021-04-03T16:17:00Z
1615557 NSS fails to build on some platforms because of HACL* and Kremlin libraries NEW 2020-05-07T09:23:07Z
1617533 HACL* update after changes in libintvector.h RESOLVED Benjamin Beurdouche [:beurdouche] 2020-04-20T21:17:22Z
1698519 Integrate HACL* code for RSA-PSS ASSIGNED Benjamin Beurdouche [:beurdouche] [nss-fx] 2021-03-15T13:52:37Z

26 Total; 6 Open (23.08%); 20 Resolved (76.92%); 0 Verified (0%);


Blog Posts