License

mlkem-native (everything under crypto/fipsmodule/ml_kem/mlkem/**) is imported under the Apache 2.0 license. The LICENSE file is updated accordingly.

Integration-specific code (everything with direct parent crypto/fipsmodule/ml_kem/*) is made under the terms of the Apache 2.0 license and the ISC license.

Import mlkem-native

This imports mlkem-native (https://github.com/pq-code-package/mlkem-native, maintained by myself and @mkannwischer) into AWS-LC, replacing the reference implementation.

This PR focuses on the minimal configuration of mlkem-native: No assembly and no FIPS-202 code are imported.

mlkem-native is a high-performance, high-assurance C90 implementation of ML-KEM developed under the Post-Quantum Cryptography Alliance (PQCA) and the Linux Foundation. It is a fork of the reference implementation that AWS-LC previously relied on, and remains close to it. mlkem-native is the default ML-KEM implementation in libOQS.

Import Mechanism

The mlkem-native source code is unmodified and imported using the importer script crypto/fipsmodule/ml_kem/importer.sh; the details of the import are in META.yml.

A custom config is provided for mlkem-native which in particular includes a small 'compatibility layer' between AWS-LC/OpenSSL and mlkem-native -- see below.

Future imports (C-only)

Future updates of the C-only mlkem-native source tree should happen through a re-import of mlkem-native: That is, (a) delete crypto/fipsmodule/ml_kem/mlkem and (b) re-run import.sh. This will re-import mlkem-native/main, though you can set the GITHUB_SHA and GITHUB_REPOSITORY environment variables to point to any other mlkem-native repository/fork.
Temporary ad-hoc changes of crypto/fipsmodule/ml_kem/mlkem/* with accompanying change-log are conceivable as well, similar to how the changes from the reference implementation were documented so far -- but those should be used sparingly and ideally be upstreamed.

Once this PR is merged, we will also merge pq-code-package/mlkem-native#654 into mlkem-native, which adds an integration test doing (a)+(b) above on any PR and checking that the basic AWS-LC build (FIPS and non-FIPS) still works. This way, we will ensure that are no large surprises when AWS-LC wants to re-import a newer version of mlkem-native.

Future imports (native code)

Once we have verified meaningful parts of the mlkem-native assembly backends, PRs will be filed to integrate those. The details for this integration are TBD and not necessary to finalize for this PR. The options I see are (a) extending import.sh to import larger parts of the mlkem-native upstream source tree, including native backends, (b) writing custom backends, backed by sources living in the s2n-bignum source tree. Both is possible and compatible with this PR, and we can discuss nearer the time.

Import Scope

mlkem-native has a C-only version as well as native 'backends' in AVX2 and Neon for high performance. This commit only imports the C-only version. Integration of native backends will be done separately.

mlkem-native offers its own FIPS-202 implementation, including fast versions of batched FIPS-202. However, this commit does not import those, but instead provides glue-code around AWS-LC's own FIPS-202 implementation. The path to leveraging the FIPS-202 performance improvements in mlkem-native would be to integrate them directly
into crypto/fipsmodule/sha.

Impact on build

None. No build-files are modified.

Compatibility layer

The configuration file mlkem_native_config.h includes a compatibility layer between AWS-LC/OpenSSL and mlkem-native, covering:

• FIPS/PCT: If AWSLC_FIPS is set, MLK_KEYGEN_PCT is enabled to include a PCT.
• FIPS/PCT: If BORINGSSL_FIPS_BREAK_TESTS is set, MLK_KEYGEN_PCT_BREAKAGE_TEST is set and mlk_break_pct defined via boringssl_fips_break_test("MLKEM_PWCT"), to include runtime-breakage of the PCT for testing purposes.
• CT: If BORINGSSL_CONSTANT_TIME_VALIDATION is set, then MLK_CT_TESTING_ENABLED is set to enable valgrind testing.
• Zeroization: MLK_CUSTOM_ZEROIZE is set and mlk_zeroize mapped to OPENSSL_cleanse to use OpenSSL's zeroization function.
• Randombytes: MLK_CUSTOM_RANDOMBYTES is set and mlk_randombytes mapped to RAND_bytes to use OpenSSL's zeroization function.

Side-channels

mlkem-native's CI uses a patched version of valgrind to check for various compilers and compile flags that there are no secret-dependent memory accesses, branches, or divisions. The relevant assertions have been kept but are unused unless MLK_CT_TESTING_ENABLED is set, which is the case if and only if BORINGSSL_CONSTANT_TIME_VALIDATION is set.

Similar to AWS-LC, mlkem-native uses value barriers to block potentially harmful compiler reasoning and optimization. Where standard gcc/clang inline assembly is not available, mlkem-native falls back to a slower 'opt blocker' based on a volatile global (an idea we picked up from DjB) -- both is described in verify.h. It will be interesting to see if the opt-blocker variant works on all platforms that AWS-LC cares about.

Formal Verification

All C-code imported in this commit is formally verified using the C Bounded Model Checker (CBMC) to be free of various classes of undefined behaviour, including out-of-bounds memory accesses and arithmetic overflow; the latter is of particular interest for ML-KEM because of the use of lazy modular reduction for improved performance.

The heart of the CBMC proofs are function contract and loop annotations to the C-code. Function contracts are denoted __contract__(...) clauses and occur at the time of declaration, while loop contracts are denoted __loop__ and follow the for statement.

The function contract and loop statements are kept in the source, but removed by the preprocessor so long as the CBMC macro is undefined. Keeping them simplifies the import, and care has been taken to make them readable to the non-expert, and thereby serve as precise documentation of assumptions and guarantees upheld by the code.

The CBMC proofs are automatic and don't require further proofs scripts; yet, they come with their own build system and toolchain dependencies, which this commit does not attempt to import. See proofs/cbmc in the mlkem-native repository. Mid-term, however, CI infrastructure should be setup that allows to import and check the CBMC proofs as part of the AWS-LC CI.

FIPS Compliance

The current reference implementation in AWS-LC accommodates FIPS (IG) requirements via:

• Adding explicit stack buffer via OPENSSL_cleanse
• Adding a Pairwise Consistency Test (PCT) after key generation (only for the FIPS-build)

mlkem-native unconditionally includes stack zeroization. mlkem-native's default secure memset is replaced by OPENSSL_cleanse.

mlkem-native conditionally includes a PCT, guarded by MLK_KEYGEN_PCT. This is set in the config if and only if AWSLC_FIPS is set.

Formatting

Code in crypto/fipsmodule/ml_kem/mlkem is directly imported from mlkem-native and comes with its own crypto/fipsmodule/ml_kem/mlkem/.clang-format.

Prefix build

The prefix build should not be affected by the import, since no definitions of external linkage are imported (everything is tagged either static directly, or MLK_EXTERNAL_API or MLK_INTERNAL_API, both of which are set to static in the context of the import, too).

Performance

It is expected -- but should be checked! -- that the ML-KEM performance with this PR is comparable to that of the reference implementation. This is because the mlkem-native's fast backends are not yet imported, the FIPS-202 code remains that of AWS-LC, and mlkem-native is otherwise close to the reference implementation.

Multilevel build

At the core, mlkem-native is currently a 'single-level' implementation of ML-KEM: A build of the main source tree provides an implementation of exactly one of ML-KEM-512/768/1024, depending on the MLKEM_K parameter. This property is inherited from the ML-KEM reference implementation, while AWS-LC's fork of the reference implementation has changed this behaviour and passes the security level as a runtime parameter.

To build all security levels, level-specific sources are built 3 times, once per security level, and linked with a single build of the level-independent code. The single-compilation-unit approach pursued by AWS-LC makes this process fairly simple since one merely needs to include the single-compilation-unit file provided by mlkem-native three times, and configure it so that the level-independent code is included only once. The final include moreover #undef'ines all macros defined by mlkem-native, reducing the risk of name clashes with other parts of crypto/fipsmodule/bcm.c.

Note that this process is entirely internal to ml_kem.c, and does not affect the AWS-LC build.

Main differences from reference implementation

mlkem-native is a fork of the ML-KEM reference implementation.

The following gives an overview of the major changes:

• CBMC and debug annotations, and minor code restructurings or signature changes to facilitate the CBMC proofs. For example, poly_add(x,a) only comes in a destructive variant to avoid specifying aliasing constraints; poly_rej_uniform has an additional offset parameter indicating the position in the sampling buffer, to avoid passing shifted pointers).
• Introduction of 4x-batched versions of some functions from the reference implementation. This is to leverage 4x-batched Keccak-f1600 implementations if present. The batching happens at the C level even if no native backend for FIPS 202 is present.
• FIPS 203 compliance: Introduced PK (FIPS 203, Section 7.2, 'modulus check') and SK (FIPS 203, Section 7.3, 'hash check') check, as well as optional PCT (FIPS 203, Section 7.1, Pairwise Consistency). Also, introduced zeroization of stack buffers as required by (FIPS 203, Section 3.3, Destruction of intermediate values).
• Introduction of native backend implementations. With the exception of the native backend for poly_rej_uniform(), which may fail and fall back to the C implementation, those are drop-in replacements for the corresponding C functions and dispatched at compile-time.
• Restructuring of files to separate level-specific from level-generic functionality. This is needed to enable a multi-level build of mlkem-native where level-generic code is shared between levels.
• More pervasive use of value barriers to harden constant-time primitives, even when Link-Time-Optimization (LTO) is enabled. The use of LTO can lead to insecure compilation in case of the reference implementation.
• Use of a multiplication cache ('mulcache') structure to simplify and speedup the base multiplication.
• Different placement of modular reductions: We reduce to unsigned canonical representatives in poly_reduce(), and assume such in all polynomial compression functions. The reference implementation works with a signed poly_reduce(), and embeds various signed->unsigned conversions in the compression functions.
• More inlining: Modular multiplication and primitives are in a header rather than a separate compilation unit.