Another verified implementation of MLKEM

[Rod Chapman]

Good morning everyone. Well… it seems like verified implementations of MLKEM are like buses… you wait for ages, then three come along at once…Earlier today, I pressed the GitHub “Make it Public” button on my own reference implementation of MLKEM here https://github.com/awslabs/LibMLKEMFrom the top-level README:This library presents a new reference implementation of FIPS 203 ML-KEM (the algorithm formerly known as Kyber), as specified in the 24th August 2023 Draft of FIPS 203.
The goals of producing these implementations are:

• To act as a vehicle for detailed review of FIPS 203.
• To produce a reference implementation of ML-KEM which is completely independent of all other known implementations of Kyber.
• To test the capability of contemporary formal languages and verification tools, such as SPARK, CBMC and Kani, and to act as a challenge problem for those languages and tools.
• To act as a set of verification challenges for the underlying SMT provers, in particular CVC5.
• As a demonstration of “hybrid” static and dynamic verification. In particular, our goal is static proof of the absence of undefined behaviour, memory-safety, and type-safety, while dynamic known-answer tests (KATs) are used to demonstrate functional correctness.

Important warning
These implementations are absolutely NOT intended for production or any use in a “high assurance” setting. In particular:

• While the code may be written in a “constant time” style, this property is not formally verified at the level of the generated code and micro-architecture, and is not guranteed to be preserved by all compilers.
• Secondly, intermediate values are not sanitized at present, as required by FIPS 203 3.3 (line 699)
• Finally, performance is unlikely to be competitive with other, more optimized, implementations.

I actually look forward to members of the community having a look at this. While I'm sure that many of you won't feel familiar with Ada or SPARK, I consider "not readable" to be a bug, and will endeavour to fix any such issues.

All the best,

 Rod

[Wrenna Robson]

Very cool, Rod. Currently in the middle of planning a house move so I don't yet have space to give this the time it deserves but it's certainly going on my list as a special treat to read when I have a chance.

Best,

Wrenna

--
You received this message because you are subscribed to the Google Groups "pqc-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pqc-forum+...@list.nist.gov.
To view this discussion on the web visit https://groups.google.com/a/list.nist.gov/d/msgid/pqc-forum/31051a9e-8699-4fc9-ba7a-fae5529ed7c4n%40list.nist.gov.