1387183 - (hacl-star) [meta] Integrate verified cryptographic primitives into NSS from the HACL* library

Status: NEW

(NSS :: Libraries, enhancement, P3)

Description

[J.C. Jones [:jcj] (he/him)]

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.

Comment 1

[J.C. Jones [:jcj] (he/him)]

Meta bug; marking unaffected so it falls off 57 tracking

Comment 2

[Nayna Jain]

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

Comment 3

[Anna Weine]

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 (:

Comment 4

[Nayna Jain]

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

Comment 5

[Anna Weine]

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

Comment 6

[Nayna Jain]

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

Comment 7

[Nayna Jain]

Hi,

Is there any update on this ?

Thanks & Regards,
- Nayna