mlkem-native

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

All C code in mlkem/src/* and mlkem/src/fips202/* is proved memory-safe (no memory overflow) and type-safe (no integer overflow) using CBMC[^CBMC]. All AArch64 and x86_64 assembly is proved to be functionally correct, memory-safe, and of secret-independent timing (constant-time), using HOL-Light[^HOL-Light].

mlkem-native includes native backends for Arm (64-bit, Neon), Intel/AMD (64-bit, AVX2), RISC-V (64-bit, RVV), and POWER (ppc64le, VSX). See benchmarks for performance data.

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

Quickstart for Ubuntu

# Install base packages
sudo apt-get update
sudo apt-get install make gcc python3 git

# Clone mlkem-native
git clone https://github.com/pq-code-package/mlkem-native.git
cd mlkem-native

# Build and run tests
make build
make test

# The same using `tests`, a convenience wrapper around `make`
./scripts/tests all
# Show all options
./scripts/tests --help

See BUILDING.md for more information.

Applications

mlkem-native is used in

• libOQS of the Open Quantum Safe project since 0.13.0 (as the default ML-KEM implementation)
• AWS' Cryptography library AWS-LC since v1.50.0
• The rustls TLS library written in Rust since 0.23.28 (through AWS-LC as the default cryptography provider)
• Pavona - a library of modular, tapeout-proven, and secure-by-default open silicon blocks

Formal Verification

All C code in mlkem/src/* and mlkem/src/fips202/* is proved memory-safe (no memory overflow) and type-safe (no integer overflow). This uses the C Bounded Model Checker (CBMC) and builds on function contracts and loop invariant annotations in the source code. See proofs/cbmc for details.

All AArch64 and x86_64 assembly is proved functionally correct, memory-safe, and to have secret-independent timing (constant-time), at the object-code level. This uses the HOL-Light interactive theorem prover and the s2n-bignum verification infrastructure (which includes models of the relevant parts of the Arm and x86 architectures). See proofs/hol_light for details.

NOTE: Formal Verification is never absolute. See SOUNDNESS.md for a detailed analysis of the scope, assumptions and risks of the formal verification efforts around mlkem-native.

Security

All AArch64 and x86_64 assembly in mlkem-native is formally proved in HOL Light to be free of secret-dependent control flow, memory access patterns, and variable-latency instructions, thwarting most timing side channels (see proofs/hol_light for details). C code is hardened against compiler-introduced timing side channels (such as KyberSlash[^KyberSlash] or clangover[^clangover]) through suitable barriers and constant-time patterns.

Absence of secret-dependent branches, memory-access patterns and variable-latency instructions is also tested using valgrind with various combinations of compilers and compilation options.

Other attacks. mlkem-native targets resistance against timing side-channels only. Other attack classes, such as power and electromagnetic side-channels, microarchitectural side-channels (e.g. speculative execution), or fault-injection attacks, are currently out of scope.

Design

mlkem-native is split into a frontend and two backends for arithmetic and FIPS202 / SHA3. The frontend is fixed, written in C, and covers all routines that are not critical to performance. The backends are flexible, take care of performance-sensitive routines, and can be implemented in C or native code (assembly/intrinsics); see mlkem/src/native/api.h for the arithmetic backend and mlkem/src/fips202/native/api.h for the FIPS-202 backend.

mlkem-native currently offers the following backends:

• Default portable C backend
• 64-bit Arm backend (using Neon)
• 64-bit Intel/AMD backend (using AVX2)
• 64-bit RISC-V backend (using RVV)
• 64-bit POWER backend (ppc64le, using VSX; supports POWER8 and above)
• 32-bit Armv8.1-M backend (using Helium/MVE) -- see #1501. This is still experimental and disabled by default.

If you'd like contribute new backends, please reach out or just open a PR.

Our AArch64 assembly is developed using the SLOTHY superoptimizer, following the approach described in the SLOTHY paper[^SLOTHY_Paper]: We write 'clean' assembly by hand and automate micro-optimizations (e.g. see the clean vs optimized AArch64 NTT). See dev/README.md for more details.

Test Vectors

mlkem-native is tested against all official ACVP ML-KEM test vectors[^ACVP] and the Wycheproof[^wycheproof] ML-KEM test vectors.

ACVP

You can run ACVP tests using the tests script or the ACVP client directly:

# Using the tests script
./scripts/tests acvp
# Using a specific ACVP release
./scripts/tests acvp --version v1.1.0.41

# Using the ACVP client directly
python3 ./test/acvp/acvp_client.py
python3 ./test/acvp/acvp_client.py --version v1.1.0.41