Open Bug 1387183 (hacl-star) Opened 2 years ago Updated 4 months ago

[meta] Integrate verified cryptographic primitives into NSS from the HACL* library


(NSS :: Libraries, enhancement, P1)



(firefox56 unaffected, firefox57 unaffected, firefox58 unaffected)

Tracking Status
firefox56 --- unaffected
firefox57 --- unaffected
firefox58 --- unaffected


(Reporter: jcj, Assigned: franziskus)


(Depends on 3 open bugs, )


(Keywords: meta)

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.
Assignee: nobody → franziskuskiefer
Depends on: hacl-ci
Depends on: hacl-eddsa
Depends on: hacl-poly1305
Meta bug; marking unaffected so it falls off 57 tracking
Depends on: 1419173
Depends on: 1419342
Depends on: 1420118
Depends on: 1424663
Depends on: 1441219
Depends on: hacl-ci-2
You need to log in before you can comment on or make changes to this bug.