OQS: Quo vadis?

[baentsch]

For people not loving Latin: This discussion is to ask how OQS should evolve in terms of level of code support.

So far, OQS has been completely non-committal, anyone daring enough to deploy PQC is basically left hanging high and dry when it comes to using PQC "for real" by a long warning text -- or needs to pay some expensive IT consultancy to mitigate the risks.

This issue is to discuss how to change this: How to make OQS a FOSS package normal users can rely on.

OQS already does (some) testing for constant-time properties, interoperability/KATs, memory leak vulnerabilities, follows upstream security advisories and in general, tries to do reasonable code under sensible licensing terms, but there are many exceptions, sometimes only on specific platforms, sometimes for single algorithms, sometimes we even forget to properly document the security status.

So here's a straw man proposal how to move forward:

Overarching principle: Separate non-committal "research" code from "production ready" code.

Mechanism:

1. Designate algorithms to be subject to thorough testing.
2. Designate tests these algorithms have to pass to be included.
3. Designate licenses these algorithms have to have.
4. Designate "production ready" configuration options.
5. Ascertain proper operation in key downstream projects.
6. Ascertain proper operation in key downstream integrations.
7. Decide whether this is the default configuration for liboqs.

Proposal:

1. Algorithms designated standard "OQS_ALGS_ENABLED=STD".
2. All tests OQS already has, maybe augmented with external code review for these algorithms. Further proposals welcome! For tests agreed, any failure has to be immediately fixed, prior to PR merge or with highest priority if detected after merge.
3. Only MIT or Apache2
4. Initially minimize OQS code executed, by setting CMAKE_BUILD_TYPE=Release OQS_DIST_BUILD=OFF OQS_USE_OPENSSL=ON OQS_OPT_TARGET=generic
5. Confirm proper operation at least in oqsprovider using interop testing with other PQC implementations, e.g., at the IETF cert interop hackathon.
6. Designate packaging projects OQS shall work with and institute CI tests to confirm this. Examples may be Fedora or brew.
7. Yes. This specific config, probably only for specific platform(s), at least x86_64, should be the default config backed by a better support policy.

Any and all feedback solicited. Particularly with so many companies voicing support for OQS no feedback would be disappointing. Also, without feedback, I may be tempted to assume a lack of interest and simply implement my opinion. This may NOT be what you want :-)

[planetf1]

A few thoughts (new contributor caveat!)

1. I think a default configuration for build which only provides 'production' algorithms is an excellent idea and very important. Someone should come along and just be able to use the library (etc) in a sensible way without getting caught out by algorithms which are not necessarily ready unless you know what are are doing

