Security/CryptoEngineering/HACL*
From MozillaWiki
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
| ID | Summary | Status | Assigned to | Whiteboard | Last change time |
|---|---|---|---|---|---|
| 1325335 | Integrate HACL* EdDSA over Curve25519 | RESOLVED | Anna Weine | [nss-nofx] | 2024-04-02T17:30:13Z |
| 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] | 2024-04-02T15:59:08Z | |
| 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 | 2022-10-11T23:50:58Z | ||
| 1612492 | Integrate HACL* SHA1 and SHA2 | NEW | 2023-10-16T14:36:19Z | ||
| 1612493 | Integrate AVX2 ChaCha20, Poly1305 and Chacha20Poly1305 from HACL* | RESOLVED | Benjamin Beurdouche [:beurdouche] | 2020-05-11T21:05:01Z | |
| 1613236 | freebl: POWER poly1305 mac vector acceleration | NEW | [nss-fx] | 2024-02-19T17:04:08Z | |
| 1615555 | Integration of HACL* P-256 | RESOLVED | Anna Weine | [nss-fx][hacl-star] | 2024-02-18T20:09:18Z |
| 1615557 | NSS fails to build on some platforms because of HACL* and Kremlin libraries | NEW | 2022-10-11T23:57:15Z | ||
| 1617533 | HACL* update after changes in libintvector.h | RESOLVED | Benjamin Beurdouche [:beurdouche] | 2020-04-20T21:17:22Z | |
| 1698519 | Integrate HACL* code for RSA-PSS | RESOLVED | Anna Weine | [nss-fx] | 2023-04-18T15:11:34Z |
| 1725142 | FTBFS on Debian kfreebsd | UNCONFIRMED | [nss-nofx] | 2022-03-15T11:38:32Z | |
| 1727555 | HACL* update - Q2 2022 | RESOLVED | Anna Weine | [nss-fx] | 2023-04-17T08:50:53Z |
| 1740834 | Use ARM crypto extension for SHA512 on Apple M1 | NEW | 2023-12-13T23:30:25Z | ||
| 1750698 | Integration of HACL* - GCM mac | ASSIGNED | Anna Weine | [nss-fx] | 2023-04-18T15:12:33Z |
| 1753026 | Integrate HACL* SHA3 | RESOLVED | Anna Weine | 2023-07-11T14:28:30Z | |
| 1854438 | Integrate HACL* P-384 | NEW | karthik.bhargavan | 2024-03-03T16:17:37Z | |
| 1854439 | Integrate HACL* P-521 | NEW | karthik.bhargavan | 2024-03-03T16:17:39Z |
34 Total; 9 Open (26.47%); 25 Resolved (73.53%); 0 Verified (0%);
