Open Bug 1387183 (hacl-star) Opened 2 years ago Updated 4 months ago
[meta] Integrate verified cryptographic primitives into NSS from the HACL* library
Project Everest is a research effort to produce a formally verified HTTPS stack, and part of that effort is producing a library of formally verified cryptographic primitives, known as HACL*. While Project Everest will need more time before having a Firefox-ready TLS library, some of the HACL*-developed algorithms are ready to go, and we should use them in NSS where possible. This is a meta bug to track the integration work. Bug Goals/Objectives 1. Adjust one HACL*-generated cryptographic algorithm to meet the standards for landable code in NSS. - This requires significant interaction with the HACL* team, as any modifications by-hand are likely to render ineffective the formal verification. 2. Implement support in NSS’ TaskCluster to periodically re-verify formally-derived code that is in-tree. 3. Land a first HACL*-generated algorithm into NSS. 4. Iterate to integrate additional formally-verified algorithms.
Meta bug; marking unaffected so it falls off 57 tracking
You need to log in before you can comment on or make changes to this bug.