mlkem-native

mlkem-native is a C99 implementation of ML-KEM targeting PC, mobile and server platforms. It is a fork of the ML-KEM reference implementation, deviating only to (a) accommodate an interface for native code (e.g. assembler), and (b) facilitate formal verification. mlkem-native provides native code backends in C, AArch64 and x86_64, offering state of the art performance on most Arm, Intel and AMD platforms.

If you need an ML-KEM implementation suitable for embedded systems, see mlkem-c-embedded.

Goals

mlkem-native aims for assurance, ease of use, and performance. We seek implementations which are manually auditable or for which we see a path towards formal verification. All assembly aims to be readable and micro-optimization deferred to automated tooling such as SLOTHY. Ultimately, mlkem-native strives for constant-time implementations for which the C-code is verified to be free of undefined behaviour, and where all assembly is functionally verified.

Current state

mlkem-native is work in progress. WE DO NOT CURRENTLY RECOMMEND RELYING ON THIS LIBRARY IN A PRODUCTION ENVIRONMENT OR TO PROTECT ANY SENSITIVE DATA. Once we have the first stable version, this notice will be removed.

Performance

mlkem-native has complete AArch64 and AVX2 backends of competitive performance (see benchmarks).

Verification

All C code in mlkem/* is verified to be memory and type safe using CBMC. This excludes, for example, out of bounds accesses, as well as integer overflows during optimized modular arithmetic. See the CBMC Readme and the CBMC Proof Guide for more information and how to reproduce the proofs. The code in fips202/* has not yet been verified using CBMC.

Initial experiments are underway to verify AArch64 using HOL-Light.

Getting started

Nix setup

All the development and build dependencies are specified in flake.nix. We recommend installing them using nix.

To execute a bash shell with the development environment specified in flake.nix, run

nix develop --experimental-features 'nix-command flakes'

Native setup

To build mlkem-native, you need make and a C99 compiler. To use the test scripts, you need Python3 with dependencies as specified in requirements.txt. We recommend using a virtual environment, e.g.:

python3 -m venv venv
./venv/bin/python3 -m pip install -r requirements.txt
source venv/bin/activate

Using make

You can build tests and benchmarks using the following make targets:

make mlkem
make bench
make bench_components
make nistkat
make kat

The resulting binaries can be found in test/build.

Using tests script

We recommend compiling and running tests and benchmarks using the ./scripts/tests script. For example,

./scripts/tests func

will compile and run functionality tests. For detailed information on how to use the script, please refer to the --help option.

Call for contributors

We are actively seeking contributors who can help us build mlkem-native. If you are interested, please contact us, or volunteer for any of the open issues.

Call for potential consumers

If you are a potential consumer of mlkem-native, please reach out: We're interested in hearing the way you want to use mlkem-native. If you have specific feature requests, please open an issue.