Integrate Kyber implementation from libjade

[dstebila]

libjade is a Jasmin project involving @cryptojedi and others that has a formally verified implementation of Kyber for some platforms. We have talked about incorporating that into liboqs.

From an email to me by @cryptojedi:

On May 6, 2023, at 8:24 AM, Peter Schwabe [email protected] wrote:

As we discussed interfacing between OQS/OpenSSL/Sandwich and Libjade in
Lisbon, I thought I'd let you know that yesterday we got a second
release of Libjade out, which is hopefully a good starting point:
https://github.com/formosa-crypto/libjade/releases/latest

We mostly made sure that the Kyber code matches the code we formally
verified, added a derandomized API, and improved documentation; see
https://github.com/formosa-crypto/libjade/blob/release/2023.05/README.md
https://github.com/formosa-crypto/libjade/blob/release/2023.05/doc/api.md

As a word of warning: the AVX2 implementation of Kyber in Libjade is
currently the "fully optimized" one and not the "fully verified" one,
i.e., the matrix generation is not proven. See
https://eprint.iacr.org/2023/215, just before Section 5. Also, we
haven't integrated the proofs with Libjade, yet, and consequently
they're not covered by CI. That's one of the plans for the next release.

We are, of course, happy for any kind of feedback by mail or in the
Formosa-Crypto Zulip: https://formosa-crypto.zulipchat.com/login/

[baentsch]

What is the ultimate goal behind this issue? Make libjade's Kyber accessible to the downstreams of liboqs? What is the value thereof? Neither liboqs nor any of its downstreams are formally verified, so I presume this property of libjade is lost when integrated, no?

In turn, deciding on a specific API (and application) to add this to, e.g., a FIPS-certifiable OpenSSL Kyber provider based on libjade (also itself verified) sounds like a (probably also commercially) interesting goal.

[dstebila]

Even if there isn't a full chain of formal verification for the entire library, having higher assurance in some components still seems worthwhile.

[baentsch]

To state something probably painfully obvious: This integration ought to be automatically repeatable after the first time, e.g., by way of using copy_from_upstream or github submodule, right? And this is still intended for 0.10.0?

[dstebila]

To state something probably painfully obvious: This integration ought to be automatically repeatable after the first time, e.g., by way of using copy_from_upstream or github submodule, right? And this is still intended for 0.10.0?

Yes, it is intended for this to be repeatable. Unclear at this point whether it'll be for 0.10.0, this is also tied up with #1521.

[baentsch]

Any reason not to close this issue @praveksharma ?

[praveksharma]

Closing now @baentsch.