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 #763
- Functional correctness proofs for AArch64 NTT and INTT in #662
- Functional correctness proofs for Keccakx1 in #826 and #821
- Support for single compilation-unit builds in #612
- Addition of the pair-wise consistency test in #769
- Valgrind-based constant-time tests in #687
- Valgrind-based detection of secret-dependent variable-latency instruction in #693
- Improved x86_64 backend performance in #709
- Documentation of differences to the reference implementation in #799
- Addition of references to FIPS algorithms and equations to relevant functions in #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