mlkem-native

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

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⁴. All AArch64 and x86_64 assembly is proved to be functionally correct,
memory-safe, and of secret-independent timing (constant-time), using 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

bash
# 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⁶ or 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⁸:
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⁹ and the
Wycheproof¹⁰ ML-KEM test vectors.

ACVP

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

bash
# 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

# Using specific ACVP test vector files (downloaded from the ACVP-Server)
# python3 ./test/acvp/acvp_client.py -p {PROMPT}.json -e {EXPECTED_RESULT}.json
# For example, assuming you have run the above
python3 ./test/acvp/acvp_client.py \
  -p ./test/acvp/.acvp-data/v1.1.0.41/files/ML-KEM-keyGen-FIPS203/prompt.json \
  -e ./test/acvp/.acvp-data/v1.1.0.41/files/ML-KEM-keyGen-FIPS203/expectedResults.json

Wycheproof

You can run Wycheproof¹⁰ tests using the tests script or the Wycheproof client directly:

bash
# Using the tests script
./scripts/tests wycheproof

# Using the Wycheproof client directly
python3 ./test/wycheproof/wycheproof_client.py

Benchmarking

You can measure performance, memory usage, and binary size using the tests script:

bash
# Speed benchmarks (-c selects cycle counter: NO, PMU, PERF, or MAC)
# Note: PERF/MAC may require the -r flag to run benchmarking binaries using sudo
./scripts/tests bench -c PMU
./scripts/tests bench -c PERF -r

# Stack usage analysis
./scripts/tests stack

# Binary size measurement
./scripts/tests size

For CI benchmark results and historical performance data, see the benchmarking page.

Usage

If you want to use mlkem-native, import mlkem into your project's source tree and build using your favourite build system. See mlkem for more information, and
examples/basic for a simple example. The build system provided in this repository is for development purposes only.

Can I bring my own FIPS-202?

mlkem-native relies on and comes with an implementation of FIPS-202¹¹. If your library has its own FIPS-202 implementation, you
can use it instead of the one shipped with mlkem-native. See FIPS202.md, and examples/bring_your_own_fips202
for an example using tiny_sha3¹².

Do I need to use the assembly backends?

No. If you want a C-only build, just omit the directories mlkem/src/native and/or mlkem/src/fips202/native from your import
and unset MLK_CONFIG_USE_NATIVE_BACKEND_ARITH and/or MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 in your mlkem_native_config.h.

Do I need to setup CBMC to use mlkem-native?

No. While we recommend that you consider using it, mlkem-native will build + run fine without CBMC -- just make sure to
include cbmc.h and have CBMC undefined. In particular, you do not need to remove all function
contracts and loop invariants from the code; they will be ignored unless CBMC is set.

Does mlkem-native support all security levels of ML-KEM?

Yes. The security level is a compile-time parameter configured by setting MLK_CONFIG_PARAMETER_SET=512/768/1024 in mlkem_native_config.h.
If your library/application requires multiple security levels, you can build + link three instances of mlkem-native
while sharing common code; this is called a 'multi-level build' and is demonstrated in examples/multilevel_build. See also mlkem.

Can I bring my own backend?

Yes, you can add further backends for ML-KEM native arithmetic and/or for FIPS-202. Follow the existing backends
as templates or see examples/custom_backend for a minimal example how to register a custom backend.

Have a Question?

If you think you have found a security bug in mlkem-native, please report the vulnerability through
Github's private vulnerability reporting. Please do not
create a public GitHub issue.

If you have any other question / non-security related issue / feature request, please open a GitHub issue.

Contributing

If you want to help us build mlkem-native, please reach out. You can contact the mlkem-native team
through the PQCA Discord. See also CONTRIBUTING.md.

Strictly speaking, we rely on C90 + stdint.h + 64-bit unsigned long long. ↩
National Institute of Standards and Technology: FIPS 203 Module-Lattice-Based Key-Encapsulation Mechanism Standard, https://csrc.nist.gov/pubs/fips/203/final ↩
Bos, Ducas, Kiltz, Lepoint, Lyubashevsky, Schanck, Schwabe, Seiler, Stehlé: CRYSTALS-Kyber C reference implementation, https://github.com/pq-crystals/kyber/tree/main/ref ↩
Diffblue, Amazon Web Services: C Bounded Model Checker, https://github.com/diffblue/cbmc ↩
John Harrison: HOL-Light Theorem Prover, https://hol-light.github.io/ ↩
Bernstein, Bhargavan, Bhasin, Chattopadhyay, Chia, Kannwischer, Kiefer, Paiva, Ravi, Tamvada: KyberSlash: Exploiting secret-dependent division timings in Kyber implementations, https://kyberslash.cr.yp.to/papers.html ↩
Antoon Purnal: clangover, https://github.com/antoonpurnal/clangover ↩
Abdulrahman, Becker, Kannwischer, Klein: Fast and Clean: Auditable high-performance assembly via constraint solving, https://eprint.iacr.org/2022/1303 ↩
National Institute of Standards and Technology: Automated Cryptographic Validation Protocol (ACVP) Server, https://github.com/usnistgov/ACVP-Server ↩
Community Cryptography Specification Project: Project Wycheproof, https://github.com/C2SP/wycheproof ↩ ↩²
National Institute of Standards and Technology: FIPS202 SHA-3 Standard: Permutation-Based Hash and Extendable-Output Functions, https://csrc.nist.gov/pubs/fips/202/final ↩
Markku-Juhani O. Saarinen: tiny_sha3, https://github.com/mjosaarinen/tiny_sha3 ↩