Import mlkem-native #2176
Open
Import mlkem-native #2176
+7,481
−2,251
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #2176 +/- ##
==========================================
+ Coverage 79.05% 79.07% +0.02%
==========================================
Files 612 615 +3
Lines 106476 106624 +148
Branches 15050 15047 -3
==========================================
+ Hits 84174 84314 +140
- Misses 21650 21657 +7
- Partials 652 653 +1 ☔ View full report in Codecov by Sentry. |
jakemas
reviewed
Feb 13, 2025
hanno-becker
force-pushed
the
mlkem_native_pr
branch
3 times, most recently
from
5c55792 to
e6bada0
Compare
|
|
hanno-becker
force-pushed
the
mlkem_native_pr
branch
3 times, most recently
from
abf6a67 to
f81cb51
Compare
hanno-becker
force-pushed
the
mlkem_native_pr
branch
2 times, most recently
from
7f0f3f8 to
3a3b631
Compare
| #define mlk_shake128ctx KECCAK1600_CTX | ||
|
|
||
| static MLK_INLINE void mlk_shake128_init(mlk_shake128ctx *state) | ||
| { |
There was a problem hiding this comment.
Please see coding style in rest of repository. Mainly, no newline for starting block and use // for coding style.
I think everything under mlkem could be excluded from clang-format.
There was a problem hiding this comment.
At least, AFAIU, only code under mlkem is imported from upstream.
There was a problem hiding this comment.
Yes, everything in ml_kem/mlkem/* comes directly from upstream, and I would prefer not to touch it. It has its own clang-format which could be imported to stop clang-format from messing with it (which it will, by default, because of the CBMC annotations).
Code in mlkem/* is glue-code specific to AWS-LC and can be formatted as usual, so I'll adjust as you suggest.
There was a problem hiding this comment.
Added mlkem-native's .clang-format to the importer.
| // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
| // SPDX-License-Identifier: Apache-2.0 OR ISC | ||
|
|
||
| /* |
There was a problem hiding this comment.
Same coding style comments.
| # upstream repository (for example, to your fork of mlkem-native), use | ||
| # | ||
| # ``` | ||
| # GITHUB_REPOSITORY={YOUR REPOSITORY} GITHUB_SHA={COMMIT_HASH} ./import.sh |
There was a problem hiding this comment.
you don't have releases in mlkem-native?
There was a problem hiding this comment.
Yes, we do -- why are you asking? You can use a tag or a hash here.
crypto/fipsmodule/ml_kem/ml_kem.c
Outdated
| @@ -1,27 +1,37 @@ | |||
| // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | |||
| // SPDX-License-Identifier: Apache-2.0 OR ISC | |||
|
|
|||
| /* mlkem-native source code */ | |||
crypto/fipsmodule/ml_kem/ml_kem.c
Outdated
| #include "./ml_kem.h" | ||
| #include "openssl/rand.h" |
There was a problem hiding this comment.
Suggested change
| #include "openssl/rand.h" | |
| #include <openssl/rand.h> |
hanno-becker
force-pushed
the
mlkem_native_pr
branch
3 times, most recently
from
589ad85 to
1c43e38
Compare
This commit removes the reference implementation of ML-KEM from the source tree, in preparation for the integration of mlkem-native. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
This imports mlkem-native (https://github.com/pq-code-package/mlkem-native) into AWS-LC, replacing the reference implementation. This commit 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](https://github.com/open-quantum-safe/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. Future updates to the source tree would ideally happen through a re-import of a different version of mlkem-native, though a temporary change-log is conceivable, similar to how the changes from the reference implementation were documented so far. **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](crytpo/fipsmodule/sha). **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 by DjB) -- both is described in [verify.h](https://github.com/aws/aws-lc/blob/df5b09029e27d54b2b117eeddb6abd983528ae15/crypto/fipsmodule/ml_kem/mlkem/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](https://github.com/diffblue/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](https://github.com/pq-code-package/mlkem-native/tree/main/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. **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. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
This commit updates the LICENSE file to indicate that mlkem-native is distributed under Apache 2.0. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
hanno-becker
force-pushed
the
mlkem_native_pr
branch
from
1c43e38 to
09ad19e
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
License
mlkem-native (everything under
crypto/fipsmodule/ml_kem/mlkem/**) is imported under the Apache 2.0 license (only). 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.
Goal
The goal is for this PR to be a driver for discussion and flushing out of technical issues, and that it be merged as a first step towards integrating mlkem-native, followed by the integration of (hopefully then-verified) native backends in AArch64 and AVX2 later in 2025.
Todos
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/mlkemand (b) re-runimport.sh. This will re-importmlkem-native/main, though you can set theGITHUB_SHAandGITHUB_REPOSITORYenvironment 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.shto 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.hincludes a compatibility layer between AWS-LC/OpenSSL and mlkem-native, covering:AWSLC_FIPSis set,MLK_KEYGEN_PCTis enabled to include a PCT.BORINGSSL_FIPS_BREAK_TESTSis set,MLK_KEYGEN_PCT_BREAKAGE_TESTis set andmlk_break_pctdefined viaboringssl_fips_break_test("MLKEM_PWCT"), to include runtime-breakage of the PCT for testing purposes.BORINGSSL_CONSTANT_TIME_VALIDATIONis set, thenMLK_CT_TESTING_ENABLEDis set to enable valgrind testing.MLK_USE_CT_ZEROIZE_NATIVEis set andct_zeroize_nativemapped toOPENSSL_cleanseto 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_ENABLEDis set, which is the case if and only ifBORINGSSL_CONSTANT_TIME_VALIDATIONis 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 theforstatement.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:
OPENSSL_cleansemlkem-native unconditionally includes stack zeroization. mlkem-native's default secure
memsetis replaced byOPENSSL_cleanse.mlkem-native conditionally includes a PCT, guarded by
MLK_KEYGEN_PCT. This is set in the config if and only ifAWSLC_FIPSis set.Formatting
Code in
crypto/fipsmodule/ml_kem/mlkemis directly imported from mlkem-native and comes with its owncrypto/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
staticdirectly, orMLK_EXTERNAL_APIorMLK_INTERNAL_API, both of which are set tostaticin 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:
poly_add(x,a)only comes in a destructive variant to avoid specifying aliasing constraints;poly_rej_uniformhas an additionaloffsetparameter indicating the position in the sampling buffer, to avoid passing shifted pointers).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.poly_reduce(), and assume such in all polynomial compression functions. The reference implementation works with a signedpoly_reduce(), and embeds various signed->unsigned conversions in the compression functions.