mlkem-native: A high-assurance, high-performance ML-KEM implementation
406 views
Skip to first unread message
Matthias Kannwischer
Dec 18, 2024, 12:08:30 AM12/18/24
to pqc-forum, Hanno Becker
We would like to bring the community's attention to the v1.0.0-alpha release of mlkem-native: An open-source (Apache-2.0), high-assurance, high-performance C90 implementation of ML-KEM. Link: https://github.com/pq-code-package/mlkem-native
mlkem-native is derived from the ML-KEM reference implementation: The latter is simple, vetted by the community for years, and the basis of various optimized research implementations. To unify, we added a frontend/backend split that combines a fixed C frontend with a choice of optimized backends in C or native code. Currently, mlkem-native comes with an AArch64 backend (derived from [1] and [2]) and an AVX2 backend (derived from [3]), offering state of the art performance on Arm64 and x86.
Further increasing confidence in the reference implementation as well as our deviations from it, we use the C Bounded Model Checker (CBMC) [4] to show absence of out of bounds accesses and carefully track the bounds of arithmetic data, establishing that there are no integer overflows; this currently covers all C code except for pieces of SHA-3, which are work in progress. Experiments are underway to use the HOL-Light/s2n-bignum verification infrastructure [5] for verification at the assembly level (see proofs for SLOTHY-optimized versions of the AArch64 NTT and invNTT by John Harrison here: [6])
All native code is constant-time in the sense that it is free of secret-dependent control flow, memory access, and instructions that are commonly variable-time, thwarting most timing side channels. The C code is hardened against compiler-introduced timing side channels (such as KyberSlash or clangover) through suitable barriers and constant-time patterns.
mlkem-native is derived from the ML-KEM reference implementation: The latter is simple, vetted by the community for years, and the basis of various optimized research implementations. To unify, we added a frontend/backend split that combines a fixed C frontend with a choice of optimized backends in C or native code. Currently, mlkem-native comes with an AArch64 backend (derived from [1] and [2]) and an AVX2 backend (derived from [3]), offering state of the art performance on Arm64 and x86.
Further increasing confidence in the reference implementation as well as our deviations from it, we use the C Bounded Model Checker (CBMC) [4] to show absence of out of bounds accesses and carefully track the bounds of arithmetic data, establishing that there are no integer overflows; this currently covers all C code except for pieces of SHA-3, which are work in progress. Experiments are underway to use the HOL-Light/s2n-bignum verification infrastructure [5] for verification at the assembly level (see proofs for SLOTHY-optimized versions of the AArch64 NTT and invNTT by John Harrison here: [6])
All native code is constant-time in the sense that it is free of secret-dependent control flow, memory access, and instructions that are commonly variable-time, thwarting most timing side channels. The C code is hardened against compiler-introduced timing side channels (such as KyberSlash or clangover) through suitable barriers and constant-time patterns.
With mlkem-native v1.0.0-alpha, we invite you to give it a try and let us know what works for you, and what doesn't, as we're working towards a first stable release. Here's the code: https://github.com/pq-code-package/mlkem-native.
Best regards,
Hanno Becker & Matthias Kannwischer
Reply all
Reply to author
Forward
0 new messages