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

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

Categories

(NSS :: Libraries, enhancement, P3)

Product:
NSS
Component:
Libraries
Type:
enhancement

Tracking

(firefox56 unaffected, firefox57 unaffected, firefox58 unaffected)

Tracking Flags:
Tracking Status
firefox56 --- unaffected
firefox57 --- unaffected
firefox58 --- unaffected

People

(Reporter: jcj, Assigned: nkulatova)

References

(Depends on 7 open bugs,
URL
)

Details

(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
Status: NEW → ASSIGNED
Meta bug; marking unaffected so it falls off 57 tracking
status-firefox56: --- → unaffected
status-firefox57: --- → unaffected
status-firefox58: --- → unaffected
Depends on: hacl-ci-2
Assignee: franziskuskiefer → nobody
Status: ASSIGNED → NEW
Priority: P1 → --
Depends on: 1612492
Depends on: 1612493
Severity: normal → N/A
Priority: -- → P1
QA Contact: mwobensmith
Assignee: nobody → nkulatova
Depends on: 1753026

Hi,

Hi,

I am from IBM and work with George Wilson. I see that bugzilla 1613236 (https://bugzilla.mozilla.org/show_bug.cgi?id=1613236) is dependent on this.
I am curious if the HaCL generated algorithm is good enough now to be pulled into NSS. Or is it pending on more development in hacl side ?
In general, What is the current status ?

Thanks & Regards,
- Nayna

Flags: needinfo?(nkulatova)

Hello,

Nice to meet you!
Answering your questions:
We consider indeed that the HACL* algorithms could compete with the existing libraries in terms of performance, at the same time providing extremely strong security guarantees. Part of the algorithms we are taking directly from their library (Curve25519, SHA3), whereas some of the code (P256, for instance) is an ongoing development.

In future, we plan to bring RSA-PSS as well. For even longer future, we would like to discuss the post-quantum algorithms, but for now it's an opened question.

Feel free to ping me if you have any other questions, I will be happy to answer (:

Flags: needinfo?(nkulatova)

Hi,

Thanks for your response. Nice to meet you too.
Thanks for sharing the details. I do some more questions especially in context of powerpc support for the same.

Powerpc support in hacl-star got added last year - https://github.com/project-everest/hacl-star/blob/master/dist/gcc-compatible/libintvector.h

And if I look at freebl version of libintvector.h (assuming I am looking at right file) - https://hg.mozilla.org/projects/nss/file/tip/lib/freebl/verified/libintvector.h . It seems it is still not having the updated one from hacl-start for powerpc.

So, I am wondering on the plan/status for updating freebl to include hacl-star powerpc support both in context of bugzilla 1613236 (freebl: POWER poly1305 mac vector acceleration) and in general (if I understand right, it will be used for other algos also like ECC). Is it pending on something else to get libintvector.h powerpc support in FreeBL ?

Can you please share details in this context ?

Thanks & Regards,
- Nayna

Flags: needinfo?(nkulatova)

Yes, the plan is to update NSS the next month in order to support it.

Flags: needinfo?(nkulatova)

Hi,

Looking at this file - https://github.com/nss-dev/nss/blob/master/lib/freebl/verified/libintvector.h . It still seems updated 16 months ago and doesn't have PowerPC support.

Is there any change in plan as I think it was going to get updated sometime in last two months ?

Thanks & Regards,
- Nayna

Flags: needinfo?(nkulatova)

Hi,

Is there any update on this ?

Thanks & Regards,
- Nayna

Flags: needinfo?(nkulatova)
Priority: P1 → P3
You need to log in before you can comment on or make changes to this bug.