v1.0.0-beta

[mkannwischer]

mlkem-native v1.0.0-beta

About

mlkem-native is a secure, fast and portable C90 implementation of ML-KEM. It is a fork of the ML-KEM reference implementation.

mlkem-native includes native backends for AArch64 and AVX2, offering competitive performance on most Arm, Intel and AMD platforms (see benchmarks). The frontend and the C backend (i.e., all C code in mlkem/* and mlkem/fips202/*) are verified using CBMC to be free of undefined behaviour. In particular, there are no out of bounds accesses, nor integer overflows during optimized modular arithmetic. HOL-Light is used to verify functional correctness of selected AArch64 assembly routines.

mlkem-native is supported by the Post-Quantum Cryptography Alliance as part of the Linux Foundation.

Release notes

This is the second official release of mlkem-native, a secure, fast and portable C90 implementation of ML-KEM.
This beta release expands the scope of formal verification (using CBMC and HOL-Light), improves FIPS compliance by adding improves FIPS compliance by adding PCT, buffer zeroization, and documentation, and increases the confidence in resistance against timing side-channels through extensive Valgrind-based testing.

What's New

Compared to v1.0.0-alpha the following
major improvements have been integrated into mlkem-native:

• Full CBMC proof coverage of the C frontend and backend including FIPS202
• Destruction of intermediate values in Destruct intermediate values #763
• Functional correctness proofs for AArch64 NTT and INTT in Add functional correctness proofs for AArch64-optimized NTT and invNTT in HOL Light #662
• Functional correctness proofs for Keccakx1 in Add proof for AArch64+SHA3 Keccak-f1600-x1 #826 and HOL-Light: Add proof for Keccak-F1600-x1 aarch64 asm #821
• Support for single compilation-unit builds in Add support for single-CU build #612
• Addition of the pair-wise consistency test in Add Pairwise Consistency Test (PCT) for FIPS 140-3 IG compliance #769
• Valgrind-based constant-time tests in Add Valgrind-based constant-time tests #687
• Valgrind-based detection of secret-dependent variable-latency instruction in Add Valgrind-based detection of variable-latency instructions #693
• Improved x86_64 backend performance in Add AVX2 native polynomial compress/decompression #709
• Documentation of differences to the reference implementation in Document relation to reference implementation #799
• Addition of references to FIPS algorithms and equations to relevant functions in Requirements Traceability: Add FIPS 203 citations to function headers #776
• Numerous documentation improvements
• Additional examples on using mlkem-native (see examples/)

See the full change log here: v1.0.0-alpha...v1.0.0-beta

---

This discussion was created from the release v1.0.0-beta.