Regarding the definition of "Assurance"

[vincentvbh]

Dear MLKEM-C-AARCH64 maintainers,

I think the definition of "Assurance" doesn't reflect the state-of-the-art development in the literature.
"Clean" is not a necessity for a program to be amenable to verification. There are continuous efforts to formally verify high-performance, highly complicated (extensively shuffled), manually written, and highly scalable (in the case of power-of-two-size NTT/iNTT) assembly code.

In the second item of "tensions",
it says "Optimal code is complex (e.g. relying on handwritten assembly), impeding maintainenance and amenability for audit or verification." (maintainenance -> maintenance). This was already resolved for some of the frequently used operations, such as Keccak permutation by https://eprint.iacr.org/2023/1861, and NTT by https://tches.iacr.org/index.php/TCHES/article/view/9838.

Recently, the latest manually shuffled NTT/iNTT for Kyber (https://github.com/neon-ntt/neon-ntt/blob/master/kyber768/ntt/__asm_NTT.S) has been formally verified with the tool CryptoLine. See fmlab-iis/cryptoline@1e0173c.
Readability for the general audience is not a requirement for formal verification (I'm sure that the resulting programs are readable for the authors if they put effort into structuring the extensively optimized assembly programs). This is one of the goals of CryptoLine: formally verifying assembly programs optimized "in the wild."
As for maintenance, you don't have to worry about that. I'm the author of the latest NTT/iNTT for Kyber and I only spent two afternoons on shuffling (the resulting programs perform comparably to the programs by SLOTHY on Cortex-A72 and Apple M1 Pro).

I believe users of this repository should be informed about the above, so they don't have to worry about something that is already addressed.

Vincent

[hanno-becker]

Hi Vincent,

Thanks for chiming in, and congratulations for verifying your NTT!

You make fair points, there are tools such as CryptoLine that can verify highly optimized and interleaved implementations. We will be considering those for MLKEM-C-AArch64 as well, but it's too early to say anything definite.

As for maintenance and amenability to audit, I'd maintain that there's added value in clean code: If you want to understand what the code is doing, for example to experiment with changes, it's much easier on the basis of clean code. Moreover, re-optimizing the code after making such changes, or when targeting a new microarchitecture, is considerably less effort with automated optimization.

This does not mean that manually optimized + verified code has no place or is somehow a flawed approach -- not at all. Achieving highly optimized + formally verified code, like you have done for the NTT or e.g. s2n-bignum provides for many classical cryptographic routines, is a remarkable feat. Yet, if we have a chance to additionally achieve transparency and scalability through clean code and automated optimization, I'd like us to have a shot at it. It certainly is possible, e.g. s2n-bigum now has a verified and automatically optimized implementation of x25519 (see this RWC'24 talk).

How things turn out for MLKEM-C-AArch64 is TBD, it's still early days.

Thanks again for your input and the references,
Hanno

[mkannwischer]

Thanks @vincentvbh for the pointer!

I agree with @hanno-becker on this that there is value in clean code and if there is formally-verified clean code (of comparable speed) it is preferrable.
I think we are all in agreement that using formally-verified code is preferrable over using non-verified code. That's also reflected in recent discussions on what level of assurance mlkem-c-aarch64 should aim for - we concluded that all assembly has to be verified. We have not settled on a formal verification toolchain yet though.

Another aspect is that for this project we are targeting a range of different uArchs and it's much easier to leave microarchitectural optimization to an automated tool.