v1.0.0-beta

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

v1.0.0-alpha

mlkem-native v1.0.0-alpha

About

mlkem-native is a C90 implementation of ML-KEM targeting PC, mobile and server platforms. It is a fork of the ML-KEM reference implementation.

mlkem-native aims to be fast, secure, and easy to use: It provides native code backends in C, AArch64 and x86_64, offering state-of-the-art performance on most Arm, Intel and AMD platforms. The C code in mlkem/* is verified using CBMC to be free of undefined behavior. In particular, there are no out of bounds accesses, nor integer overflows during optimized modular arithmetic.

Release notes

This is first official release of mlkem-native, a C90 implementation of ML-KEM targeting PC, mobile and server platforms. This alpha release of mlkem-native features complete backends in C, AArch64 and x86_64, offering state-of-the-art performance on most Arm, Intel and AMD platforms.

With this alpha release we intend to spark experiments on integrations of mlkem-native in other software. We appreciate any feedback on how to improve and extend mlkem-native in the future. Please open an issue on https://github.com/pq-code-package/mlkem-native. While we continue on improving and extending mlkem-native, we expect that the majority of the code is stable. In particular, the core external APIs are stable; we will potentially expose additional functions (e.g., operating on expanded secret keys) in the future.