liboqs
liboqs copied to clipboard
open-quantum-safe
Integrate Kyber implementation from libjade
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/
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.
Even if there isn't a full chain of formal verification for the entire library, having higher assurance in some components still seems worthwhile.
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?
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_upstreamor 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.