2. Agree aim should be that 'main' is always stable and release-able at any time (in practice this won't be 100% achieved, and releases would signify what one would expect a consumer to use, but should strive for it)

3. This becomes particularly important if the libraries are to be used beyond individual research/academia, ie by companies and included in other stacks. From looking through the code it already seems to mostly be this way, with the addition of BSD-3 and CC0-1.0 ? Whilst the spirit of CC0-1.0 seems aligned, as per the faq in itself it's not a license.. so needs some figuring out.

4. Most important is that this is very clear as the initial recommendation in the docs (and any scripts) for a 'default' build

5. yes. I'm not familar with oqs-provider tests, but also need to consider testing strategy against OpenSSL versions (I see a separate issue is open for alignment on platforms already)

6. Interesting in how the two CIs (packaging project vs oqs) relate.. +1 on brew/fedora. ubuntu / debian / macports also come to mind.

7. aarch64 also increasing in footprint, albeit generic - servers and of course mac m1/2/3

On the last point - I think this issue is really important. Happy to help out with some of the steps needed to make it even easier to consume pqc in both open source & commercial apps

[baentsch]

Happy to help out with some of the steps needed

Great to hear. Looking forward to PRs.

[tomato42]

From Red Hat PoV we are interested in 4 architectures: x86_64, aarch64, ppc64le, and s390x.

[planetf1]

Another topic (perhaps a distinct discussion) is the future relationship between pq-code-package & liboqs etc

[baentsch]

Most definitely. OQS to me feels a bit like a project in decay (no response to this issue serves as a good point in case) and it might be nice to hear what could give it some new impetus. So by all means, please add thoughts in this discussion.

[SWilson4]

Caveat: I was a little late to the party on the PQCP and I haven't been involved in any of the discussion around it up to this point, so take this with a grain of salt.

My hope is that PQCP will help us delineate between "production" and "experimental" tracks. I had envisioned that PQCP would contain high-assurance, "production-ready" implementations, serving as an upstream for a "production" version of liboqs, which would build only these implementations. This "production" library could be distributed via package managers etc similarly to libcrypto. This would in turn (I believe) allow a "production" version of oqs-provider.

[baentsch]

PQCP would contain high-assurance, "production-ready" implementations, serving as an upstream for a "production" version of liboqs

If one assumes PQCP to be delivering "production ready" code from the start, what value would there be to add it to liboqs (from the perspective of creating "production ready" code? We are constantly reducing the number of OQS sub projects, so why bother making OQS "more production ready" (or support more platforms)? Wouldn't it be more sensible to do PQCP integrations instead, e.g., a pqcp-provider?

In addition, wouldn't the "upstream notion" mean that liboqs cannot strive to be "production ready" until PQCP is? So who knows how far that project is wrt releases OQS can utilize for that purpose? Is there a github repo one can check out? @praveksharma ? Further, AFAIK PQCP does not aim to create high assurance classic crypto code (again, I'm not involved in the project, so just guess; so confirmation solicited, @dstebila ?). That however would mean liboqs would need to "resolve" its "production ready" classic code somewhere else... OpenSSL? Either way, liboqs does need to do something if it wants to be used in production.

[dstebila]

If one assumes PQCP to be delivering "production ready" code from the start, what value would there be to add it to liboqs (from the perspective of creating "production ready" code? We are constantly reducing the number of OQS sub projects, so why bother making OQS "more production ready" (or support more platforms)? Wouldn't it be more sensible to do PQCP integrations instead, e.g., a pqcp-provider?

PQCP is probably not going to create binary distributions, nor a library of multiple algorithms. It will be standalone source code implementations, somewhat akin to PQClean.

Further, AFAIK PQCP does not aim to create high assurance classic crypto code (again, I'm not involved in the project, so just guess; so confirmation solicited, @dstebila ?). That however would mean liboqs would need to "resolve" its "production ready" classic code somewhere else... OpenSSL? Either way, liboqs does need to do something if it wants to be used in production.

Still to be determined how the classical algorithms that ML-KEM relies on will appear in PQCP. I don't think PQCP will aim to create high assurance classical crypto code in a standalone way, though some implementations, especially the formally verified ones, might come with their own formally verified SHAKE implementation woven in.

[baentsch]

Still to be determined how the classical algorithms that ML-KEM relies on will appear in PQCP.

PQCP is probably not going to create binary distributions, nor a library of multiple algorithms. It will be standalone source code implementations, somewhat akin to PQClean.

Thanks for your (current) perspective.

Is it possible that PQCP does not have a mission or vision as to what it wants to provide, apart of a collection of source code repositories just as github already does? Just created a question regarding this to the PQCP TSC.

So, taking the above as initial input, let me comment that I think that PQClean is a library of multiple algorithms. Only because of that property, OQS could use it as a common upstream source. If PQCP does not aim to provide at least a common API (normally the hallmark of a library, though) what synergies can PQCP provide to OQS?

Personally, I'd consider this very inefficient and a waste of money from the perspective of software integration (or certification: AFAIK, system components ready to be integrated are getting certified, not singular software code repositories).

It might be worthwhile discussing this then at PQCA (GB) level: Does PQCA want to support OQS as a downstream integration API for others to create "product-ready" binaries/application integrations or does it want PQCP to serve this purpose? Is PQCA willing to fund a possibly disparate collection of source code modules every user still has to integrate into their crypto code stack? If indeed PQCP has no intention to provide a (common/library) interface for multiple algorithms, OQS should (keep) serving this purpose, but begin to develop its own "product ready" code path (incl. common code).

Alternatively, if PQCP should have an API and given that OQS has a long history of code serving the research community, it could keep doing this -- recommending commercial use, e.g., integrations to OpenSSL, to use the new PQCP API, designed only for that purpose.

I personally do not see great value investing much more time in either project until this becomes (more) clear: I "just" want PQC to become usable and productively deploy-able in the real world and thus want to know which project aims to support this going forward -- and which project gets which support in this regard (if any).

[tomato42]

The most important is to clearly specify and maintain the status of the individual algorithms.

If an algorithm is designated "production-ready" (other names available), then that should mean that it has non-problematic licence (most preferably OSI-approved that's not CC0), has extensive test coverage (including against side-channel attacks), and that there is committent to maintain that status (not accepting PRs that would undermine it).

While other things are nice, they aren't as important for production usage.

[SWilson4]

With regard to point (2), my biggest concern about our current testing framework is the lack of coverage for rarely-triggered code. It's conceivable that a bug could exist in code that is triggered by conditions that occur with

• low enough probability that we never hit them in a CI run but
• high enough probability that they are hit "in the wild", when (presumably) the code will be run an order of magnitude more often than it is in CI.

Formal verification should (I believe) address this issue. In the past I've also done manual testing to trigger rarely executed code blocks, but this of course is finicky and not as comprehensive. Should formal verification prove to be a bridge too far, I would concur that some sort of external code review / audit is a decent substitute.

[baentsch]

Hmm -- I'm not sure formally verified code provides the same assurance(s) as code audits, code coverage testing and fuzzing combined (just to name a few alternatives we may consider applying to OQS if we say'd say it should have "production properties"):

For example, is it guaranteed that formally verified code is free of "rarely triggered code"? Doesn't such code (only) provide assurance wrt to adherence to specification, but not absence of errors (e.g., outside of specification)? Does such code guarantee adherence to proper integration and development procedures (e.g., not allowing someone nefarious to introduce an "insecure wrapper" around the formally verified code)?

Therefore, I'd argue OQS --surely if it wants to be independent of upstream sources not providing clear assurances in this regard-- has to have (at least for those parts that will be used "productively")

• fuzzing
• code audits
• code coverage tests (aiming for CI to touch 100%)

As (most of) those things are pretty old issues we never worked on so far I really wonder which appetite truly exists for OQS to take this on. But this really seems to be for the TSC to decide. The discussions here should inform this decision.

[dstebila]

One task for PQCP is to define what assurance levels its implementations meets and find a way to communicate that clearly (pq-code-package/tsc#3).

At a base level formally verified means that "implementation X is proven to implement specification Y", so the assurance is only as good as the inherent correctness of specification Y. Some of the formally verified implementations intended to be included in PQCP have additional formally verified assurances, such as:

• implementation X does not have memory errors
• implementation X does not have input-dependent branching or memory accesses
• implementation X resists the SPECTRE microarchitecture attack

Formal verification is not a complete replacement for auditing, and you are right that problems can be introduced in code wrapped around formally verified code. Likely there will be demand/value in auditing code wrapped around formally verified code, as well as the formal verification toolchain itself -- any maybe even auditing the generated formally verified code as well, I don't know.

One benefit that formal verification can bring compare to audits is that formal verification is mechanical, and can be done in CI -- one could decide to accept a change in formally verified code only once the formal verification tests all pass on that code. But this can be done "cheaply" (for some definitions of cheaply) -- at least compared to starting a whole new manual audit cycle.

[baentsch]

ACK. In sum, this means OQS will need to have auditing (possibly simplified as and when/if PQCP code ever gets integrated to it), fuzzing, code coverage if it aims to be "production ready", e.g., if PQCA supports this goal.

[tomato42]

Hmm, while I agree that an implementation that is formally verified is better than one that's not, personally I put more trust on testing the combined, and complete, system that uses the algorithms.

While PKCS#1v1.5 and CVEs like CVE-2023-0361 are rather worst case scenario, making sure that output of the KEM doesn't leak even if it's used later, not only derived, is necessary for the overall security of the system.

So, I think, what we need in practice is precise definitions of the testing performed, or properties guaranteed by specific formal proofs, and then which of those are applicable to which implementations. This way integrators can decide if they're OK with a given level of assurance, or if they should contribute additional testing.

On top of it there may be a project-recommended level at which an implementation is defined as production grade, but thinking of it more as a threshold rather than the end result, may be better.

[bhess]

my biggest concern about our current testing framework is the lack of coverage for rarely-triggered code

Agreed, it would be desirable to have more extensive coverage for a production track.

Other than formal verification a useful tool will be tailor-made test vectors that trigger more rare cases in an algorithm, less likely to be captured by one (or 100) random KAT. AFAIK there ideas about a PQCP subproject for providing such vectors, which should be worthwhile considering as an addition to the OQS test suite.

Another test that comes to mind are automated tests for issues like Kyberslash. Our current tests for secret-dependent control flow don't automatically capture variable-time instructions (div instructions in the case of Kyberslash). Since these are platform-dependent, a limited set of platforms (and compilers/configurations) supported in a production track would make automation feasible.