Import mldsa-native #2902
Import mldsa-native #2902
Conversation
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
This comment was marked as duplicate.
This comment was marked as duplicate.
Sorry, something went wrong.
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## main #2902 +/- ##
==========================================
- Coverage 78.19% 78.10% -0.09%
==========================================
Files 685 691 +6
Lines 118074 118641 +567
Branches 16617 16678 +61
==========================================
+ Hits 92330 92670 +340
- Misses 24856 25084 +228
+ Partials 888 887 -1 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
This comment was marked as duplicate.
This comment was marked as duplicate.
Sorry, something went wrong.
This comment was marked as duplicate.
This comment was marked as duplicate.
Sorry, something went wrong.
This comment was marked as duplicate.
This comment was marked as duplicate.
Sorry, something went wrong.
This reverts commit fd8991a.
This comment was marked as duplicate.
This comment was marked as duplicate.
Sorry, something went wrong.
jakemas
force-pushed
the
import-mldsa-native-again
branch
from
2978380 to
07f1b84
Compare
This comment was marked as duplicate.
This comment was marked as duplicate.
Sorry, something went wrong.
This comment was marked as duplicate.
This comment was marked as duplicate.
Sorry, something went wrong.
This comment was marked as duplicate.
This comment was marked as duplicate.
Sorry, something went wrong.
|
Opened awslabs/aws-lc-verification#180 for the SAW proof wrapper function changes. |
2 participants
Issues:
Related PRs:
Import mldsa-native
This imports mldsa-native (https://github.com/pq-code-package/mldsa-native) into AWS-LC.
This PR focuses on the minimal configuration of mldsa-native: No assembly and no FIPS-202 code are imported.
mldsa-native is a high-performance, high-assurance C90 implementation of ML-DSA developed under the Post-Quantum Cryptography Alliance (PQCA) and the Linux Foundation. It is a fork of the Dilithium reference implementation.
Import Mechanism
The mldsa-native source code is unmodified and imported using the importer script
crypto/fipsmodule/ml_dsa/importer.sh;the details of the import are in META.yml.A custom config is provided for mldsa-native which in particular includes a small 'compatibility layer' between AWS-LC/OpenSSL and mldsa-native -- see below.
Future imports (C-only)
Future updates of the C-only mldsa-native source tree should happen through a re-import of mldsa-native: That is, (a) delete
crypto/fipsmodule/ml_dsa/mldsaand (b) re-run import.sh. This will re-importmldsa-native/main, though you can set theGITHUB_SHAandGITHUB_REPOSITORYenvironment variables to point to any other mldsa-native repository/fork.Future imports (native code)
Once we have verified meaningful parts of the mldsa-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 are (a) extending import.sh to import larger parts of the mldsa-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.
Import Scope
mldsa-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.
mldsa-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 mldsa-native would be to integrate them directly into
crypto/fipsmodule/sha.Impact on build
None. No build-files are modified. The multilevel build process remains unchanged.
Compatibility layer
The configuration file
mldsa_native_config.hincludes a compatibility layer between AWS-LC/OpenSSL and mldsa-native, covering:MLD_CONFIG_KEYGEN_PCTis enabled to include a PCT.BORINGSSL_FIPS_BREAK_TESTSis set,MLD_CONFIG_KEYGEN_PCT_BREAKAGE_TESTis set andmld_break_pctdefined viaboringssl_fips_break_test("MLDSA_PWCT"), to include runtime-breakage of the PCT for testing purposes.BORINGSSL_CONSTANT_TIME_VALIDATIONis set, thenMLD_CONFIG_CT_TESTING_ENABLEDis set to enable valgrind testing.MLD_CONFIG_CUSTOM_ZEROIZEis set andmld_zeroizemapped toOPENSSL_cleanseto use OpenSSL's zeroization function.MLD_CONFIG_CUSTOM_RANDOMBYTESis set andmld_randombytesmapped toRAND_bytesto use AWS-LC's randombytes function.Side-channels
mldsa-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
MLD_CONFIG_CT_TESTING_ENABLEDis set, which is the case if and only ifBORINGSSL_CONSTANT_TIME_VALIDATIONis set.mldsa-native uses value barriers to block potentially harmful compiler reasoning and optimization. Where standard gcc/clang inline assembly is not available, mldsa-native falls back to a slower 'opt blocker' based on a volatile global -- both are described in ct.h.
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-DSA 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.
FIPS Compliance
mldsa-native unconditionally includes stack zeroization. mldsa-native's default secure memset is replaced by
OPENSSL_cleanse.mldsa-native conditionally includes a PCT, guarded by
MLD_CONFIG_KEYGEN_PCT. This is set in the config if and only ifAWSLC_FIPSis set.While not part of the FIPS standard, the
pk_from_skfunction includes validation of both t0 (low-order bits) and tr (hash of public key) using constant-time comparison functions (mld_ct_memcmp), providing strong assurance of key consistency.Testing
We KAT ML-DSA with test vectors obtained from https://github.com/post-quantum-cryptography/KAT within
PQDSAParameterTest.KAT. We select the KATs for the signing modehedged, which derives the signing private random seed (rho) pseudorandomly from the signer's private key, the message to be signed, and a 256-bit stringrndwhich is generated at random. Thepurevariant of these KATs were used, as they provide test vector inputs for "pure" i.e., non-pre-hashed messages.We also run the ACVP test vectors obtained from https://github.com/usnistgov/ACVP-Server within the three functions
PerMLDSATest.ACVPKeyGen,PerMLDSATest.ACVPSigGenandPerMLDSATest.ACVPSigVer. These correspond to the tests found at ML-DSA-keyGen-FIPS204, ML-DSA-sigGen-FIPS204, and ML-DSA-sigVer-FIPS204.To test ML-DSA pure, non-deterministic mode, we use
tgId = 19, 21, 23of sigGen andtgId = 7, 9, 11of sigVer.To test ML-DSA ExternalMu, non-deterministic mode, we use
tgId = 20, 22, 24of sigGen andtgId = 8, 10, 12of sigVer.Test Results:
Formatting
Code in
crypto/fipsmodule/ml_dsa/mldsais directly imported from mldsa-native and comes with its owncrypto/fipsmodule/ml_dsa/mldsa/.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
MLD_EXTERNAL_APIorMLD_INTERNAL_API, both of which are set to static in the context of the import, too).Performance
Performance should be comparable to the previous integration as both are based on C-only code with AWS-LC's FIPS-202 implementation. The fast mldsa-native backends are not yet imported.
Multilevel build
At the core, mldsa-native is currently a 'single-level' implementation of ML-DSA: A build of the main source tree provides an implementation of exactly one of ML-DSA-44/65/87, depending on the
MLD_CONFIG_PARAMETER_SETparameter.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 mldsa-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 mldsa-native, reducing the risk of name clashes with other parts of
crypto/fipsmodule/bcm.c.Note that this process is entirely internal to ml_dsa.c, and does not affect the AWS-LC build.
HashML-DSA: mldsa-native includes lots of HashML-DSA functionality that we dont need in aws-lc. Perhaps we should add config upstream to mldsa-native to choose which of pure/externalmu/hash modes are imported to reduce unused code.
Main differences from reference implementation
mldsa-native is a fork of the ML-DSA reference implementation (Dilithium).
The following gives an overview of the major changes:
License
mldsa-native (everything under
crypto/fipsmodule/ml_dsa/mldsa/**) is imported under the Apache 2.0 license and the ISC license. The LICENSE file remains unchanged.Integration-specific code (everything with direct parent
crypto/fipsmodule/ml_dsa/*) is made under the terms of the Apache 2.0 license and the ISC license.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license and the ISC license.