search

pq-code-package / mlkem-c-aarch64

ML-KEM implementation optimized for aarch64
Apache License 2.0
3 stars 5 forks source link

Assurance Level #37

Open mkannwischer opened 1 month ago

mkannwischer commented 1 month ago

According to the PQCP charter, the goal for projects within PQCP is to build high-assurance production-ready software implementations of forthcoming post-quantum cryptography standards, starting with the ML-KEM algorithm

During the first PQCP TSC meeting it was discussed that we should be more explicit on what we mean by high-assurance production-ready. This differs between different sub-projects of PQCP and it would be good to come up with some assurance levels to unify between different project. For the next TSC meeting (May 23), each sub-project should document the corresponding interpretation of high-assurance production-ready and document the intended level of assurance.

Let's discuss here.

hanno-becker commented 1 month ago

Ultimately, I would like to see at least:

hanno-becker commented 1 month ago

@mkannwischer @cothan Thoughts?

mkannwischer commented 1 month ago

What do you mean by "ASM code is verified for functional correctness"? You mean by passing testvectors? I think we need to distinguish between the ultimate goal and the initial goal for a first release. Initially, I'd aim for no formal verification, i.e., likely the lowest assurance level of the PQCP This would aim to

All of the tests should be integrated into CI. For the code audits there is going to be a process to go through in the PQCA. There is some budget for this in the PQCA and we need to talk to the TAC to get this started.

hanno-becker commented 1 month ago

What do you mean by "ASM code is verified for functional correctness"? You mean by passing testvectors?

No, I meant formal verification against a specification on the basis of some architecture model.

I think we need to distinguish between the ultimate goal and the initial goal for a first release.

Agreed. I described above what I would like to see as the mid-term assurance level for this repository, but not necessarily as the baseline upon first release. We should clarify at the next TSC meeting what we're talking about.

cothan commented 1 month ago

I don't know much about formal verification, at our first release we can use some model checker to verify the code. I'm learning how to use CBMC, but I'm not sure if it can check SIMD instructions. I will try soon.

mkannwischer commented 1 month ago

CBMC would only be useful for the C sources, right? I think there is still plenty of functions that are going to stay in C as they are not performance critical for which this is going to be useful. Those are likely the same functions that can be shared with other implementations within the PQCP. In case we are considering to use CBMC, I think we should discuss this in the TSC as well to make sure everyone is on-board with that.

hanno-becker commented 1 month ago

CBMC will be a useful tool for verifying the absence of certain classes of undefined behaviour in the C sources (only). One can also specify custom assertions and have CBMC attempt to prove those, but I am unsure if this would we practical for the functional specifications encountered in MLKEM, esp. modular arithmetic. See e.g. how in LibMLKEM the correctness of modular multiplication has to be deferred to interactive provers

hanno-becker commented 1 month ago

In case we are considering to use CBMC, I think we should discuss this in the TSC as well to make sure everyone is on-board with that.

I don't object to bringing this up, but it's not urgent, and ultimately our choice, isn't it?

cothan commented 1 month ago

Honestly, I have no idea what can and what cannot work in formal verification for ML-KEM. So my opinion about high assurance tool set is naive. I can learn from your PRs. Definitely, it CBMC isn't our ultimately choice, even the pure C implementation has to deal with modular arithmetic correctness so it may not be the only tool we use. But again, I have no idea and no background in formal. So @hanno-becker and @mkannwischer please take the lead.

hanno-becker commented 1 month ago

We don't have to sort the how at this point, only agree on what we want to achieve.

In the interest of progress, I think @mkannwischer points above make sense for an initial pre-release. At the same time, I don't think we qualify as "high assurance" and "production-ready" if we don't handle functional correctness of at least the assembly.

rod-chapman commented 1 month ago

I concur with Hanno. To expand a little, reasonable targets for formal (static) verification would be:

  1. Absence of undefined behaviour.
  2. Absence of all other memory- and type-safety defects, including arithmetic overflows.
  3. Absence of dependence on unspecified behaviour (e.g. no dependence on expression evaluation order).

These are basic targets that must come first before other, more advanced proofs could be attempted.

(PS.. allow me to introduce myself: I am Rod, colleague of Hanno at AWS. I am responsible for the LibMLKEM SPARK/Ada implementation and its proof.)

mkannwischer commented 1 month ago

Thanks @rod-chapman!

Would you see these basic targets as required for any kind of deployment, or do you see value in having a fast implementations first and adding these (basic) proofs later?

rod-chapman commented 1 month ago

Basic proofs of all the C code would be a good starting point, and should come first. Additional proofs of optimized assembly code can come later as and when needed.

(There are some additional full correctness proofs in my SPARK code, for example ... the correctness of "*" (mod Q) on Zq for example.)

rod-chapman commented 1 month ago

One concern I have is that there appears to be repetition of C code across all our proposed repositories? Why? I see no need at all to have the same C code repeated and/or copied across several repo's. The non-time-critical stuff should identical for all platforms anyway.

hanno-becker commented 1 month ago

@rod-chapman I agree that a shared C code base is preferred, but it is TBD if it can be achieved. For example, the AArch64 repository will require changes to the C code when introducing the batched Keccak API, which the maintainers of mlkem-c-generic may or may not want to upstream.

rod-chapman commented 1 month ago

"Batched" or "not batched" is an implementation detail. Surely, the API should be the same regardless...

hanno-becker commented 1 month ago

I thought you're talking about the C code, which is part of the implementation.

mkannwischer commented 1 month ago

I agree that we want to share as much as possible between the C projects (embedded, generic, aarch64 for now). Maybe we even want to combine them into a single project at some point.

The reason for starting off with separate code bases was the different goals of the projects: In particular, the generic project wants to stay in sync with the Kyber teams reference implementation and they want to make as few changes as possible. That's why we started off our own copy and postponed the discussion of code sharing to a later point. (Since nothing has been merged into the generic project so far, I believe this was a good approach).

I'm happy to kick-off the discussion of code sharing between embedded and aarch64 projects now. Let's do that in a separate issue: https://github.com/pq-code-package/mlkem-c-aarch64/issues/42

hanno-becker commented 3 weeks ago

Related: #63