From 80d95d517b94353b6c2ac2ca304f251f10cfb686 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Sun, 14 Jun 2026 21:24:40 +0800 Subject: [PATCH 1/2] Add ML-KEM Braid API Split K-PKE.Encrypt and ML-KEM.Encaps into two phases (u and v) to support protocols like MLKEMBraid that transmit large KEM components in parallel over bandwidth-constrained channels. CPA level (indcpa): - mlk_indcpa_enc_u: computes ct_u from ek_seed, outputs intermediate state (sp, epp, sp_cache) - mlk_indcpa_enc_v: computes ct_v from ek_vector using intermediate state from enc_u CCA KEM level (kem): - mlk_kem_enc_derand_u: FO transform + enc_u, outputs shared secret and intermediate state; only needs ek_seed and H(pk) - mlk_kem_enc_v: modulus check on ek_vector + enc_v; only needs ek_vector epp is serialized as 4-bit nibbles (ETA2 - x) to provide a natural coefficient bound on deserialization; sp is serialized as 16-bit LE. The shared sp mulcache is computed once and threaded through enc_u/enc_v. Includes CBMC contracts and proofs for the new functions, the MLK_CONFIG_ENABLE_MLKEM_BRAID configuration option exposing the API, recomputed peak stack consumption values, and OpenTitan work buffer size updates. The test verifies that the incremental API produces identical ciphertexts and shared secrets as the standard API across all three parameter sets. Co-authored-by: Hanno Becker Signed-off-by: Matthias J. Kannwischer Signed-off-by: Rod Chapman --- .github/actions/config-variations/action.yml | 17 +- .github/workflows/integration-pavona.yml | 5 + BIBLIOGRAPHY.md | 2 + .../mlkem_native/mlkem_native_config.h | 10 + .../mlkem_native/mlkem_native_config.h | 10 + .../mlkem_native/mlkem_native_config.h | 10 + .../mlkem_native/mlkem_native_config.h | 10 + .../mlkem_native/mlkem_native_config.h | 10 + .../mlkem_native/mlkem_native_config.h | 10 + .../Makefile | 1 + .../mlkem_native/mlkem_native_config.h | 10 + .../mlkem_native/mlkem_native_config.h | 10 + .../mlkem_native/mlkem_native_config.h | 10 + .../mlkem_native/mlkem_native_config.h | 10 + integration/pavona/update-alloc-sizes.patch | 27 + mlkem/mlkem_native.c | 10 + mlkem/mlkem_native.h | 18 +- mlkem/mlkem_native_asm.S | 10 + mlkem/mlkem_native_config.h | 10 + mlkem/src/common.h | 12 + mlkem/src/indcpa.c | 254 +++---- mlkem/src/indcpa.h | 98 +++ mlkem/src/kem.c | 230 ++++++ mlkem/src/kem.h | 136 ++++ proofs/cbmc/deserialize_epp/Makefile | 36 + .../deserialize_epp/deserialize_epp_harness.c | 21 + proofs/cbmc/deserialize_polyvec_16le/Makefile | 36 + .../deserialize_polyvec_16le_harness.c | 22 + proofs/cbmc/enc_getnoise_eta1_eta2/Makefile | 66 -- .../enc_getnoise_eta1_eta2_harness.c | 23 - proofs/cbmc/indcpa_enc/Makefile | 24 +- proofs/cbmc/indcpa_enc_u/Makefile | 54 ++ .../cbmc/indcpa_enc_u/indcpa_enc_u_harness.c | 16 + proofs/cbmc/indcpa_enc_v/Makefile | 44 ++ .../cbmc/indcpa_enc_v/indcpa_enc_v_harness.c | 16 + proofs/cbmc/kem_enc_derand_u/Makefile | 41 ++ .../kem_enc_derand_u_harness.c | 12 + proofs/cbmc/kem_enc_v/Makefile | 44 ++ proofs/cbmc/kem_enc_v/kem_enc_v_harness.c | 12 + proofs/cbmc/mlkem_native_config_cbmc.h | 10 + proofs/cbmc/serialize_epp/Makefile | 36 + .../serialize_epp/serialize_epp_harness.c | 21 + proofs/cbmc/serialize_polyvec_16le/Makefile | 36 + .../serialize_polyvec_16le_harness.c | 22 + test/configs/break_pct_config.h | 10 + test/configs/configs.yml | 8 + test/configs/custom_heap_alloc_config.h | 10 + test/configs/custom_memcpy_config.h | 10 + test/configs/custom_memset_config.h | 10 + .../custom_native_capability_config_0.h | 10 + .../custom_native_capability_config_1.h | 10 + ...stom_native_capability_config_CPUID_AVX2.h | 10 + ...native_capability_config_ID_AA64PFR1_EL1.h | 10 + test/configs/custom_randombytes_config.h | 10 + test/configs/custom_stdlib_config.h | 10 + test/configs/custom_zeroize_config.h | 10 + test/configs/no_asm_config.h | 10 + test/configs/serial_fips202_config.h | 10 + test/configs/test_alloc_config.h | 10 + test/configs/test_mlkem_braid_config.h | 670 ++++++++++++++++++ test/src/test_mlkem.c | 204 ++++-- 61 files changed, 2228 insertions(+), 316 deletions(-) create mode 100644 integration/pavona/update-alloc-sizes.patch create mode 100644 proofs/cbmc/deserialize_epp/Makefile create mode 100644 proofs/cbmc/deserialize_epp/deserialize_epp_harness.c create mode 100644 proofs/cbmc/deserialize_polyvec_16le/Makefile create mode 100644 proofs/cbmc/deserialize_polyvec_16le/deserialize_polyvec_16le_harness.c delete mode 100644 proofs/cbmc/enc_getnoise_eta1_eta2/Makefile delete mode 100644 proofs/cbmc/enc_getnoise_eta1_eta2/enc_getnoise_eta1_eta2_harness.c create mode 100644 proofs/cbmc/indcpa_enc_u/Makefile create mode 100644 proofs/cbmc/indcpa_enc_u/indcpa_enc_u_harness.c create mode 100644 proofs/cbmc/indcpa_enc_v/Makefile create mode 100644 proofs/cbmc/indcpa_enc_v/indcpa_enc_v_harness.c create mode 100644 proofs/cbmc/kem_enc_derand_u/Makefile create mode 100644 proofs/cbmc/kem_enc_derand_u/kem_enc_derand_u_harness.c create mode 100644 proofs/cbmc/kem_enc_v/Makefile create mode 100644 proofs/cbmc/kem_enc_v/kem_enc_v_harness.c create mode 100644 proofs/cbmc/serialize_epp/Makefile create mode 100644 proofs/cbmc/serialize_epp/serialize_epp_harness.c create mode 100644 proofs/cbmc/serialize_polyvec_16le/Makefile create mode 100644 proofs/cbmc/serialize_polyvec_16le/serialize_polyvec_16le_harness.c create mode 100644 test/configs/test_mlkem_braid_config.h diff --git a/.github/actions/config-variations/action.yml b/.github/actions/config-variations/action.yml index b776d605f9..3966a33c1d 100644 --- a/.github/actions/config-variations/action.yml +++ b/.github/actions/config-variations/action.yml @@ -11,7 +11,7 @@ inputs: description: 'List of tests to run (space-separated IDs) or "all" for all tests. Available IDs: pct-enabled, pct-enabled-broken, custom-alloc-heap, custom-zeroize, native-cap-ON, native-cap-OFF, native-cap-ID_AA64PFR1_EL1, native-cap-CPUID_AVX2, no-asm, serial-fips202, custom-randombytes, custom-memcpy, custom-memset, custom-stdlib, - nblocks-1, nblocks-2, nblocks-4' + mlkem-braid, nblocks-1, nblocks-2, nblocks-4' required: false default: 'all' opt: @@ -231,6 +231,21 @@ runs: examples: false # Some examples use a custom config themselves alloc: false # Requires custom config rng_fail: true + - name: "ML-KEM Braid (incremental encapsulation API)" + if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'mlkem-braid') }} + uses: ./.github/actions/multi-functest + with: + gh_token: ${{ inputs.gh_token }} + compile_mode: native + cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLK_CONFIG_FILE=\\\\\\\"configs/test_mlkem_braid_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + func: true + kat: true + acvp: true + opt: ${{ inputs.opt }} + examples: false + alloc: false + rng_fail: true - name: "MLKEM_GEN_MATRIX_NBLOCKS=1" if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'nblocks-1') }} uses: ./.github/actions/multi-functest diff --git a/.github/workflows/integration-pavona.yml b/.github/workflows/integration-pavona.yml index f6e06f5714..770a7b37ff 100644 --- a/.github/workflows/integration-pavona.yml +++ b/.github/workflows/integration-pavona.yml @@ -79,6 +79,11 @@ jobs: echo "=== Patched extensions.bzl ===" cat third_party/mlkem_native/extensions.bzl + - name: Update work buffer sizes + run: | + cd "$PAVONA_DIR" + git apply "$GITHUB_WORKSPACE/integration/pavona/update-alloc-sizes.patch" + - name: Patch functest to only test deterministic API run: | cd "$PAVONA_DIR" diff --git a/BIBLIOGRAPHY.md b/BIBLIOGRAPHY.md index e1249b2e57..a53513033a 100644 --- a/BIBLIOGRAPHY.md +++ b/BIBLIOGRAPHY.md @@ -91,6 +91,7 @@ source code and documentation. - [test/configs/no_asm_config.h](test/configs/no_asm_config.h) - [test/configs/serial_fips202_config.h](test/configs/serial_fips202_config.h) - [test/configs/test_alloc_config.h](test/configs/test_alloc_config.h) + - [test/configs/test_mlkem_braid_config.h](test/configs/test_mlkem_braid_config.h) ### `FIPS202` @@ -154,6 +155,7 @@ source code and documentation. - [test/configs/no_asm_config.h](test/configs/no_asm_config.h) - [test/configs/serial_fips202_config.h](test/configs/serial_fips202_config.h) - [test/configs/test_alloc_config.h](test/configs/test_alloc_config.h) + - [test/configs/test_mlkem_braid_config.h](test/configs/test_mlkem_braid_config.h) ### `HOL-Light` diff --git a/examples/basic_deterministic/mlkem_native/mlkem_native_config.h b/examples/basic_deterministic/mlkem_native/mlkem_native_config.h index 8c072921ff..d5c9f63a36 100644 --- a/examples/basic_deterministic/mlkem_native/mlkem_native_config.h +++ b/examples/basic_deterministic/mlkem_native/mlkem_native_config.h @@ -152,6 +152,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/examples/bring_your_own_fips202/mlkem_native/mlkem_native_config.h b/examples/bring_your_own_fips202/mlkem_native/mlkem_native_config.h index 31333aa667..23bf3bf1af 100644 --- a/examples/bring_your_own_fips202/mlkem_native/mlkem_native_config.h +++ b/examples/bring_your_own_fips202/mlkem_native/mlkem_native_config.h @@ -152,6 +152,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/examples/bring_your_own_fips202_static/mlkem_native/mlkem_native_config.h b/examples/bring_your_own_fips202_static/mlkem_native/mlkem_native_config.h index 85adffa9b8..1325b513c9 100644 --- a/examples/bring_your_own_fips202_static/mlkem_native/mlkem_native_config.h +++ b/examples/bring_your_own_fips202_static/mlkem_native/mlkem_native_config.h @@ -153,6 +153,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/examples/custom_backend/mlkem_native/mlkem_native_config.h b/examples/custom_backend/mlkem_native/mlkem_native_config.h index 9598cdc3e0..3c2f48b8c9 100644 --- a/examples/custom_backend/mlkem_native/mlkem_native_config.h +++ b/examples/custom_backend/mlkem_native/mlkem_native_config.h @@ -154,6 +154,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/examples/monolithic_build/mlkem_native/mlkem_native_config.h b/examples/monolithic_build/mlkem_native/mlkem_native_config.h index 619c176b76..f7a9318490 100644 --- a/examples/monolithic_build/mlkem_native/mlkem_native_config.h +++ b/examples/monolithic_build/mlkem_native/mlkem_native_config.h @@ -151,6 +151,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/examples/monolithic_build_multilevel/mlkem_native/mlkem_native_config.h b/examples/monolithic_build_multilevel/mlkem_native/mlkem_native_config.h index 6be461e4d6..41add6b63f 100644 --- a/examples/monolithic_build_multilevel/mlkem_native/mlkem_native_config.h +++ b/examples/monolithic_build_multilevel/mlkem_native/mlkem_native_config.h @@ -153,6 +153,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/examples/monolithic_build_multilevel_native/Makefile b/examples/monolithic_build_multilevel_native/Makefile index 3853806d2f..ad3aa37cb6 100644 --- a/examples/monolithic_build_multilevel_native/Makefile +++ b/examples/monolithic_build_multilevel_native/Makefile @@ -23,6 +23,7 @@ CFLAGS := \ -Wno-long-long \ -Wno-unknown-pragmas \ -Wno-unused-command-line-argument \ + -Wno-unused-function \ -O3 \ -fomit-frame-pointer \ -std=c99 \ diff --git a/examples/monolithic_build_multilevel_native/mlkem_native/mlkem_native_config.h b/examples/monolithic_build_multilevel_native/mlkem_native/mlkem_native_config.h index ac478b2bab..4f2eb38dc8 100644 --- a/examples/monolithic_build_multilevel_native/mlkem_native/mlkem_native_config.h +++ b/examples/monolithic_build_multilevel_native/mlkem_native/mlkem_native_config.h @@ -157,6 +157,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/examples/monolithic_build_native/mlkem_native/mlkem_native_config.h b/examples/monolithic_build_native/mlkem_native/mlkem_native_config.h index 7b731cd6a1..33afaf21df 100644 --- a/examples/monolithic_build_native/mlkem_native/mlkem_native_config.h +++ b/examples/monolithic_build_native/mlkem_native/mlkem_native_config.h @@ -151,6 +151,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/examples/multilevel_build/mlkem_native/mlkem_native_config.h b/examples/multilevel_build/mlkem_native/mlkem_native_config.h index d5474ad777..9edc26a5e0 100644 --- a/examples/multilevel_build/mlkem_native/mlkem_native_config.h +++ b/examples/multilevel_build/mlkem_native/mlkem_native_config.h @@ -152,6 +152,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/examples/multilevel_build_native/mlkem_native/mlkem_native_config.h b/examples/multilevel_build_native/mlkem_native/mlkem_native_config.h index 2a0467f096..7bc877a80f 100644 --- a/examples/multilevel_build_native/mlkem_native/mlkem_native_config.h +++ b/examples/multilevel_build_native/mlkem_native/mlkem_native_config.h @@ -154,6 +154,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/integration/pavona/update-alloc-sizes.patch b/integration/pavona/update-alloc-sizes.patch new file mode 100644 index 0000000000..a830f16dd9 --- /dev/null +++ b/integration/pavona/update-alloc-sizes.patch @@ -0,0 +1,27 @@ +diff --git a/sw/device/lib/crypto/include/mlkem.h b/sw/device/lib/crypto/include/mlkem.h +index ee8c531..00f0887 100644 +--- a/sw/device/lib/crypto/include/mlkem.h ++++ b/sw/device/lib/crypto/include/mlkem.h +@@ -33,16 +33,16 @@ enum { + + // Work buffer sizes in 32-bit words + kOtcryptoMlkem512WorkBufferKeypairWords = 5824 / sizeof(uint32_t), +- kOtcryptoMlkem512WorkBufferEncapsWords = 8384 / sizeof(uint32_t), +- kOtcryptoMlkem512WorkBufferDecapsWords = 9152 / sizeof(uint32_t), ++ kOtcryptoMlkem512WorkBufferEncapsWords = 6304 / sizeof(uint32_t), ++ kOtcryptoMlkem512WorkBufferDecapsWords = 7072 / sizeof(uint32_t), + + kOtcryptoMlkem768WorkBufferKeypairWords = 10176 / sizeof(uint32_t), +- kOtcryptoMlkem768WorkBufferEncapsWords = 13248 / sizeof(uint32_t), +- kOtcryptoMlkem768WorkBufferDecapsWords = 14336 / sizeof(uint32_t), ++ kOtcryptoMlkem768WorkBufferEncapsWords = 10656 / sizeof(uint32_t), ++ kOtcryptoMlkem768WorkBufferDecapsWords = 11744 / sizeof(uint32_t), + + kOtcryptoMlkem1024WorkBufferKeypairWords = 15552 / sizeof(uint32_t), +- kOtcryptoMlkem1024WorkBufferEncapsWords = 19136 / sizeof(uint32_t), +- kOtcryptoMlkem1024WorkBufferDecapsWords = 20704 / sizeof(uint32_t), ++ kOtcryptoMlkem1024WorkBufferEncapsWords = 16032 / sizeof(uint32_t), ++ kOtcryptoMlkem1024WorkBufferDecapsWords = 17600 / sizeof(uint32_t), + }; + + /** diff --git a/mlkem/mlkem_native.c b/mlkem/mlkem_native.c index d8b0fd5398..03d33d97d9 100644 --- a/mlkem/mlkem_native.c +++ b/mlkem/mlkem_native.c @@ -207,6 +207,9 @@ #undef MLK_CONTEXT_PARAMETERS_2 #undef MLK_CONTEXT_PARAMETERS_3 #undef MLK_CONTEXT_PARAMETERS_4 +#undef MLK_CONTEXT_PARAMETERS_5 +#undef MLK_CONTEXT_PARAMETERS_6 +#undef MLK_CONTEXT_PARAMETERS_7 #undef MLK_EMPTY_CU #undef MLK_ERR_FAIL #undef MLK_ERR_OUT_OF_MEMORY @@ -229,14 +232,21 @@ #undef mlk_gen_matrix #undef mlk_indcpa_dec #undef mlk_indcpa_enc +#undef mlk_indcpa_enc_u +#undef mlk_indcpa_enc_v #undef mlk_indcpa_keypair_derand /* mlkem/src/kem.h */ +#undef MLKEM_EPP_BYTES +#undef MLKEM_POLY16_BYTES +#undef MLKEM_POLYVEC16_BYTES #undef MLK_KEM_H #undef mlk_kem_check_pk #undef mlk_kem_check_sk #undef mlk_kem_dec #undef mlk_kem_enc #undef mlk_kem_enc_derand +#undef mlk_kem_enc_derand_u +#undef mlk_kem_enc_v #undef mlk_kem_keypair #undef mlk_kem_keypair_derand /* mlkem/src/params.h */ diff --git a/mlkem/mlkem_native.h b/mlkem/mlkem_native.h index 9bbb3e2d52..839c4280da 100644 --- a/mlkem/mlkem_native.h +++ b/mlkem/mlkem_native.h @@ -477,17 +477,17 @@ int MLK_API_NAMESPACE(check_sk)( */ /* check-magic: off */ #define MLK_TOTAL_ALLOC_512_KEYPAIR_NO_PCT 5824 -#define MLK_TOTAL_ALLOC_512_KEYPAIR_PCT 10048 -#define MLK_TOTAL_ALLOC_512_ENCAPS 8384 -#define MLK_TOTAL_ALLOC_512_DECAPS 9152 +#define MLK_TOTAL_ALLOC_512_KEYPAIR_PCT 7968 +#define MLK_TOTAL_ALLOC_512_ENCAPS 6304 +#define MLK_TOTAL_ALLOC_512_DECAPS 7072 #define MLK_TOTAL_ALLOC_768_KEYPAIR_NO_PCT 10176 -#define MLK_TOTAL_ALLOC_768_KEYPAIR_PCT 15552 -#define MLK_TOTAL_ALLOC_768_ENCAPS 13248 -#define MLK_TOTAL_ALLOC_768_DECAPS 14336 +#define MLK_TOTAL_ALLOC_768_KEYPAIR_PCT 12960 +#define MLK_TOTAL_ALLOC_768_ENCAPS 10656 +#define MLK_TOTAL_ALLOC_768_DECAPS 11744 #define MLK_TOTAL_ALLOC_1024_KEYPAIR_NO_PCT 15552 -#define MLK_TOTAL_ALLOC_1024_KEYPAIR_PCT 22400 -#define MLK_TOTAL_ALLOC_1024_ENCAPS 19136 -#define MLK_TOTAL_ALLOC_1024_DECAPS 20704 +#define MLK_TOTAL_ALLOC_1024_KEYPAIR_PCT 19296 +#define MLK_TOTAL_ALLOC_1024_ENCAPS 16032 +#define MLK_TOTAL_ALLOC_1024_DECAPS 17600 /* check-magic: on */ /* diff --git a/mlkem/mlkem_native_asm.S b/mlkem/mlkem_native_asm.S index c2edd2b161..2c7aadd84c 100644 --- a/mlkem/mlkem_native_asm.S +++ b/mlkem/mlkem_native_asm.S @@ -231,6 +231,9 @@ #undef MLK_CONTEXT_PARAMETERS_2 #undef MLK_CONTEXT_PARAMETERS_3 #undef MLK_CONTEXT_PARAMETERS_4 +#undef MLK_CONTEXT_PARAMETERS_5 +#undef MLK_CONTEXT_PARAMETERS_6 +#undef MLK_CONTEXT_PARAMETERS_7 #undef MLK_EMPTY_CU #undef MLK_ERR_FAIL #undef MLK_ERR_OUT_OF_MEMORY @@ -253,14 +256,21 @@ #undef mlk_gen_matrix #undef mlk_indcpa_dec #undef mlk_indcpa_enc +#undef mlk_indcpa_enc_u +#undef mlk_indcpa_enc_v #undef mlk_indcpa_keypair_derand /* mlkem/src/kem.h */ +#undef MLKEM_EPP_BYTES +#undef MLKEM_POLY16_BYTES +#undef MLKEM_POLYVEC16_BYTES #undef MLK_KEM_H #undef mlk_kem_check_pk #undef mlk_kem_check_sk #undef mlk_kem_dec #undef mlk_kem_enc #undef mlk_kem_enc_derand +#undef mlk_kem_enc_derand_u +#undef mlk_kem_enc_v #undef mlk_kem_keypair #undef mlk_kem_keypair_derand /* mlkem/src/params.h */ diff --git a/mlkem/mlkem_native_config.h b/mlkem/mlkem_native_config.h index e9e5b12df9..8b2a907abe 100644 --- a/mlkem/mlkem_native_config.h +++ b/mlkem/mlkem_native_config.h @@ -136,6 +136,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/mlkem/src/common.h b/mlkem/src/common.h index 463029bde9..cc4b10a850 100644 --- a/mlkem/src/common.h +++ b/mlkem/src/common.h @@ -205,6 +205,12 @@ (arg0, arg1, arg2, context) #define MLK_CONTEXT_PARAMETERS_4(arg0, arg1, arg2, arg3, context) \ (arg0, arg1, arg2, arg3, context) +#define MLK_CONTEXT_PARAMETERS_5(arg0, arg1, arg2, arg3, arg4, context) \ + (arg0, arg1, arg2, arg3, arg4, context) +#define MLK_CONTEXT_PARAMETERS_6(a0, a1, a2, a3, a4, a5, context) \ + (a0, a1, a2, a3, a4, a5, context) +#define MLK_CONTEXT_PARAMETERS_7(a0, a1, a2, a3, a4, a5, a6, context) \ + (a0, a1, a2, a3, a4, a5, a6, context) #else /* MLK_CONFIG_CONTEXT_PARAMETER */ #define MLK_CONTEXT_PARAMETERS_0(context) () #define MLK_CONTEXT_PARAMETERS_1(arg0, context) (arg0) @@ -212,6 +218,12 @@ #define MLK_CONTEXT_PARAMETERS_3(arg0, arg1, arg2, context) (arg0, arg1, arg2) #define MLK_CONTEXT_PARAMETERS_4(arg0, arg1, arg2, arg3, context) \ (arg0, arg1, arg2, arg3) +#define MLK_CONTEXT_PARAMETERS_5(arg0, arg1, arg2, arg3, arg4, context) \ + (arg0, arg1, arg2, arg3, arg4) +#define MLK_CONTEXT_PARAMETERS_6(a0, a1, a2, a3, a4, a5, context) \ + (a0, a1, a2, a3, a4, a5) +#define MLK_CONTEXT_PARAMETERS_7(a0, a1, a2, a3, a4, a5, a6, context) \ + (a0, a1, a2, a3, a4, a5, a6) #endif /* !MLK_CONFIG_CONTEXT_PARAMETER */ #if defined(MLK_CONFIG_CONTEXT_PARAMETER_TYPE) != \ diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index 50d2b92c0f..5d840c6521 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -30,10 +30,8 @@ * of mlkem-native (e.g. with varying parameter sets) * within a single compilation unit. */ #define mlk_pack_pk MLK_ADD_PARAM_SET(mlk_pack_pk) -#define mlk_unpack_pk MLK_ADD_PARAM_SET(mlk_unpack_pk) #define mlk_pack_sk MLK_ADD_PARAM_SET(mlk_pack_sk) #define mlk_unpack_sk MLK_ADD_PARAM_SET(mlk_unpack_sk) -#define mlk_pack_ciphertext MLK_ADD_PARAM_SET(mlk_pack_ciphertext) #define mlk_unpack_ciphertext MLK_ADD_PARAM_SET(mlk_unpack_ciphertext) #define mlk_matvec_mul MLK_ADD_PARAM_SET(mlk_matvec_mul) #define mlk_polyvec_permute_bitrev_to_custom \ @@ -41,7 +39,6 @@ #define mlk_polymat_permute_bitrev_to_custom \ MLK_ADD_PARAM_SET(mlk_polymat_permute_bitrev_to_custom) #define mlk_keypair_getnoise_eta1 MLK_ADD_PARAM_SET(mlk_keypair_getnoise_eta1) -#define mlk_enc_getnoise_eta1_eta2 MLK_ADD_PARAM_SET(mlk_enc_getnoise_eta1_eta2) /* End of parameter set namespacing */ /** @@ -64,29 +61,6 @@ static void mlk_pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], mlk_memcpy(r + MLKEM_POLYVECBYTES, seed, MLKEM_SYMBYTES); } -/** - * De-serialize public key from a byte array; approximate inverse of - * mlk_pack_pk. - * - * @spec{Implements @[FIPS203, Algorithm 14 (K-PKE.Encrypt), L2-3].} - * - * @param[out] pk Output public-key polynomial vector. Coefficients - * will be normalized to [0,1,..,MLKEM_Q-1]. - * @param[out] seed Output seed to generate matrix A. - * @param[in] packedpk Input serialized public key. - */ -static void mlk_unpack_pk(mlk_polyvec *pk, uint8_t seed[MLKEM_SYMBYTES], - const uint8_t packedpk[MLKEM_INDCPA_PUBLICKEYBYTES]) -{ - mlk_polyvec_frombytes(pk, packedpk); - mlk_memcpy(seed, packedpk + MLKEM_POLYVECBYTES, MLKEM_SYMBYTES); - - /* NOTE: If a modulus check was conducted on the PK, we know at this - * point that the coefficients of `pk` are unsigned canonical. The - * specifications and proofs, however, do _not_ assume this, and instead - * work with the easily provable bound by MLKEM_UINT12_LIMIT. */ -} - /** * Serialize the secret key. * @@ -116,24 +90,6 @@ static void mlk_unpack_sk(mlk_polyvec *sk, mlk_polyvec_frombytes(sk, packedsk); } -/** - * Serialize the ciphertext as the concatenation of the compressed and - * serialized vector of polynomials b and the compressed and serialized - * polynomial v. - * - * @spec{Implements @[FIPS203, Algorithm 14 (K-PKE.Encrypt), L22-23].} - * - * @param[out] r Output serialized ciphertext. - * @param[in] b Input vector of polynomials b. - * @param[in] v Input polynomial v. - */ -static void mlk_pack_ciphertext(uint8_t r[MLKEM_INDCPA_BYTES], - const mlk_polyvec *b, mlk_poly *v) -{ - mlk_polyvec_compress_du(r, b); - mlk_poly_compress_dv(r + MLKEM_POLYVECCOMPRESSEDBYTES_DU, v); -} - /** * De-serialize and decompress ciphertext from a byte array; approximate * inverse of mlk_pack_ciphertext. @@ -379,58 +335,6 @@ __contract__( #endif /* MLKEM_K == 4 */ } -/** - * Compute and fill the sp, ep, and epp polynomial structures needed by - * mlk_indcpa_enc(). Uses x4-batched versions of `poly_getnoise` to leverage - * batched Keccak-f1600. - * - * @spec{Implements @[FIPS203, Algorithm 14 (K-PKE.Encrypt)] steps 9-16.} - * - * @param[out] sp Output polynomial vector. - * @param[out] ep Output polynomial vector. - * @param[out] epp Output polynomial. - * @param[in] coins Seed bytes for sampling. - */ -static void mlk_enc_getnoise_eta1_eta2(mlk_polyvec *sp, mlk_polyvec *ep, - mlk_poly *epp, - const uint8_t coins[MLKEM_SYMBYTES]) -__contract__( - requires(memory_no_alias(sp, sizeof(mlk_polyvec))) - requires(memory_no_alias(ep, sizeof(mlk_polyvec))) - requires(memory_no_alias(epp, sizeof(mlk_poly))) - requires(memory_no_alias(coins, MLKEM_SYMBYTES)) - assigns(memory_slice(sp, sizeof(mlk_polyvec))) - assigns(memory_slice(ep, sizeof(mlk_polyvec))) - assigns(memory_slice(epp, sizeof(mlk_poly))) - ensures(forall(k0, 0, MLKEM_K, array_abs_bound(sp->vec[k0].coeffs, 0, MLKEM_N, MLKEM_ETA1 + 1))) - ensures(forall(k1, 0, MLKEM_K, array_abs_bound(ep->vec[k1].coeffs, 0, MLKEM_N, MLKEM_ETA2 + 1))) - ensures(array_abs_bound(epp->coeffs, 0, MLKEM_N, MLKEM_ETA2 + 1)) -) -{ -#if MLKEM_K == 2 - mlk_poly_getnoise_eta1122_4x(&sp->vec[0], &sp->vec[1], &ep->vec[0], - &ep->vec[1], coins, 0, 1, 2, 3); - mlk_poly_getnoise_eta2(epp, coins, 4); -#elif MLKEM_K == 3 - /* - * In this call, only the first three output buffers are needed, - * so we pass NULL as the fourth parameter, and 0xFF as its dummy nonce. - */ - mlk_poly_getnoise_eta1_4x(&sp->vec[0], &sp->vec[1], &sp->vec[2], NULL, coins, - 0, 1, 2, 0xFF /* irrelevant */); - /* The fourth output buffer in this call _is_ used. */ - mlk_poly_getnoise_eta2_4x(&ep->vec[0], &ep->vec[1], &ep->vec[2], epp, coins, - 3, 4, 5, 6); -#elif MLKEM_K == 4 - mlk_poly_getnoise_eta1_4x(&sp->vec[0], &sp->vec[1], &sp->vec[2], &sp->vec[3], - coins, 0, 1, 2, 3); - mlk_poly_getnoise_eta2_4x(&ep->vec[0], &ep->vec[1], &ep->vec[2], &ep->vec[3], - coins, 4, 5, 6, 7); - mlk_poly_getnoise_eta2(epp, coins, 8); -#endif /* MLKEM_K == 4 */ -} - - /* Reference: `indcpa_keypair_derand()` in the reference implementation @[REF]. * - We use a different implementation of `gen_matrix()` which * uses x4-batched Keccak-f1600 (see `mlk_gen_matrix()` above). @@ -509,43 +413,29 @@ int mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], return ret; } -/* Reference: `indcpa_enc()` in the reference implementation @[REF]. - * - We use x4-batched versions of `poly_getnoise` to leverage - * batched x4-batched Keccak-f1600. - * - We use a different implementation of `gen_matrix()` which - * uses x4-batched Keccak-f1600 (see `mlk_gen_matrix()` above). - * - We use a mulcache to speed up matrix-vector multiplication. - * - We include buffer zeroization. - */ +#if defined(MLK_CONFIG_ENABLE_MLKEM_BRAID) MLK_INTERNAL_API -int mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], - const uint8_t m[MLKEM_INDCPA_MSGBYTES], - const uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], - const uint8_t coins[MLKEM_SYMBYTES], - MLK_CONFIG_CONTEXT_PARAMETER_TYPE context) +#else +static MLK_ALWAYS_INLINE +#endif +int mlk_indcpa_enc_u(uint8_t ct_u[MLKEM_POLYVECCOMPRESSEDBYTES_DU], + mlk_polyvec *sp, mlk_poly *epp, + mlk_polyvec_mulcache *sp_cache, + const uint8_t seed[MLKEM_SYMBYTES], + const uint8_t coins[MLKEM_SYMBYTES], + MLK_CONFIG_CONTEXT_PARAMETER_TYPE context) { int ret = 0; - MLK_ALLOC(seed, uint8_t, MLKEM_SYMBYTES, context); MLK_ALLOC(at, mlk_polymat, 1, context); - MLK_ALLOC(sp, mlk_polyvec, 1, context); - MLK_ALLOC(pkpv, mlk_polyvec, 1, context); MLK_ALLOC(ep, mlk_polyvec, 1, context); MLK_ALLOC(b, mlk_polyvec, 1, context); - MLK_ALLOC(v, mlk_poly, 1, context); - MLK_ALLOC(k, mlk_poly, 1, context); - MLK_ALLOC(epp, mlk_poly, 1, context); - MLK_ALLOC(sp_cache, mlk_polyvec_mulcache, 1, context); - if (seed == NULL || at == NULL || sp == NULL || pkpv == NULL || ep == NULL || - b == NULL || v == NULL || k == NULL || epp == NULL || sp_cache == NULL) + if (at == NULL || ep == NULL || b == NULL) { ret = MLK_ERR_OUT_OF_MEMORY; goto cleanup; } - mlk_unpack_pk(pkpv, seed, pk); - mlk_poly_frommsg(k, m); - /* * Declassify the public seed. * Required to use it in conditional-branches in rejection sampling. @@ -556,39 +446,134 @@ int mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], mlk_gen_matrix(at, seed, 1 /* transpose */); - mlk_enc_getnoise_eta1_eta2(sp, ep, epp, coins); +#if MLKEM_K == 2 + mlk_poly_getnoise_eta1122_4x(&sp->vec[0], &sp->vec[1], &ep->vec[0], + &ep->vec[1], coins, 0, 1, 2, 3); + mlk_poly_getnoise_eta2(epp, coins, 4); +#elif MLKEM_K == 3 + /* + * In this call, only the first three output buffers are needed. + * The last parameter is a dummy that's overwritten later. + */ + mlk_poly_getnoise_eta1_4x(&sp->vec[0], &sp->vec[1], &sp->vec[2], NULL, coins, + 0, 1, 2, 0xFF /* irrelevant */); + /* The fourth output buffer in this call _is_ used. */ + mlk_poly_getnoise_eta2_4x(&ep->vec[0], &ep->vec[1], &ep->vec[2], epp, coins, + 3, 4, 5, 6); +#elif MLKEM_K == 4 + mlk_poly_getnoise_eta1_4x(&sp->vec[0], &sp->vec[1], &sp->vec[2], &sp->vec[3], + coins, 0, 1, 2, 3); + mlk_poly_getnoise_eta2_4x(&ep->vec[0], &ep->vec[1], &ep->vec[2], &ep->vec[3], + coins, 4, 5, 6, 7); + mlk_poly_getnoise_eta2(epp, coins, 8); +#endif /* MLKEM_K == 4 */ mlk_polyvec_ntt(sp); mlk_polyvec_mulcache_compute(sp_cache, sp); mlk_matvec_mul(b, at, sp, sp_cache); - mlk_polyvec_basemul_acc_montgomery_cached(v, pkpv, sp, sp_cache); mlk_polyvec_invntt_tomont(b); - mlk_poly_invntt_tomont(v); mlk_polyvec_add(b, ep); + mlk_polyvec_reduce(b); + + mlk_polyvec_compress_du(ct_u, b); + +cleanup: + /* Specification: Partially implements + * @[FIPS203, Section 3.3, Destruction of intermediate values] */ + MLK_FREE(b, mlk_polyvec, 1, context); + MLK_FREE(ep, mlk_polyvec, 1, context); + MLK_FREE(at, mlk_polymat, 1, context); + return ret; +} + +#if defined(MLK_CONFIG_ENABLE_MLKEM_BRAID) +MLK_INTERNAL_API +#else +static MLK_ALWAYS_INLINE +#endif +int mlk_indcpa_enc_v(uint8_t ct_v[MLKEM_POLYCOMPRESSEDBYTES_DV], + const mlk_polyvec *sp, const mlk_poly *epp, + const mlk_polyvec_mulcache *sp_cache, + const uint8_t m[MLKEM_INDCPA_MSGBYTES], + const uint8_t ek_vector[MLKEM_POLYVECBYTES], + MLK_CONFIG_CONTEXT_PARAMETER_TYPE context) +{ + int ret = 0; + MLK_ALLOC(pkpv, mlk_polyvec, 1, context); + MLK_ALLOC(v, mlk_poly, 1, context); + MLK_ALLOC(k, mlk_poly, 1, context); + + if (pkpv == NULL || v == NULL || k == NULL) + { + ret = MLK_ERR_OUT_OF_MEMORY; + goto cleanup; + } + + mlk_polyvec_frombytes(pkpv, ek_vector); + mlk_poly_frommsg(k, m); + + mlk_polyvec_basemul_acc_montgomery_cached(v, pkpv, sp, sp_cache); + + mlk_poly_invntt_tomont(v); + mlk_poly_add(v, epp); mlk_poly_add(v, k); - - mlk_polyvec_reduce(b); mlk_poly_reduce(v); - mlk_pack_ciphertext(c, b, v); + mlk_poly_compress_dv(ct_v, v); cleanup: /* Specification: Partially implements * @[FIPS203, Section 3.3, Destruction of intermediate values] */ - MLK_FREE(sp_cache, mlk_polyvec_mulcache, 1, context); - MLK_FREE(epp, mlk_poly, 1, context); MLK_FREE(k, mlk_poly, 1, context); MLK_FREE(v, mlk_poly, 1, context); - MLK_FREE(b, mlk_polyvec, 1, context); - MLK_FREE(ep, mlk_polyvec, 1, context); MLK_FREE(pkpv, mlk_polyvec, 1, context); + return ret; +} + +/* Reference: `indcpa_enc()` in the reference implementation @[REF]. + * Implemented as a composition of mlk_indcpa_enc_u and + * mlk_indcpa_enc_v. + */ +MLK_INTERNAL_API +int mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], + const uint8_t m[MLKEM_INDCPA_MSGBYTES], + const uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], + const uint8_t coins[MLKEM_SYMBYTES], + MLK_CONFIG_CONTEXT_PARAMETER_TYPE context) +{ + int ret = 0; + MLK_ALLOC(sp, mlk_polyvec, 1, context); + MLK_ALLOC(epp, mlk_poly, 1, context); + MLK_ALLOC(sp_cache, mlk_polyvec_mulcache, 1, context); + + if (sp == NULL || epp == NULL || sp_cache == NULL) + { + ret = MLK_ERR_OUT_OF_MEMORY; + goto cleanup; + } + + /* Phase 1: compute ct_u and intermediate state (sp, epp, sp_cache) */ + ret = mlk_indcpa_enc_u(c, sp, epp, sp_cache, pk + MLKEM_POLYVECBYTES, coins, + context); + if (ret != 0) + { + goto cleanup; + } + + /* Phase 2: compute ct_v using intermediate state */ + ret = mlk_indcpa_enc_v(c + MLKEM_POLYVECCOMPRESSEDBYTES_DU, sp, epp, sp_cache, + m, pk, context); + +cleanup: + /* Specification: Partially implements + * @[FIPS203, Section 3.3, Destruction of intermediate values] */ + MLK_FREE(sp_cache, mlk_polyvec_mulcache, 1, context); + MLK_FREE(epp, mlk_poly, 1, context); MLK_FREE(sp, mlk_polyvec, 1, context); - MLK_FREE(at, mlk_polymat, 1, context); - MLK_FREE(seed, uint8_t, MLKEM_SYMBYTES, context); return ret; } @@ -641,13 +626,10 @@ int mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES], /* To facilitate single-compilation-unit (SCU) builds, undefine all macros. * Don't modify by hand -- this is auto-generated by scripts/autogen. */ #undef mlk_pack_pk -#undef mlk_unpack_pk #undef mlk_pack_sk #undef mlk_unpack_sk -#undef mlk_pack_ciphertext #undef mlk_unpack_ciphertext #undef mlk_matvec_mul #undef mlk_polyvec_permute_bitrev_to_custom #undef mlk_polymat_permute_bitrev_to_custom #undef mlk_keypair_getnoise_eta1 -#undef mlk_enc_getnoise_eta1_eta2 diff --git a/mlkem/src/indcpa.h b/mlkem/src/indcpa.h index 5fe5e22e90..808b56f7cc 100644 --- a/mlkem/src/indcpa.h +++ b/mlkem/src/indcpa.h @@ -124,6 +124,104 @@ __contract__( return_value == MLK_ERR_OUT_OF_MEMORY) ); +#define mlk_indcpa_enc_u MLK_NAMESPACE_K(indcpa_enc_u) MLK_CONTEXT_PARAMETERS_6 + +#define mlk_indcpa_enc_v MLK_NAMESPACE_K(indcpa_enc_v) MLK_CONTEXT_PARAMETERS_6 + +#if defined(MLK_CONFIG_ENABLE_MLKEM_BRAID) +/************************************************* + * Name: mlk_indcpa_enc_u + * + * Description: Computes the u-component of a K-PKE ciphertext + * (first phase of incremental K-PKE.Encrypt). + * + * Produces ct_u = Compress_du(A^T * r + e1) and outputs + * the intermediate state (sp, epp) needed by + * mlk_indcpa_enc_v to complete the encryption. + * + * Arguments: - uint8_t *ct_u: pointer to output ct_u + * (of length MLKEM_POLYVECCOMPRESSEDBYTES_DU) + * - mlk_polyvec *sp: pointer to output r vector in NTT domain + * - mlk_poly *epp: pointer to output e2 noise polynomial + * - const uint8_t *seed: pointer to input public seed rho + * (of length MLKEM_SYMBYTES) + * - const uint8_t *coins: pointer to input random coins + * (of length MLKEM_SYMBYTES) to deterministically generate + * all randomness + * + * Specification: Partially implements + * @[FIPS203, Algorithm 14 (K-PKE.Encrypt), L1-19] + * + **************************************************/ +MLK_INTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int mlk_indcpa_enc_u(uint8_t ct_u[MLKEM_POLYVECCOMPRESSEDBYTES_DU], + mlk_polyvec *sp, mlk_poly *epp, + mlk_polyvec_mulcache *sp_cache, + const uint8_t seed[MLKEM_SYMBYTES], + const uint8_t coins[MLKEM_SYMBYTES], + MLK_CONFIG_CONTEXT_PARAMETER_TYPE context) +__contract__( + requires(memory_no_alias(ct_u, MLKEM_POLYVECCOMPRESSEDBYTES_DU)) + requires(memory_no_alias(sp, sizeof(mlk_polyvec))) + requires(memory_no_alias(epp, sizeof(mlk_poly))) + requires(memory_no_alias(sp_cache, sizeof(mlk_polyvec_mulcache))) + requires(memory_no_alias(seed, MLKEM_SYMBYTES)) + requires(memory_no_alias(coins, MLKEM_SYMBYTES)) + assigns(memory_slice(ct_u, MLKEM_POLYVECCOMPRESSEDBYTES_DU)) + assigns(memory_slice(sp, sizeof(mlk_polyvec))) + assigns(memory_slice(epp, sizeof(mlk_poly))) + assigns(memory_slice(sp_cache, sizeof(mlk_polyvec_mulcache))) + ensures(return_value == 0 || return_value == MLK_ERR_OUT_OF_MEMORY) + ensures(return_value == 0 ==> + array_abs_bound(epp->coeffs, 0, MLKEM_N, MLKEM_ETA2 + 1)) +); + +/************************************************* + * Name: mlk_indcpa_enc_v + * + * Description: Computes the v-component of a K-PKE ciphertext + * (second phase of incremental K-PKE.Encrypt). + * + * Produces ct_v = Compress_dv(t^T * r + e2 + msg) using + * intermediate state (sp, epp) from mlk_indcpa_enc_u. + * + * Arguments: - uint8_t *ct_v: pointer to output ct_v + * (of length MLKEM_POLYCOMPRESSEDBYTES_DV) + * - const mlk_polyvec *sp: pointer to input r vector + * in NTT domain + * - const mlk_poly *epp: pointer to input e2 noise polynomial + * - const uint8_t *m: pointer to input message + * (of length MLKEM_INDCPA_MSGBYTES) + * - const uint8_t *ek_vector: pointer to input encoded public + * key vector t_hat (of length MLKEM_POLYVECBYTES) + * + * Specification: Partially implements + * @[FIPS203, Algorithm 14 (K-PKE.Encrypt), L2-3, L20-23] + * + **************************************************/ +MLK_INTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int mlk_indcpa_enc_v(uint8_t ct_v[MLKEM_POLYCOMPRESSEDBYTES_DV], + const mlk_polyvec *sp, const mlk_poly *epp, + const mlk_polyvec_mulcache *sp_cache, + const uint8_t m[MLKEM_INDCPA_MSGBYTES], + const uint8_t ek_vector[MLKEM_POLYVECBYTES], + MLK_CONFIG_CONTEXT_PARAMETER_TYPE context) +__contract__( + requires(memory_no_alias(ct_v, MLKEM_POLYCOMPRESSEDBYTES_DV)) + requires(memory_no_alias(sp, sizeof(mlk_polyvec))) + requires(memory_no_alias(epp, sizeof(mlk_poly))) + requires(memory_no_alias(sp_cache, sizeof(mlk_polyvec_mulcache))) + requires(array_abs_bound(epp->coeffs, 0, MLKEM_N, 16)) + requires(memory_no_alias(m, MLKEM_INDCPA_MSGBYTES)) + requires(memory_no_alias(ek_vector, MLKEM_POLYVECBYTES)) + assigns(memory_slice(ct_v, MLKEM_POLYCOMPRESSEDBYTES_DV)) + ensures(return_value == 0 || return_value == MLK_ERR_OUT_OF_MEMORY) +); + +#endif /* MLK_CONFIG_ENABLE_MLKEM_BRAID */ + #define mlk_indcpa_dec MLK_NAMESPACE_K(indcpa_dec) MLK_CONTEXT_PARAMETERS_3 /** * Decryption function of the CPA-secure public-key encryption scheme diff --git a/mlkem/src/kem.c b/mlkem/src/kem.c index 3c82d6df70..0225647494 100644 --- a/mlkem/src/kem.c +++ b/mlkem/src/kem.c @@ -35,6 +35,11 @@ * of mlkem-native (e.g. with varying security levels) * within a single compilation unit. */ #define mlk_check_pct MLK_ADD_PARAM_SET(mlk_check_pct) MLK_CONTEXT_PARAMETERS_2 +#define mlk_serialize_epp MLK_ADD_PARAM_SET(mlk_serialize_epp) +#define mlk_deserialize_epp MLK_ADD_PARAM_SET(mlk_deserialize_epp) +#define mlk_serialize_polyvec_16le MLK_ADD_PARAM_SET(mlk_serialize_polyvec_16le) +#define mlk_deserialize_polyvec_16le \ + MLK_ADD_PARAM_SET(mlk_deserialize_polyvec_16le) /* End of parameter set namespacing */ /* Reference: Not implemented in the reference implementation @[REF]. */ @@ -369,6 +374,227 @@ int mlk_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], } #endif /* !MLK_CONFIG_NO_RANDOMIZED_API */ +#if defined(MLK_CONFIG_ENABLE_MLKEM_BRAID) + +/* 4-bit packing for noise polynomial e2. + * Coefficients in [-ETA2, ETA2] are stored as (ETA2 - x), fitting in 4 bits. + * Two coefficients per byte (low nibble first). */ +static void mlk_serialize_epp(uint8_t out[MLKEM_EPP_BYTES], const mlk_poly *p) +__contract__( + requires(memory_no_alias(out, MLKEM_EPP_BYTES)) + requires(memory_no_alias(p, sizeof(mlk_poly))) + requires(array_abs_bound(p->coeffs, 0, MLKEM_N, MLKEM_ETA2 + 1)) + assigns(memory_slice(out, MLKEM_EPP_BYTES)) +) +{ + unsigned j; + for (j = 0; j < MLKEM_N / 2; j++) + __loop__( + assigns(j, memory_slice(out, MLKEM_EPP_BYTES)) + invariant(j <= MLKEM_N / 2) + decreases(MLKEM_N / 2 - j)) + { + uint8_t lo = (uint8_t)(MLKEM_ETA2 - p->coeffs[2 * j]); + uint8_t hi = (uint8_t)(MLKEM_ETA2 - p->coeffs[2 * j + 1]); + out[j] = (uint8_t)((lo & 0xF) | (uint8_t)(hi << 4)); + } +} + +static void mlk_deserialize_epp(mlk_poly *p, const uint8_t in[MLKEM_EPP_BYTES]) +__contract__( + requires(memory_no_alias(in, MLKEM_EPP_BYTES)) + requires(memory_no_alias(p, sizeof(mlk_poly))) + assigns(memory_slice(p, sizeof(mlk_poly))) + ensures(array_abs_bound(p->coeffs, 0, MLKEM_N, 16)) +) +{ + unsigned j; + for (j = 0; j < MLKEM_N / 2; j++) + __loop__( + assigns(j, memory_slice(p, sizeof(mlk_poly))) + invariant(j <= MLKEM_N / 2) + invariant(array_abs_bound(p->coeffs, 0, 2 * j, 16)) + decreases(MLKEM_N / 2 - j)) + { + p->coeffs[2 * j] = (int16_t)((int16_t)MLKEM_ETA2 - (int16_t)(in[j] & 0xF)); + p->coeffs[2 * j + 1] = + (int16_t)((int16_t)MLKEM_ETA2 - (int16_t)(in[j] >> 4)); + } +} + +/* 16-bit little-endian serialization for intermediate polyvec state. + * Stores each int16_t coefficient as 2 bytes in LE order. + * Coefficients must be non-negative (e.g., after reduce). */ +static void mlk_serialize_polyvec_16le(uint8_t out[MLKEM_POLYVEC16_BYTES], + const mlk_polyvec *v) +__contract__( + requires(memory_no_alias(out, MLKEM_POLYVEC16_BYTES)) + requires(memory_no_alias(v, sizeof(mlk_polyvec))) + assigns(memory_slice(out, MLKEM_POLYVEC16_BYTES)) +) +{ + unsigned i, j; + for (i = 0; i < MLKEM_K; i++) + __loop__( + assigns(i, j, memory_slice(out, MLKEM_POLYVEC16_BYTES)) + invariant(i <= MLKEM_K) + decreases(MLKEM_K - i)) + { + for (j = 0; j < MLKEM_N; j++) + __loop__( + assigns(j, memory_slice(out, MLKEM_POLYVEC16_BYTES)) + invariant(j <= MLKEM_N) + decreases(MLKEM_N - j)) + { + uint16_t c = mlk_cast_int16_to_uint16(v->vec[i].coeffs[j]); + out[i * MLKEM_POLY16_BYTES + 2 * j] = (uint8_t)(c & 0xFF); + out[i * MLKEM_POLY16_BYTES + 2 * j + 1] = (uint8_t)(c >> 8); + } + } +} + +static void mlk_deserialize_polyvec_16le( + mlk_polyvec *v, const uint8_t in[MLKEM_POLYVEC16_BYTES]) +__contract__( + requires(memory_no_alias(in, MLKEM_POLYVEC16_BYTES)) + requires(memory_no_alias(v, sizeof(mlk_polyvec))) + assigns(memory_slice(v, sizeof(mlk_polyvec))) +) +{ + unsigned i, j; + for (i = 0; i < MLKEM_K; i++) + __loop__( + assigns(i, j, memory_slice(v, sizeof(mlk_polyvec))) + invariant(i <= MLKEM_K) + decreases(MLKEM_K - i)) + { + for (j = 0; j < MLKEM_N; j++) + __loop__( + assigns(j, memory_slice(v, sizeof(mlk_polyvec))) + invariant(j <= MLKEM_N) + decreases(MLKEM_N - j)) + { + v->vec[i].coeffs[j] = mlk_cast_uint16_to_int16( + (uint16_t)((unsigned)in[i * MLKEM_POLY16_BYTES + 2 * j] | + ((unsigned)in[i * MLKEM_POLY16_BYTES + 2 * j + 1] << 8))); + } + } +} + +MLK_EXTERNAL_API +int mlk_kem_enc_derand_u(uint8_t ct_u[MLKEM_POLYVECCOMPRESSEDBYTES_DU], + uint8_t ss[MLKEM_SSBYTES], + uint8_t sp_serial[MLKEM_POLYVEC16_BYTES], + uint8_t epp_serial[MLKEM_EPP_BYTES], + const uint8_t seed[MLKEM_SYMBYTES], + const uint8_t hpk[MLKEM_SYMBYTES], + const uint8_t coins[MLKEM_SYMBYTES], + MLK_CONFIG_CONTEXT_PARAMETER_TYPE context) +{ + int ret = 0; + MLK_ALLOC(buf, uint8_t, 2 * MLKEM_SYMBYTES, context); + MLK_ALLOC(kr, uint8_t, 2 * MLKEM_SYMBYTES, context); + MLK_ALLOC(sp, mlk_polyvec, 1, context); + MLK_ALLOC(epp, mlk_poly, 1, context); + MLK_ALLOC(sp_cache, mlk_polyvec_mulcache, 1, context); + + if (buf == NULL || kr == NULL || sp == NULL || epp == NULL || + sp_cache == NULL) + { + ret = MLK_ERR_OUT_OF_MEMORY; + goto cleanup; + } + + /* FO transform: (K, r) = G(coins || H(pk)) */ + mlk_memcpy(buf, coins, MLKEM_SYMBYTES); + mlk_memcpy(buf + MLKEM_SYMBYTES, hpk, MLKEM_SYMBYTES); + mlk_hash_g(kr, buf, 2 * MLKEM_SYMBYTES); + + /* Compute ct_u using derived randomness r */ + ret = mlk_indcpa_enc_u(ct_u, sp, epp, sp_cache, seed, kr + MLKEM_SYMBYTES, + context); + if (ret != 0) + { + goto cleanup; + } + + /* Reduce sp to unsigned canonical form before serialization */ + mlk_polyvec_reduce(sp); + + /* Serialize intermediate state */ + mlk_serialize_polyvec_16le(sp_serial, sp); + mlk_serialize_epp(epp_serial, epp); + + /* Shared secret K = first MLKEM_SYMBYTES bytes of G output */ + mlk_memcpy(ss, kr, MLKEM_SYMBYTES); + +cleanup: + /* Specification: Partially implements + * @[FIPS203, Section 3.3, Destruction of intermediate values] */ + MLK_FREE(sp_cache, mlk_polyvec_mulcache, 1, context); + MLK_FREE(epp, mlk_poly, 1, context); + MLK_FREE(sp, mlk_polyvec, 1, context); + MLK_FREE(kr, uint8_t, 2 * MLKEM_SYMBYTES, context); + MLK_FREE(buf, uint8_t, 2 * MLKEM_SYMBYTES, context); + return ret; +} + +MLK_EXTERNAL_API +int mlk_kem_enc_v(uint8_t ct_v[MLKEM_POLYCOMPRESSEDBYTES_DV], + const uint8_t sp_serial[MLKEM_POLYVEC16_BYTES], + const uint8_t epp_serial[MLKEM_EPP_BYTES], + const uint8_t coins[MLKEM_SYMBYTES], + const uint8_t ek_vector[MLKEM_POLYVECBYTES], + MLK_CONFIG_CONTEXT_PARAMETER_TYPE context) +{ + int ret = 0; + MLK_ALLOC(sp, mlk_polyvec, 1, context); + MLK_ALLOC(epp, mlk_poly, 1, context); + MLK_ALLOC(sp_cache, mlk_polyvec_mulcache, 1, context); + MLK_ALLOC(p, mlk_polyvec, 1, context); + MLK_ALLOC(p_reencoded, uint8_t, MLKEM_POLYVECBYTES, context); + + if (sp == NULL || epp == NULL || sp_cache == NULL || p == NULL || + p_reencoded == NULL) + { + ret = MLK_ERR_OUT_OF_MEMORY; + goto cleanup; + } + + /* Specification: Implements @[FIPS203, Section 7.2, Modulus check] + * on the public key vector ek_vector */ + mlk_polyvec_frombytes(p, ek_vector); + mlk_polyvec_reduce(p); + mlk_polyvec_tobytes(p_reencoded, p); + ret = mlk_ct_memcmp(ek_vector, p_reencoded, MLKEM_POLYVECBYTES) ? MLK_ERR_FAIL + : 0; + if (ret != 0) + { + goto cleanup; + } + + /* Deserialize intermediate state */ + mlk_deserialize_polyvec_16le(sp, sp_serial); + mlk_deserialize_epp(epp, epp_serial); + + /* Compute mulcache for deserialized sp */ + mlk_polyvec_mulcache_compute(sp_cache, sp); + + ret = mlk_indcpa_enc_v(ct_v, sp, epp, sp_cache, coins, ek_vector, context); + +cleanup: + /* Specification: Partially implements + * @[FIPS203, Section 3.3, Destruction of intermediate values] */ + MLK_FREE(p_reencoded, uint8_t, MLKEM_POLYVECBYTES, context); + MLK_FREE(p, mlk_polyvec, 1, context); + MLK_FREE(sp_cache, mlk_polyvec_mulcache, 1, context); + MLK_FREE(epp, mlk_poly, 1, context); + MLK_FREE(sp, mlk_polyvec, 1, context); + return ret; +} + +#endif /* MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /* Reference: `crypto_kem_dec()` in the reference implementation @[REF] * - We include secret key check * - We include stack buffer zeroization */ @@ -444,3 +670,7 @@ int mlk_kem_dec(uint8_t ss[MLKEM_SSBYTES], /* To facilitate single-compilation-unit (SCU) builds, undefine all macros. * Don't modify by hand -- this is auto-generated by scripts/autogen. */ #undef mlk_check_pct +#undef mlk_serialize_epp +#undef mlk_deserialize_epp +#undef mlk_serialize_polyvec_16le +#undef mlk_deserialize_polyvec_16le diff --git a/mlkem/src/kem.h b/mlkem/src/kem.h index 5310dc8b4d..116401a867 100644 --- a/mlkem/src/kem.h +++ b/mlkem/src/kem.h @@ -55,6 +55,12 @@ #define mlk_kem_check_pk MLK_NAMESPACE_K(check_pk) MLK_CONTEXT_PARAMETERS_1 #define mlk_kem_check_sk MLK_NAMESPACE_K(check_sk) MLK_CONTEXT_PARAMETERS_1 +#if defined(MLK_CONFIG_ENABLE_MLKEM_BRAID) +#define mlk_kem_enc_derand_u \ + MLK_NAMESPACE_K(enc_derand_u) MLK_CONTEXT_PARAMETERS_7 +#define mlk_kem_enc_v MLK_NAMESPACE_K(enc_v) MLK_CONTEXT_PARAMETERS_5 +#endif + /** * Implements modulus check mandated by FIPS 203, i.e., ensures that * coefficients are in [0,q-1]. @@ -265,6 +271,136 @@ __contract__( return_value == MLK_ERR_RNG_FAIL) ); +#if defined(MLK_CONFIG_ENABLE_MLKEM_BRAID) + +/* Size of a polynomial serialized via 16-bit little-endian encoding + * (2 bytes per coefficient). Used for the intermediate state in + * incremental encapsulation. */ +#define MLKEM_POLY16_BYTES (MLKEM_N * 2) +#define MLKEM_POLYVEC16_BYTES (MLKEM_K * MLKEM_POLY16_BYTES) + +/* Size of noise polynomial e2 packed as 4-bit nibbles (2 coefficients per + * byte). Coefficients in [-ETA2, ETA2] are stored as (ETA2 - x), fitting + * in 4 bits. */ +#define MLKEM_EPP_BYTES (MLKEM_N / 2) + +/** + * First phase of incremental ML-KEM encapsulation. + * + * Computes the u-component of the ciphertext and the shared secret, and + * outputs serialized intermediate state needed by mlk_kem_enc_v. + * + * Only requires the public seed (ek_seed) and the hash of the full public + * key (hpk), not the full public key. + * + * @spec{Partially implements @[FIPS203, Algorithm 17, ML-KEM.Encaps_Internal, + * L1-4] combined with the u-phase of K-PKE.Encrypt.} + * + * @param[out] ct_u Output u-component of ciphertext (an already + * allocated array of MLKEM_POLYVECCOMPRESSEDBYTES_DU + * bytes). + * @param[out] ss Output shared secret (an already allocated array of + * MLKEM_SSBYTES bytes). + * @param[out] sp_serial Output serialized r vector in NTT domain (an already + * allocated array of MLKEM_POLYVEC16_BYTES bytes, + * needed by mlk_kem_enc_v). + * @param[out] epp_serial Output serialized e2 noise polynomial as 4-bit + * nibbles (an already allocated array of + * MLKEM_EPP_BYTES bytes, needed by mlk_kem_enc_v). + * @param[in] seed Input public seed rho (an already allocated array of + * MLKEM_SYMBYTES bytes, from pk[MLKEM_POLYVECBYTES:]). + * @param[in] hpk Input H(pk) (an already allocated array of + * MLKEM_SYMBYTES bytes). + * @param[in] coins Input randomness (an already allocated array of + * MLKEM_SYMBYTES bytes). + * @param context Application context (build-configurable; see + * MLK_CONFIG_CONTEXT_PARAMETER_TYPE). + * + * @retval 0 Success. + * @retval MLK_ERR_OUT_OF_MEMORY MLK_CONFIG_CUSTOM_ALLOC_FREE was used and + * MLK_CUSTOM_ALLOC returned NULL. + */ +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int mlk_kem_enc_derand_u(uint8_t ct_u[MLKEM_POLYVECCOMPRESSEDBYTES_DU], + uint8_t ss[MLKEM_SSBYTES], + uint8_t sp_serial[MLKEM_POLYVEC16_BYTES], + uint8_t epp_serial[MLKEM_EPP_BYTES], + const uint8_t seed[MLKEM_SYMBYTES], + const uint8_t hpk[MLKEM_SYMBYTES], + const uint8_t coins[MLKEM_SYMBYTES], + MLK_CONFIG_CONTEXT_PARAMETER_TYPE context) +__contract__( + requires(memory_no_alias(ct_u, MLKEM_POLYVECCOMPRESSEDBYTES_DU)) + requires(memory_no_alias(ss, MLKEM_SSBYTES)) + requires(memory_no_alias(sp_serial, MLKEM_POLYVEC16_BYTES)) + requires(memory_no_alias(epp_serial, MLKEM_EPP_BYTES)) + requires(memory_no_alias(seed, MLKEM_SYMBYTES)) + requires(memory_no_alias(hpk, MLKEM_SYMBYTES)) + requires(memory_no_alias(coins, MLKEM_SYMBYTES)) + assigns(memory_slice(ct_u, MLKEM_POLYVECCOMPRESSEDBYTES_DU)) + assigns(memory_slice(ss, MLKEM_SSBYTES)) + assigns(memory_slice(sp_serial, MLKEM_POLYVEC16_BYTES)) + assigns(memory_slice(epp_serial, MLKEM_EPP_BYTES)) + ensures(return_value == 0 || return_value == MLK_ERR_OUT_OF_MEMORY) +); + +/** + * Second phase of incremental ML-KEM encapsulation. + * + * Deserializes the intermediate state from mlk_kem_enc_derand_u and + * computes the v-component of the ciphertext. + * + * Performs the modulus check on ek_vector. + * + * @spec{Partially implements @[FIPS203, Algorithm 17, ML-KEM.Encaps_Internal] + * combined with the v-phase of K-PKE.Encrypt, and @[FIPS203, Section 7.2, + * modulus check].} + * + * @param[out] ct_v Output v-component of ciphertext (an already + * allocated array of MLKEM_POLYCOMPRESSEDBYTES_DV + * bytes). + * @param[in] sp_serial Input serialized r vector in NTT domain (an already + * allocated array of MLKEM_POLYVEC16_BYTES bytes, + * from mlk_kem_enc_derand_u). + * @param[in] epp_serial Input serialized e2 noise polynomial as 4-bit + * nibbles (an already allocated array of + * MLKEM_EPP_BYTES bytes, from mlk_kem_enc_derand_u). + * @param[in] coins Input randomness (an already allocated array of + * MLKEM_SYMBYTES bytes, same as passed to + * mlk_kem_enc_derand_u). + * @param[in] ek_vector Input encoded public key vector t_hat (an already + * allocated array of MLKEM_POLYVECBYTES bytes, from + * pk[0:MLKEM_POLYVECBYTES]). + * @param context Application context (build-configurable; see + * MLK_CONFIG_CONTEXT_PARAMETER_TYPE). + * + * @retval 0 Success. + * @retval MLK_ERR_FAIL The modulus check on ek_vector failed. + * @retval MLK_ERR_OUT_OF_MEMORY MLK_CONFIG_CUSTOM_ALLOC_FREE was used and + * MLK_CUSTOM_ALLOC returned NULL. + */ +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int mlk_kem_enc_v(uint8_t ct_v[MLKEM_POLYCOMPRESSEDBYTES_DV], + const uint8_t sp_serial[MLKEM_POLYVEC16_BYTES], + const uint8_t epp_serial[MLKEM_EPP_BYTES], + const uint8_t coins[MLKEM_SYMBYTES], + const uint8_t ek_vector[MLKEM_POLYVECBYTES], + MLK_CONFIG_CONTEXT_PARAMETER_TYPE context) +__contract__( + requires(memory_no_alias(ct_v, MLKEM_POLYCOMPRESSEDBYTES_DV)) + requires(memory_no_alias(sp_serial, MLKEM_POLYVEC16_BYTES)) + requires(memory_no_alias(epp_serial, MLKEM_EPP_BYTES)) + requires(memory_no_alias(coins, MLKEM_SYMBYTES)) + requires(memory_no_alias(ek_vector, MLKEM_POLYVECBYTES)) + assigns(memory_slice(ct_v, MLKEM_POLYCOMPRESSEDBYTES_DV)) + ensures(return_value == 0 || return_value == MLK_ERR_FAIL || + return_value == MLK_ERR_OUT_OF_MEMORY) +); + +#endif /* MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /** * Generate shared secret for a given ciphertext and private key. * diff --git a/proofs/cbmc/deserialize_epp/Makefile b/proofs/cbmc/deserialize_epp/Makefile new file mode 100644 index 0000000000..f08792f8ce --- /dev/null +++ b/proofs/cbmc/deserialize_epp/Makefile @@ -0,0 +1,36 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = deserialize_epp_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = mlk_deserialize_epp + +DEFINES += -DMLK_CONFIG_ENABLE_MLKEM_BRAID +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_deserialize_epp +USE_FUNCTION_CONTRACTS = +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = mlk_deserialize_epp + +# This function is large enough to need... +CBMC_OBJECT_BITS = 12 + +include ../Makefile.common diff --git a/proofs/cbmc/deserialize_epp/deserialize_epp_harness.c b/proofs/cbmc/deserialize_epp/deserialize_epp_harness.c new file mode 100644 index 0000000000..85d753c1eb --- /dev/null +++ b/proofs/cbmc/deserialize_epp/deserialize_epp_harness.c @@ -0,0 +1,21 @@ +// Copyright (c) The mlkem-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include +#include + +#define mlk_deserialize_epp MLK_NAMESPACE(deserialize_epp) +void mlk_deserialize_epp(mlk_poly *p, const uint8_t in[MLKEM_EPP_BYTES]); + +void harness(void) +{ + { + /* Dummy use of `free` to work around CBMC issue #8814. */ + free(NULL); + } + + uint8_t *in; + mlk_poly *p; + + mlk_deserialize_epp(p, in); +} diff --git a/proofs/cbmc/deserialize_polyvec_16le/Makefile b/proofs/cbmc/deserialize_polyvec_16le/Makefile new file mode 100644 index 0000000000..b67c3ccc01 --- /dev/null +++ b/proofs/cbmc/deserialize_polyvec_16le/Makefile @@ -0,0 +1,36 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = deserialize_polyvec_16le_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = mlk_deserialize_polyvec_16le + +DEFINES += -DMLK_CONFIG_ENABLE_MLKEM_BRAID +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_deserialize_polyvec_16le +USE_FUNCTION_CONTRACTS = +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = mlk_deserialize_polyvec_16le + +# This function is large enough to need... +CBMC_OBJECT_BITS = 12 + +include ../Makefile.common diff --git a/proofs/cbmc/deserialize_polyvec_16le/deserialize_polyvec_16le_harness.c b/proofs/cbmc/deserialize_polyvec_16le/deserialize_polyvec_16le_harness.c new file mode 100644 index 0000000000..03f265624e --- /dev/null +++ b/proofs/cbmc/deserialize_polyvec_16le/deserialize_polyvec_16le_harness.c @@ -0,0 +1,22 @@ +// Copyright (c) The mlkem-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include +#include + +#define mlk_deserialize_polyvec_16le MLK_NAMESPACE(deserialize_polyvec_16le) +void mlk_deserialize_polyvec_16le(mlk_polyvec *v, + const uint8_t in[MLKEM_POLYVEC16_BYTES]); + +void harness(void) +{ + { + /* Dummy use of `free` to work around CBMC issue #8814. */ + free(NULL); + } + + uint8_t *in; + mlk_polyvec *v; + + mlk_deserialize_polyvec_16le(v, in); +} diff --git a/proofs/cbmc/enc_getnoise_eta1_eta2/Makefile b/proofs/cbmc/enc_getnoise_eta1_eta2/Makefile deleted file mode 100644 index b6233db7ac..0000000000 --- a/proofs/cbmc/enc_getnoise_eta1_eta2/Makefile +++ /dev/null @@ -1,66 +0,0 @@ -# Copyright (c) The mlkem-native project authors -# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -include ../Makefile_params.common - -HARNESS_ENTRY = harness -HARNESS_FILE = enc_getnoise_eta1_eta2_harness - -# This should be a unique identifier for this proof, and will appear on the -# Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = mlk_enc_getnoise_eta1_eta2 - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/src/indcpa.c - -CHECK_FUNCTION_CONTRACTS=mlk_enc_getnoise_eta1_eta2 - -# Note that the called function mlk_poly_getnoise_eta2_4x() is actually -# just #define'd to be mlk_poly_getnoise_eta1_4x() -ifeq ($(MLKEM_K),2) -USE_FUNCTION_CONTRACTS = mlk_poly_getnoise_eta1122_4x -USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta2 -else ifeq ($(MLKEM_K),3) -USE_FUNCTION_CONTRACTS = mlk_poly_getnoise_eta1_4x -else # MLKEM_K must be 4 -USE_FUNCTION_CONTRACTS = mlk_poly_getnoise_eta1_4x -USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta2 -endif - -APPLY_LOOP_CONTRACTS=on -USE_DYNAMIC_FRAMES=1 - -# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead -EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 - -FUNCTION_NAME = mlk_enc_getnoise_eta1_eta2 - -# If this proof is found to consume huge amounts of RAM, you can set the -# EXPENSIVE variable. With new enough versions of the proof tools, this will -# restrict the number of EXPENSIVE CBMC jobs running at once. See the -# documentation in Makefile.common under the "Job Pools" heading for details. -# EXPENSIVE = true - -# This function is large enough to need... -CBMC_OBJECT_BITS = 10 - -# If you require access to a file-local ("static") function or object to conduct -# your proof, set the following (and do not include the original source file -# ("mlkem/src/poly.c") in PROJECT_SOURCES). -# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i -# include ../Makefile.common -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/poly.c -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz -# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must -# be set before including Makefile.common, but any use of variables on the -# left-hand side requires those variables to be defined. Hence, _SOURCE, -# _FUNCTIONS, _OBJECTS is set after including Makefile.common. - -include ../Makefile.common diff --git a/proofs/cbmc/enc_getnoise_eta1_eta2/enc_getnoise_eta1_eta2_harness.c b/proofs/cbmc/enc_getnoise_eta1_eta2/enc_getnoise_eta1_eta2_harness.c deleted file mode 100644 index 836df9f72c..0000000000 --- a/proofs/cbmc/enc_getnoise_eta1_eta2/enc_getnoise_eta1_eta2_harness.c +++ /dev/null @@ -1,23 +0,0 @@ -// Copyright (c) The mlkem-native project authors -// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: MIT-0 - -#include - -#define mlk_enc_getnoise_eta1_eta2 MLK_NAMESPACE(enc_getnoise_eta1_eta2) -void mlk_enc_getnoise_eta1_eta2(mlk_polyvec *sp, mlk_polyvec *ep, mlk_poly *epp, - const uint8_t coins[MLKEM_SYMBYTES]); - -void harness(void) -{ - mlk_polyvec *sp, *ep; - mlk_poly *epp; - uint8_t *coins; - - { - /* Dummy use of `free` to work around CBMC issue #8814. */ - free(NULL); - } - - mlk_enc_getnoise_eta1_eta2(sp, ep, epp, coins); -} diff --git a/proofs/cbmc/indcpa_enc/Makefile b/proofs/cbmc/indcpa_enc/Makefile index e9ac63b842..10afd2d9c6 100644 --- a/proofs/cbmc/indcpa_enc/Makefile +++ b/proofs/cbmc/indcpa_enc/Makefile @@ -10,7 +10,7 @@ HARNESS_FILE = indcpa_enc_harness # Litani dashboard. It can be human-readable and contain spaces if you wish. PROOF_UID = mlk_indcpa_enc -DEFINES += +DEFINES += -DMLK_CONFIG_ENABLE_MLKEM_BRAID INCLUDES += REMOVE_FUNCTION_BODY += @@ -20,24 +20,14 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/src/indcpa.c CHECK_FUNCTION_CONTRACTS=mlk_indcpa_enc -USE_FUNCTION_CONTRACTS = mlk_poly_frommsg +USE_FUNCTION_CONTRACTS = mlk_indcpa_enc_u +USE_FUNCTION_CONTRACTS += mlk_indcpa_enc_v +USE_FUNCTION_CONTRACTS += mlk_zeroize + +# Suppress spurious warning for gen_matrix() not having loop contracts +# by making it appear to be call-by-contract USE_FUNCTION_CONTRACTS += mlk_gen_matrix -USE_FUNCTION_CONTRACTS += mlk_enc_getnoise_eta1_eta2 -USE_FUNCTION_CONTRACTS += mlk_polyvec_ntt -USE_FUNCTION_CONTRACTS += mlk_polyvec_mulcache_compute -USE_FUNCTION_CONTRACTS += mlk_polyvec_basemul_acc_montgomery_cached -USE_FUNCTION_CONTRACTS += mlk_polyvec_invntt_tomont -USE_FUNCTION_CONTRACTS += mlk_poly_invntt_tomont -USE_FUNCTION_CONTRACTS += mlk_polyvec_add -USE_FUNCTION_CONTRACTS += mlk_poly_add -USE_FUNCTION_CONTRACTS += mlk_polyvec_reduce -USE_FUNCTION_CONTRACTS += mlk_poly_reduce -USE_FUNCTION_CONTRACTS += mlk_polyvec_compress_du -USE_FUNCTION_CONTRACTS += mlk_poly_compress_dv -USE_FUNCTION_CONTRACTS += mlk_polyvec_frombytes -USE_FUNCTION_CONTRACTS += mlk_matvec_mul -USE_FUNCTION_CONTRACTS += mlk_zeroize APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/indcpa_enc_u/Makefile b/proofs/cbmc/indcpa_enc_u/Makefile new file mode 100644 index 0000000000..66ef380c8d --- /dev/null +++ b/proofs/cbmc/indcpa_enc_u/Makefile @@ -0,0 +1,54 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = indcpa_enc_u_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = mlk_indcpa_enc_u + +DEFINES += -DMLK_CONFIG_ENABLE_MLKEM_BRAID +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/indcpa.c + +CHECK_FUNCTION_CONTRACTS=mlk_indcpa_enc_u +USE_FUNCTION_CONTRACTS = mlk_gen_matrix +ifeq ($(MLKEM_K),2) +USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta1122_4x +USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta2 +else ifeq ($(MLKEM_K),3) +USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta1_4x +else ifeq ($(MLKEM_K),4) +USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta1_4x +USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta2 +endif + +USE_FUNCTION_CONTRACTS += mlk_polyvec_ntt +USE_FUNCTION_CONTRACTS += mlk_polyvec_mulcache_compute +USE_FUNCTION_CONTRACTS += mlk_matvec_mul +USE_FUNCTION_CONTRACTS += mlk_polyvec_invntt_tomont +USE_FUNCTION_CONTRACTS += mlk_polyvec_add +USE_FUNCTION_CONTRACTS += mlk_polyvec_reduce +USE_FUNCTION_CONTRACTS += mlk_polyvec_compress_du +USE_FUNCTION_CONTRACTS += mlk_zeroize +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_smt_only --z3 + +FUNCTION_NAME = mlk_indcpa_enc_u + +# This function is large enough to need... +CBMC_OBJECT_BITS = 12 + +include ../Makefile.common diff --git a/proofs/cbmc/indcpa_enc_u/indcpa_enc_u_harness.c b/proofs/cbmc/indcpa_enc_u/indcpa_enc_u_harness.c new file mode 100644 index 0000000000..210f0cb363 --- /dev/null +++ b/proofs/cbmc/indcpa_enc_u/indcpa_enc_u_harness.c @@ -0,0 +1,16 @@ +// Copyright (c) The mlkem-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include + +void harness(void) +{ + uint8_t *ct_u; + mlk_polyvec *sp; + mlk_poly *epp; + mlk_polyvec_mulcache *sp_cache; + uint8_t *seed; + uint8_t *coins; + mlk_indcpa_enc_u(ct_u, sp, epp, sp_cache, seed, coins, + NULL /* context will be dropped by preprocessor */); +} diff --git a/proofs/cbmc/indcpa_enc_v/Makefile b/proofs/cbmc/indcpa_enc_v/Makefile new file mode 100644 index 0000000000..077c73a18b --- /dev/null +++ b/proofs/cbmc/indcpa_enc_v/Makefile @@ -0,0 +1,44 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = indcpa_enc_v_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = mlk_indcpa_enc_v + +DEFINES += -DMLK_CONFIG_ENABLE_MLKEM_BRAID +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/indcpa.c + +CHECK_FUNCTION_CONTRACTS=mlk_indcpa_enc_v +USE_FUNCTION_CONTRACTS = mlk_polyvec_frombytes +USE_FUNCTION_CONTRACTS += mlk_poly_frommsg +USE_FUNCTION_CONTRACTS += mlk_polyvec_mulcache_compute +USE_FUNCTION_CONTRACTS += mlk_polyvec_basemul_acc_montgomery_cached +USE_FUNCTION_CONTRACTS += mlk_poly_invntt_tomont +USE_FUNCTION_CONTRACTS += mlk_poly_add +USE_FUNCTION_CONTRACTS += mlk_poly_reduce +USE_FUNCTION_CONTRACTS += mlk_poly_compress_dv +USE_FUNCTION_CONTRACTS += mlk_zeroize +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_smt_only --z3 + +FUNCTION_NAME = mlk_indcpa_enc_v + +# This function is large enough to need... +CBMC_OBJECT_BITS = 10 + +include ../Makefile.common diff --git a/proofs/cbmc/indcpa_enc_v/indcpa_enc_v_harness.c b/proofs/cbmc/indcpa_enc_v/indcpa_enc_v_harness.c new file mode 100644 index 0000000000..3556db3be0 --- /dev/null +++ b/proofs/cbmc/indcpa_enc_v/indcpa_enc_v_harness.c @@ -0,0 +1,16 @@ +// Copyright (c) The mlkem-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include + +void harness(void) +{ + uint8_t *ct_v; + mlk_polyvec *sp; + mlk_poly *epp; + mlk_polyvec_mulcache *sp_cache; + uint8_t *m; + uint8_t *ek_vector; + mlk_indcpa_enc_v(ct_v, sp, epp, sp_cache, m, ek_vector, + NULL /* context will be dropped by preprocessor */); +} diff --git a/proofs/cbmc/kem_enc_derand_u/Makefile b/proofs/cbmc/kem_enc_derand_u/Makefile new file mode 100644 index 0000000000..1d05ff0996 --- /dev/null +++ b/proofs/cbmc/kem_enc_derand_u/Makefile @@ -0,0 +1,41 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = kem_enc_derand_u_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = mlk_enc_derand_u + +DEFINES += -DMLK_CONFIG_ENABLE_MLKEM_BRAID +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_enc_derand_u +USE_FUNCTION_CONTRACTS = mlk_indcpa_enc_u +USE_FUNCTION_CONTRACTS += mlk_sha3_512 +USE_FUNCTION_CONTRACTS += mlk_polyvec_reduce +USE_FUNCTION_CONTRACTS += mlk_serialize_epp +USE_FUNCTION_CONTRACTS += mlk_serialize_polyvec_16le +USE_FUNCTION_CONTRACTS += mlk_zeroize +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = mlk_enc_derand_u + +# This function is large enough to need... +CBMC_OBJECT_BITS = 10 + +include ../Makefile.common diff --git a/proofs/cbmc/kem_enc_derand_u/kem_enc_derand_u_harness.c b/proofs/cbmc/kem_enc_derand_u/kem_enc_derand_u_harness.c new file mode 100644 index 0000000000..f93fb97dac --- /dev/null +++ b/proofs/cbmc/kem_enc_derand_u/kem_enc_derand_u_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include + +void harness(void) +{ + uint8_t *ct_u, *ss, *sp_serial, *epp_serial; + uint8_t *seed, *hpk, *coins; + mlk_kem_enc_derand_u(ct_u, ss, sp_serial, epp_serial, seed, hpk, coins, + NULL /* context will be dropped by preprocessor */); +} diff --git a/proofs/cbmc/kem_enc_v/Makefile b/proofs/cbmc/kem_enc_v/Makefile new file mode 100644 index 0000000000..09d25f0341 --- /dev/null +++ b/proofs/cbmc/kem_enc_v/Makefile @@ -0,0 +1,44 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = kem_enc_v_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = mlk_enc_v + +DEFINES += -DMLK_CONFIG_ENABLE_MLKEM_BRAID +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_enc_v +USE_FUNCTION_CONTRACTS = mlk_indcpa_enc_v +USE_FUNCTION_CONTRACTS += mlk_polyvec_frombytes +USE_FUNCTION_CONTRACTS += mlk_polyvec_reduce +USE_FUNCTION_CONTRACTS += mlk_polyvec_tobytes +USE_FUNCTION_CONTRACTS += mlk_deserialize_epp +USE_FUNCTION_CONTRACTS += mlk_deserialize_polyvec_16le +USE_FUNCTION_CONTRACTS += mlk_polyvec_mulcache_compute +USE_FUNCTION_CONTRACTS += mlk_ct_memcmp +USE_FUNCTION_CONTRACTS += mlk_zeroize +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_smt_only --z3 + +FUNCTION_NAME = mlk_enc_v + +# This function is large enough to need... +CBMC_OBJECT_BITS = 12 + +include ../Makefile.common diff --git a/proofs/cbmc/kem_enc_v/kem_enc_v_harness.c b/proofs/cbmc/kem_enc_v/kem_enc_v_harness.c new file mode 100644 index 0000000000..a667fdd9c3 --- /dev/null +++ b/proofs/cbmc/kem_enc_v/kem_enc_v_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include + +void harness(void) +{ + uint8_t *ct_v, *sp_serial, *epp_serial; + uint8_t *coins, *ek_vector; + mlk_kem_enc_v(ct_v, sp_serial, epp_serial, coins, ek_vector, + NULL /* context will be dropped by preprocessor */); +} diff --git a/proofs/cbmc/mlkem_native_config_cbmc.h b/proofs/cbmc/mlkem_native_config_cbmc.h index e7272221d1..af9b87624b 100644 --- a/proofs/cbmc/mlkem_native_config_cbmc.h +++ b/proofs/cbmc/mlkem_native_config_cbmc.h @@ -153,6 +153,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/proofs/cbmc/serialize_epp/Makefile b/proofs/cbmc/serialize_epp/Makefile new file mode 100644 index 0000000000..cefa72cc17 --- /dev/null +++ b/proofs/cbmc/serialize_epp/Makefile @@ -0,0 +1,36 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = serialize_epp_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = mlk_serialize_epp + +DEFINES += -DMLK_CONFIG_ENABLE_MLKEM_BRAID +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_serialize_epp +USE_FUNCTION_CONTRACTS = +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = mlk_serialize_epp + +# This function is large enough to need... +CBMC_OBJECT_BITS = 12 + +include ../Makefile.common diff --git a/proofs/cbmc/serialize_epp/serialize_epp_harness.c b/proofs/cbmc/serialize_epp/serialize_epp_harness.c new file mode 100644 index 0000000000..64cd383beb --- /dev/null +++ b/proofs/cbmc/serialize_epp/serialize_epp_harness.c @@ -0,0 +1,21 @@ +// Copyright (c) The mlkem-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include +#include + +#define mlk_serialize_epp MLK_NAMESPACE(serialize_epp) +void mlk_serialize_epp(uint8_t out[MLKEM_EPP_BYTES], const mlk_poly *p); + +void harness(void) +{ + { + /* Dummy use of `free` to work around CBMC issue #8814. */ + free(NULL); + } + + uint8_t *out; + mlk_poly *p; + + mlk_serialize_epp(out, p); +} diff --git a/proofs/cbmc/serialize_polyvec_16le/Makefile b/proofs/cbmc/serialize_polyvec_16le/Makefile new file mode 100644 index 0000000000..2f69562b5c --- /dev/null +++ b/proofs/cbmc/serialize_polyvec_16le/Makefile @@ -0,0 +1,36 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = serialize_polyvec_16le_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = mlk_serialize_polyvec_16le + +DEFINES += -DMLK_CONFIG_ENABLE_MLKEM_BRAID +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_serialize_polyvec_16le +USE_FUNCTION_CONTRACTS = +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = mlk_serialize_polyvec_16le + +# This function is large enough to need... +CBMC_OBJECT_BITS = 12 + +include ../Makefile.common diff --git a/proofs/cbmc/serialize_polyvec_16le/serialize_polyvec_16le_harness.c b/proofs/cbmc/serialize_polyvec_16le/serialize_polyvec_16le_harness.c new file mode 100644 index 0000000000..e1fa5e238d --- /dev/null +++ b/proofs/cbmc/serialize_polyvec_16le/serialize_polyvec_16le_harness.c @@ -0,0 +1,22 @@ +// Copyright (c) The mlkem-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include +#include + +#define mlk_serialize_polyvec_16le MLK_NAMESPACE(serialize_polyvec_16le) +void mlk_serialize_polyvec_16le(uint8_t out[MLKEM_POLYVEC16_BYTES], + const mlk_polyvec *v); + +void harness(void) +{ + { + /* Dummy use of `free` to work around CBMC issue #8814. */ + free(NULL); + } + + uint8_t *out; + mlk_polyvec *v; + + mlk_serialize_polyvec_16le(out, v); +} diff --git a/test/configs/break_pct_config.h b/test/configs/break_pct_config.h index b955b63081..238a4e9a2a 100644 --- a/test/configs/break_pct_config.h +++ b/test/configs/break_pct_config.h @@ -152,6 +152,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/configs.yml b/test/configs/configs.yml index 8ad847f82c..63ed56501c 100644 --- a/test/configs/configs.yml +++ b/test/configs/configs.yml @@ -465,3 +465,11 @@ configs: #endif /* !__ASSEMBLER__ */ MLK_CONFIG_FILE: comment: "/* No need to set this -- we _are_ already in a custom config */" + + - path: test/configs/test_mlkem_braid_config.h + description: "Enable ML-KEM Braid API" + defines: + MLK_CONFIG_NAMESPACE_PREFIX: mlk + MLK_CONFIG_ENABLE_MLKEM_BRAID: true + MLK_CONFIG_FILE: + comment: "/* No need to set this -- we _are_ already in a custom config */" diff --git a/test/configs/custom_heap_alloc_config.h b/test/configs/custom_heap_alloc_config.h index b4aa854b16..0e77433409 100644 --- a/test/configs/custom_heap_alloc_config.h +++ b/test/configs/custom_heap_alloc_config.h @@ -151,6 +151,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/custom_memcpy_config.h b/test/configs/custom_memcpy_config.h index 74fcdbf413..3d431272f6 100644 --- a/test/configs/custom_memcpy_config.h +++ b/test/configs/custom_memcpy_config.h @@ -151,6 +151,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/custom_memset_config.h b/test/configs/custom_memset_config.h index 3d783454b7..0ec47ccce5 100644 --- a/test/configs/custom_memset_config.h +++ b/test/configs/custom_memset_config.h @@ -151,6 +151,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/custom_native_capability_config_0.h b/test/configs/custom_native_capability_config_0.h index d0c05a1780..4cb83f5195 100644 --- a/test/configs/custom_native_capability_config_0.h +++ b/test/configs/custom_native_capability_config_0.h @@ -152,6 +152,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/custom_native_capability_config_1.h b/test/configs/custom_native_capability_config_1.h index 5b72911f6b..ee2f245ed7 100644 --- a/test/configs/custom_native_capability_config_1.h +++ b/test/configs/custom_native_capability_config_1.h @@ -152,6 +152,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/custom_native_capability_config_CPUID_AVX2.h b/test/configs/custom_native_capability_config_CPUID_AVX2.h index afde1e7d81..8e473ec061 100644 --- a/test/configs/custom_native_capability_config_CPUID_AVX2.h +++ b/test/configs/custom_native_capability_config_CPUID_AVX2.h @@ -152,6 +152,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/custom_native_capability_config_ID_AA64PFR1_EL1.h b/test/configs/custom_native_capability_config_ID_AA64PFR1_EL1.h index 72ce101048..77683c12e6 100644 --- a/test/configs/custom_native_capability_config_ID_AA64PFR1_EL1.h +++ b/test/configs/custom_native_capability_config_ID_AA64PFR1_EL1.h @@ -152,6 +152,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/custom_randombytes_config.h b/test/configs/custom_randombytes_config.h index 093503eb8e..39568dcf7e 100644 --- a/test/configs/custom_randombytes_config.h +++ b/test/configs/custom_randombytes_config.h @@ -151,6 +151,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/custom_stdlib_config.h b/test/configs/custom_stdlib_config.h index 0e06730688..b5065a710c 100644 --- a/test/configs/custom_stdlib_config.h +++ b/test/configs/custom_stdlib_config.h @@ -152,6 +152,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/custom_zeroize_config.h b/test/configs/custom_zeroize_config.h index ea7f4194bb..c16eecfffb 100644 --- a/test/configs/custom_zeroize_config.h +++ b/test/configs/custom_zeroize_config.h @@ -151,6 +151,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/no_asm_config.h b/test/configs/no_asm_config.h index 7c5ca7f50e..37b015fc7d 100644 --- a/test/configs/no_asm_config.h +++ b/test/configs/no_asm_config.h @@ -152,6 +152,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/serial_fips202_config.h b/test/configs/serial_fips202_config.h index 4f6a171446..7bf42de8ad 100644 --- a/test/configs/serial_fips202_config.h +++ b/test/configs/serial_fips202_config.h @@ -151,6 +151,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/test_alloc_config.h b/test/configs/test_alloc_config.h index 55daffc0ca..7aedce3e3f 100644 --- a/test/configs/test_alloc_config.h +++ b/test/configs/test_alloc_config.h @@ -154,6 +154,16 @@ */ /* #define MLK_CONFIG_CONSTANTS_ONLY */ +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +/* #define MLK_CONFIG_ENABLE_MLKEM_BRAID */ + /****************************************************************************** * * Build-only configuration options diff --git a/test/configs/test_mlkem_braid_config.h b/test/configs/test_mlkem_braid_config.h new file mode 100644 index 0000000000..23e2f16fd2 --- /dev/null +++ b/test/configs/test_mlkem_braid_config.h @@ -0,0 +1,670 @@ +/* + * Copyright (c) The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + */ + +/* References + * ========== + * + * - [FIPS140_3_IG] + * Implementation Guidance for FIPS 140-3 and the Cryptographic Module + * Validation Program + * National Institute of Standards and Technology + * https://csrc.nist.gov/projects/cryptographic-module-validation-program/fips-140-3-ig-announcements + * + * - [FIPS203] + * FIPS 203 Module-Lattice-Based Key-Encapsulation Mechanism Standard + * National Institute of Standards and Technology + * https://csrc.nist.gov/pubs/fips/203/final + */ + +/* + * WARNING: This file is auto-generated from scripts/autogen + * in the mlkem-native repository. + * Do not modify it directly. + */ + +/* + * Test configuration: Enable ML-KEM Braid API + * + * This configuration differs from the default mlkem/mlkem_native_config.h in + * the following places: + * - MLK_CONFIG_NAMESPACE_PREFIX + * - MLK_CONFIG_ENABLE_MLKEM_BRAID + */ + + +#ifndef MLK_CONFIG_H +#define MLK_CONFIG_H + +/** + * Specifies the parameter set for ML-KEM: + * - MLK_CONFIG_PARAMETER_SET=512 corresponds to ML-KEM-512 + * - MLK_CONFIG_PARAMETER_SET=768 corresponds to ML-KEM-768 + * - MLK_CONFIG_PARAMETER_SET=1024 corresponds to ML-KEM-1024 + * + * If you want to support multiple parameter sets, build the library multiple + * times and set MLK_CONFIG_MULTILEVEL_BUILD. See MLK_CONFIG_MULTILEVEL_BUILD + * for how to do this while minimizing code duplication. + * + * This can also be set using CFLAGS. + */ +#ifndef MLK_CONFIG_PARAMETER_SET +#define MLK_CONFIG_PARAMETER_SET \ + 768 /* Change this for different security strengths */ +#endif + +/** + * MLK_CONFIG_FILE + * + * If defined, this is a header that will be included instead of the default + * configuration file mlkem/mlkem_native_config.h. + * + * When you need to build mlkem-native in multiple configurations, using + * varying MLK_CONFIG_FILE can be more convenient than configuring everything + * through CFLAGS. + * + * To use, MLK_CONFIG_FILE _must_ be defined prior to the inclusion of any + * mlkem-native headers. For example, it can be set by passing + * `-DMLK_CONFIG_FILE="..."` on the command line. + */ +/* No need to set this -- we _are_ already in a custom config */ +/* #define MLK_CONFIG_FILE "mlkem_native_config.h" */ + +/** + * The prefix to use to namespace global symbols from mlkem/. + * + * In a multi-level build, level-dependent symbols will additionally be + * prefixed with the parameter set (512/768/1024). + * + * This can also be set using CFLAGS. + */ +#define MLK_CONFIG_NAMESPACE_PREFIX mlk + +/** + * MLK_CONFIG_MULTILEVEL_BUILD + * + * Set this if the build is part of a multi-level build supporting multiple + * parameter sets. + * + * If you need only a single parameter set, keep this unset. + * + * To build mlkem-native with support for all parameter sets, build it three + * times -- once per parameter set -- and set the option + * MLK_CONFIG_MULTILEVEL_WITH_SHARED for exactly one of them, and + * MLK_CONFIG_MULTILEVEL_NO_SHARED for the others. + * MLK_CONFIG_MULTILEVEL_BUILD should be set for all of them. + * + * See examples/multilevel_build for an example. + * + * This can also be set using CFLAGS. + */ +/* #define MLK_CONFIG_MULTILEVEL_BUILD */ + +/** + * MLK_CONFIG_EXTERNAL_API_QUALIFIER + * + * If set, this option provides an additional function qualifier to be added + * to declarations of mlkem-native's public API. + * + * The primary use case for this option are single-CU builds where the public + * API exposed by mlkem-native is wrapped by another API in the consuming + * application. In this case, even mlkem-native's public API can be marked + * `static`. + */ +/* #define MLK_CONFIG_EXTERNAL_API_QUALIFIER */ + +/** + * MLK_CONFIG_NO_RANDOMIZED_API + * + * If this option is set, mlkem-native will be built without the randomized + * API functions (crypto_kem_keypair and crypto_kem_enc). This allows users + * to build mlkem-native without providing a randombytes() implementation + * if they only need the deterministic API (crypto_kem_keypair_derand, + * crypto_kem_enc_derand, crypto_kem_dec). + * + * @note This option is incompatible with MLK_CONFIG_KEYGEN_PCT as the + * current PCT implementation requires crypto_kem_enc(). + */ +/* #define MLK_CONFIG_NO_RANDOMIZED_API */ + +/** + * MLK_CONFIG_NO_SUPERCOP + * + * By default, mlkem_native.h exposes the mlkem-native API in the SUPERCOP + * naming convention (crypto_kem_xxx). If you don't need this, set + * MLK_CONFIG_NO_SUPERCOP. + * + * @note You must set this for a multi-level build as the SUPERCOP naming + * does not disambiguate between the parameter sets. + */ +/* #define MLK_CONFIG_NO_SUPERCOP */ + +/** + * MLK_CONFIG_CONSTANTS_ONLY + * + * If you only need the size constants (MLKEM_PUBLICKEYBYTES, etc.) but no + * function declarations, set MLK_CONFIG_CONSTANTS_ONLY. + * + * This only affects the public header mlkem_native.h, not the + * implementation. + */ +/* #define MLK_CONFIG_CONSTANTS_ONLY */ + +/****************************************************************************** + * Name: MLK_CONFIG_ENABLE_MLKEM_BRAID + * + * Description: If this option is set, mlkem-native exposes the incremental + * encapsulation API (mlk_kem_enc_derand_u, mlk_kem_enc_v) + * needed for the ML-KEM Braid protocol. + * + *****************************************************************************/ +#define MLK_CONFIG_ENABLE_MLKEM_BRAID + +/****************************************************************************** + * + * Build-only configuration options + * + * The remaining configurations are build-options only. + * They do not affect the API described in mlkem_native.h. + * + *****************************************************************************/ + +#if defined(MLK_BUILD_INTERNAL) +/** + * MLK_CONFIG_MULTILEVEL_WITH_SHARED + * + * This is for multi-level builds of mlkem-native only. If you need only a + * single parameter set, keep this unset. + * + * If this is set, all MLK_CONFIG_PARAMETER_SET-independent code will be + * included in the build, including code needed only for other parameter + * sets. + * + * Example: mlk_poly_cbd3 is only needed for MLK_CONFIG_PARAMETER_SET == 512. + * Yet, if this option is set for a build with + * MLK_CONFIG_PARAMETER_SET == 768/1024, it would be included. + * + * To build mlkem-native with support for all parameter sets, build it three + * times -- once per parameter set -- and set the option + * MLK_CONFIG_MULTILEVEL_WITH_SHARED for exactly one of them, and + * MLK_CONFIG_MULTILEVEL_NO_SHARED for the others. + * MLK_CONFIG_MULTILEVEL_BUILD should be set for all of them. + * + * See examples/multilevel_build for an example. + * + * This can also be set using CFLAGS. + */ +/* #define MLK_CONFIG_MULTILEVEL_WITH_SHARED */ + +/** + * MLK_CONFIG_MULTILEVEL_NO_SHARED + * + * This is for multi-level builds of mlkem-native only. If you need only a + * single parameter set, keep this unset. + * + * If this is set, no MLK_CONFIG_PARAMETER_SET-independent code will be + * included in the build. + * + * To build mlkem-native with support for all parameter sets, build it three + * times -- once per parameter set -- and set the option + * MLK_CONFIG_MULTILEVEL_WITH_SHARED for exactly one of them, and + * MLK_CONFIG_MULTILEVEL_NO_SHARED for the others. + * MLK_CONFIG_MULTILEVEL_BUILD should be set for all of them. + * + * See examples/multilevel_build for an example. + * + * This can also be set using CFLAGS. + */ +/* #define MLK_CONFIG_MULTILEVEL_NO_SHARED */ + +/** + * MLK_CONFIG_MONOBUILD_KEEP_SHARED_HEADERS + * + * This is only relevant for single compilation unit (SCU) builds of + * mlkem-native. In this case, it determines whether directives defined in + * parameter-set-independent headers should be #undef'ined or not at the + * end of the SCU file. This is needed in multilevel builds. + * + * See examples/multilevel_build_native for an example. + * + * This can also be set using CFLAGS. + */ +/* #define MLK_CONFIG_MONOBUILD_KEEP_SHARED_HEADERS */ + +/** + * MLK_CONFIG_USE_NATIVE_BACKEND_ARITH + * + * Determines whether a native arithmetic backend should be used. + * + * The arithmetic backend covers performance-critical functions such as the + * number-theoretic transform (NTT). + * + * If this option is unset, the C backend will be used. + * + * If this option is set, the arithmetic backend to be used is determined + * by MLK_CONFIG_ARITH_BACKEND_FILE: if the latter is unset, the default + * backend for the target architecture will be used. If set, it must be the + * name of a backend metadata file. + * + * This can also be set using CFLAGS. + */ +#if !defined(MLK_CONFIG_USE_NATIVE_BACKEND_ARITH) +/* #define MLK_CONFIG_USE_NATIVE_BACKEND_ARITH */ +#endif + +/** + * MLK_CONFIG_ARITH_BACKEND_FILE + * + * The arithmetic backend to use. + * + * If MLK_CONFIG_USE_NATIVE_BACKEND_ARITH is unset, this option is ignored. + * + * If MLK_CONFIG_USE_NATIVE_BACKEND_ARITH is set, this option must either + * be undefined or the filename of an arithmetic backend. If unset, the + * default backend will be used. + * + * This can be set using CFLAGS. + */ +#if defined(MLK_CONFIG_USE_NATIVE_BACKEND_ARITH) && \ + !defined(MLK_CONFIG_ARITH_BACKEND_FILE) +#define MLK_CONFIG_ARITH_BACKEND_FILE "native/meta.h" +#endif + +/** + * MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 + * + * Determines whether a native FIPS202 backend should be used. + * + * The FIPS202 backend covers 1x/2x/4x-fold Keccak-f1600, which is the + * performance bottleneck of SHA3 and SHAKE. + * + * If this option is unset, the C backend will be used. + * + * If this option is set, the FIPS202 backend to be used is determined by + * MLK_CONFIG_FIPS202_BACKEND_FILE: if the latter is unset, the default + * backend for the target architecture will be used. If set, it must be + * the name of a backend metadata file. + * + * This can also be set using CFLAGS. + */ +#if !defined(MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202) +/* #define MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 */ +#endif + +/** + * MLK_CONFIG_FIPS202_BACKEND_FILE + * + * The FIPS-202 backend to use. + * + * If MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 is set, this option must either + * be undefined or the filename of a FIPS202 backend. If unset, the default + * backend will be used. + * + * This can be set using CFLAGS. + */ +#if defined(MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202) && \ + !defined(MLK_CONFIG_FIPS202_BACKEND_FILE) +#define MLK_CONFIG_FIPS202_BACKEND_FILE "fips202/native/auto.h" +#endif + +/** + * MLK_CONFIG_FIPS202_CUSTOM_HEADER + * + * Custom header to use for FIPS-202. + * + * This should only be set if you intend to use a custom FIPS-202 + * implementation, different from the one shipped with mlkem-native. + * + * If set, it must be the name of a file serving as the replacement for + * mlkem/fips202/fips202.h, and exposing the same API (see FIPS202.md). + */ +/* #define MLK_CONFIG_FIPS202_CUSTOM_HEADER "SOME_FILE.h" */ + +/** + * MLK_CONFIG_FIPS202X4_CUSTOM_HEADER + * + * Custom header to use for FIPS-202-X4. + * + * This should only be set if you intend to use a custom FIPS-202 + * implementation, different from the one shipped with mlkem-native. + * + * If set, it must be the name of a file serving as the replacement for + * mlkem/fips202/fips202x4.h, and exposing the same API (see FIPS202.md). + */ +/* #define MLK_CONFIG_FIPS202X4_CUSTOM_HEADER "SOME_FILE.h" */ + +/** + * MLK_CONFIG_CUSTOM_ZEROIZE + * + * In compliance with @[FIPS203, Section 3.3], mlkem-native zeroizes + * intermediate stack buffers before returning from function calls. + * + * Set this option and define `mlk_zeroize` if you want to use a custom + * method to zeroize intermediate stack buffers. The default implementation + * uses SecureZeroMemory on Windows and a memset + compiler barrier + * otherwise. If neither of those is available on the target platform, + * compilation will fail, and you will need to use MLK_CONFIG_CUSTOM_ZEROIZE + * to provide a custom implementation of `mlk_zeroize()`. + * + * @warning The explicit stack zeroization conducted by mlkem-native reduces + * the likelihood of data leaking on the stack, but does not + * eliminate it. The C standard makes no guarantee about where a + * compiler allocates structures and whether/where it makes copies + * of them. Also, in addition to entire structures, there may also + * be potentially exploitable leakage of individual values on the + * stack. If you need bullet-proof zeroization of the stack, you + * need to consider additional measures instead of what this + * feature provides. In this case, you can set mlk_zeroize to a + * no-op. + */ +/* #define MLK_CONFIG_CUSTOM_ZEROIZE + #if !defined(__ASSEMBLER__) + #include + #include "src/sys.h" + static MLK_INLINE void mlk_zeroize(void *ptr, size_t len) + { + ... your implementation ... + } + #endif +*/ + +/** + * MLK_CONFIG_CUSTOM_RANDOMBYTES + * + * mlkem-native does not provide a secure randombytes implementation. Such + * an implementation has to be provided by the consumer. + * + * If this option is not set, mlkem-native expects a function + * int randombytes(uint8_t *out, size_t outlen). It is expected to return + * zero on success, and non-zero on failure. In case of failure, the + * top-level APIs will return an MLK_ERR_RNG_FAIL error code. + * + * Set this option and define `mlk_randombytes` (with the same signature + * and behaviour) if you want to use a custom method to sample randombytes + * with a different name or signature. + */ +/* #define MLK_CONFIG_CUSTOM_RANDOMBYTES + #if !defined(__ASSEMBLER__) + #include + #include "src/sys.h" + static MLK_INLINE int mlk_randombytes(uint8_t *ptr, size_t len) + { + ... your implementation ... + return 0; + } + #endif +*/ + +/** + * MLK_CONFIG_CUSTOM_CAPABILITY_FUNC + * + * mlkem-native backends may rely on specific hardware features. Those + * backends will only be included in an mlkem-native build if support for + * the respective features is enabled at compile-time. However, when + * building for a heterogeneous set of CPUs to run the resulting + * binary/library on, feature detection at _runtime_ is needed to decide + * whether a backend can be used or not. + * + * Set this option and define `mlk_sys_check_capability` if you want to + * use a custom method to dispatch between implementations. + * + * If this option is not set, mlkem-native uses compile-time feature + * detection only to decide which backend to use. + * + * If you compile mlkem-native on a system with different capabilities + * than the system that the resulting binary/library will be run on, you + * must use this option. + */ +/* #define MLK_CONFIG_CUSTOM_CAPABILITY_FUNC + static MLK_INLINE int mlk_sys_check_capability(mlk_sys_cap cap) + __contract__( + ensures(return_value == 0 || return_value == 1) + ) + { + ... your implementation ... + } +*/ + +/** + * MLK_CONFIG_CUSTOM_ALLOC_FREE [EXPERIMENTAL] + * + * Set this option and define `MLK_CUSTOM_ALLOC` and `MLK_CUSTOM_FREE` if + * you want to use custom allocation for large local structures or buffers. + * + * By default, all buffers/structures are allocated on the stack. If this + * option is set, most of them will be allocated via MLK_CUSTOM_ALLOC. + * + * Parameters to MLK_CUSTOM_ALLOC: + * - T* v: Target pointer to declare. + * - T: Type of structure to be allocated. + * - N: Number of elements to be allocated. + * + * Parameters to MLK_CUSTOM_FREE: + * - T* v: Target pointer to free. May be NULL. + * - T: Type of structure to be freed. + * - N: Number of elements to be freed. + * + * @warning This option is experimental. Its scope, configuration and + * function/macro signatures may change at any time. We expect a + * stable API for v2. + * + * @note Even if this option is set, some allocations further down the call + * stack will still be made from the stack, consuming up to 3KB of + * stack space. Those will likely be added to the scope of this + * option in the future. + * + * @note MLK_CUSTOM_ALLOC need not guarantee a successful allocation nor + * include error handling. Upon failure, the target pointer should + * simply be set to NULL. The calling code will handle this case and + * invoke MLK_CUSTOM_FREE. + */ +/* #define MLK_CONFIG_CUSTOM_ALLOC_FREE + #if !defined(__ASSEMBLER__) + #include + #define MLK_CUSTOM_ALLOC(v, T, N) \ + T* (v) = (T *)aligned_alloc(MLK_DEFAULT_ALIGN, \ + MLK_ALIGN_UP(sizeof(T) * (N))) + #define MLK_CUSTOM_FREE(v, T, N) free(v) + #endif +*/ + +/** + * MLK_CONFIG_CUSTOM_MEMCPY + * + * Set this option and define `mlk_memcpy` if you want to use a custom + * method to copy memory instead of the standard library memcpy function. + * + * The custom implementation must have the same signature and behavior as + * the standard memcpy function: + * void *mlk_memcpy(void *dest, const void *src, size_t n) + */ +/* #define MLK_CONFIG_CUSTOM_MEMCPY + #if !defined(__ASSEMBLER__) + #include + #include "src/sys.h" + static MLK_INLINE void *mlk_memcpy(void *dest, const void *src, size_t n) + { + ... your implementation ... + } + #endif +*/ + +/** + * MLK_CONFIG_CUSTOM_MEMSET + * + * Set this option and define `mlk_memset` if you want to use a custom + * method to set memory instead of the standard library memset function. + * + * The custom implementation must have the same signature and behavior as + * the standard memset function: + * void *mlk_memset(void *s, int c, size_t n) + */ +/* #define MLK_CONFIG_CUSTOM_MEMSET + #if !defined(__ASSEMBLER__) + #include + #include "src/sys.h" + static MLK_INLINE void *mlk_memset(void *s, int c, size_t n) + { + ... your implementation ... + } + #endif +*/ + +/** + * MLK_CONFIG_INTERNAL_API_QUALIFIER + * + * If set, this option provides an additional qualifier to be added to + * declarations of internal API functions and data. + * + * The primary use case for this option are single-CU builds, in which case + * this option can be set to `static`. + */ +/* #define MLK_CONFIG_INTERNAL_API_QUALIFIER */ + +/** + * MLK_CONFIG_CT_TESTING_ENABLED + * + * If set, mlkem-native annotates data as secret/public using valgrind's + * annotations VALGRIND_MAKE_MEM_UNDEFINED and VALGRIND_MAKE_MEM_DEFINED, + * enabling various checks for secret-dependent control flow or + * variable-time execution (depending on the exact version of valgrind + * installed). + */ +/* #define MLK_CONFIG_CT_TESTING_ENABLED */ + +/** + * MLK_CONFIG_NO_ASM + * + * If this option is set, mlkem-native will be built without use of native + * code or inline assembly. + * + * By default, inline assembly is used to implement value barriers. Without + * inline assembly, mlkem-native will use a global volatile 'opt blocker' + * instead; see verify.h. + * + * Inline assembly is also used to implement a secure zeroization function + * on non-Windows platforms. If this option is set and the target platform + * is not Windows, you MUST set MLK_CONFIG_CUSTOM_ZEROIZE and provide a + * custom zeroization function. + * + * If this option is set, MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 and + * MLK_CONFIG_USE_NATIVE_BACKEND_ARITH will be ignored, and no native + * backends will be used. + */ +/* #define MLK_CONFIG_NO_ASM */ + +/** + * MLK_CONFIG_NO_ASM_VALUE_BARRIER + * + * If this option is set, mlkem-native will be built without use of native + * code or inline assembly for value barriers. + * + * By default, inline assembly (if available) is used to implement value + * barriers. Without inline assembly, mlkem-native will use a global + * volatile 'opt blocker' instead; see verify.h. + */ +/* #define MLK_CONFIG_NO_ASM_VALUE_BARRIER */ + +/** + * MLK_CONFIG_KEYGEN_PCT + * + * Compliance with @[FIPS140_3_IG, p.87] requires a Pairwise Consistency + * Test (PCT) to be carried out on a freshly generated keypair before it + * can be exported. + * + * Set this option if such a check should be implemented. In this case, + * crypto_kem_keypair_derand and crypto_kem_keypair will return a non-zero + * error code if the PCT failed. + * + * @note This feature will drastically lower the performance of key + * generation. + */ +/* #define MLK_CONFIG_KEYGEN_PCT */ + +/** + * MLK_CONFIG_KEYGEN_PCT_BREAKAGE_TEST + * + * If this option is set, the user must provide a runtime function + * `static inline int mlk_break_pct() { ... }` to indicate whether the PCT + * should be made to fail. + * + * This option only has an effect if MLK_CONFIG_KEYGEN_PCT is set. + */ +/* #define MLK_CONFIG_KEYGEN_PCT_BREAKAGE_TEST + #if !defined(__ASSEMBLER__) + #include "src/sys.h" + static MLK_INLINE int mlk_break_pct(void) + { + ... return 0/1 depending on whether PCT should be broken ... + } + #endif +*/ + +/** + * MLK_CONFIG_SERIAL_FIPS202_ONLY + * + * Set this to use a FIPS202 implementation with global state that supports + * only one active Keccak computation at a time (e.g. some hardware + * accelerators). + * + * If this option is set, batched Keccak operations are disabled for + * rejection sampling during matrix generation. Instead, matrix entries + * will be generated one at a time. + * + * This allows offloading Keccak computations to a hardware accelerator + * that holds only a single Keccak state locally, rather than requiring + * support for batched (4x) Keccak states. + * + * @note Depending on the target CPU, disabling batched Keccak may reduce + * performance when using software FIPS202 implementations. Only + * enable this when you have to. + */ +/* #define MLK_CONFIG_SERIAL_FIPS202_ONLY */ + +/** + * MLK_CONFIG_CONTEXT_PARAMETER + * + * Set this to add a context parameter that is provided to public API + * functions and is then available in custom callbacks. + * + * The type of the context parameter is configured via + * MLK_CONFIG_CONTEXT_PARAMETER_TYPE. + */ +/* #define MLK_CONFIG_CONTEXT_PARAMETER */ + +/** + * MLK_CONFIG_CONTEXT_PARAMETER_TYPE + * + * Set this to define the type for the context parameter used by + * MLK_CONFIG_CONTEXT_PARAMETER. + * + * This is only relevant if MLK_CONFIG_CONTEXT_PARAMETER is set. + */ +/* #define MLK_CONFIG_CONTEXT_PARAMETER_TYPE void* */ + +/************************* Config internals ********************************/ + +#endif /* MLK_BUILD_INTERNAL */ + +/* Default namespace + * + * Don't change this. If you need a different namespace, re-define + * MLK_CONFIG_NAMESPACE_PREFIX above instead, and remove the following. + * + * The default MLKEM namespace is + * + * PQCP_MLKEM_NATIVE_MLKEM_ + * + * e.g., PQCP_MLKEM_NATIVE_MLKEM512_ + */ + +#if MLK_CONFIG_PARAMETER_SET == 512 +#define MLK_DEFAULT_NAMESPACE_PREFIX PQCP_MLKEM_NATIVE_MLKEM512 +#elif MLK_CONFIG_PARAMETER_SET == 768 +#define MLK_DEFAULT_NAMESPACE_PREFIX PQCP_MLKEM_NATIVE_MLKEM768 +#elif MLK_CONFIG_PARAMETER_SET == 1024 +#define MLK_DEFAULT_NAMESPACE_PREFIX PQCP_MLKEM_NATIVE_MLKEM1024 +#endif + +#endif /* !MLK_CONFIG_H */ diff --git a/test/src/test_mlkem.c b/test/src/test_mlkem.c index 88564b4df9..eca7c2a052 100644 --- a/test/src/test_mlkem.c +++ b/test/src/test_mlkem.c @@ -6,8 +6,9 @@ #include #include #include "../../mlkem/src/compress.h" +#include "../../mlkem/src/kem.h" +#include "../../mlkem/src/symmetric.h" -#include "../../mlkem/mlkem_native.h" #include "../notrandombytes/notrandombytes.h" #ifndef NTESTS_FUNC @@ -27,115 +28,115 @@ } while (0) -static int test_keys_core(uint8_t pk[CRYPTO_PUBLICKEYBYTES], - uint8_t sk[CRYPTO_SECRETKEYBYTES], - uint8_t ct[CRYPTO_CIPHERTEXTBYTES], - uint8_t key_a[CRYPTO_BYTES], - uint8_t key_b[CRYPTO_BYTES]) +static int test_keys_core(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES], + uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES], + uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], + uint8_t key_a[MLKEM_SSBYTES], + uint8_t key_b[MLKEM_SSBYTES]) { /* Alice generates a public key */ - CHECK(crypto_kem_keypair(pk, sk) == 0); + CHECK(mlk_kem_keypair(pk, sk, 0) == 0); /* Bob derives a secret key and creates a response */ - CHECK(crypto_kem_enc(ct, key_b, pk) == 0); + CHECK(mlk_kem_enc(ct, key_b, pk, 0) == 0); /* Alice uses Bobs response to get her shared key */ - CHECK(crypto_kem_dec(key_a, ct, sk) == 0); + CHECK(mlk_kem_dec(key_a, ct, sk, 0) == 0); /* mark as defined, so we can compare */ - MLK_CT_TESTING_DECLASSIFY(key_a, CRYPTO_BYTES); - MLK_CT_TESTING_DECLASSIFY(key_b, CRYPTO_BYTES); + MLK_CT_TESTING_DECLASSIFY(key_a, MLKEM_SSBYTES); + MLK_CT_TESTING_DECLASSIFY(key_b, MLKEM_SSBYTES); - CHECK(memcmp(key_a, key_b, CRYPTO_BYTES) == 0); + CHECK(memcmp(key_a, key_b, MLKEM_SSBYTES) == 0); return 0; } static int test_keys(void) { - uint8_t pk[CRYPTO_PUBLICKEYBYTES]; - uint8_t sk[CRYPTO_SECRETKEYBYTES]; - uint8_t ct[CRYPTO_CIPHERTEXTBYTES]; - uint8_t key_a[CRYPTO_BYTES]; - uint8_t key_b[CRYPTO_BYTES]; + uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]; + uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES]; + uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES]; + uint8_t key_a[MLKEM_SSBYTES]; + uint8_t key_b[MLKEM_SSBYTES]; return test_keys_core(pk, sk, ct, key_a, key_b); } static int test_keys_unaligned(void) { - MLK_ALIGN uint8_t pk[CRYPTO_PUBLICKEYBYTES + 1]; - MLK_ALIGN uint8_t sk[CRYPTO_SECRETKEYBYTES + 1]; - MLK_ALIGN uint8_t ct[CRYPTO_CIPHERTEXTBYTES + 1]; - MLK_ALIGN uint8_t key_a[CRYPTO_BYTES + 1]; - MLK_ALIGN uint8_t key_b[CRYPTO_BYTES + 1]; + MLK_ALIGN uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES + 1]; + MLK_ALIGN uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES + 1]; + MLK_ALIGN uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES + 1]; + MLK_ALIGN uint8_t key_a[MLKEM_SSBYTES + 1]; + MLK_ALIGN uint8_t key_b[MLKEM_SSBYTES + 1]; return test_keys_core(pk + 1, sk + 1, ct + 1, key_a + 1, key_b + 1); } static int test_invalid_pk(void) { - uint8_t pk[CRYPTO_PUBLICKEYBYTES]; - uint8_t sk[CRYPTO_SECRETKEYBYTES]; - uint8_t ct[CRYPTO_CIPHERTEXTBYTES]; - uint8_t key_b[CRYPTO_BYTES]; + uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]; + uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES]; + uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES]; + uint8_t key_b[MLKEM_SSBYTES]; /* Alice generates a public key */ - CHECK(crypto_kem_keypair(pk, sk) == 0); + CHECK(mlk_kem_keypair(pk, sk, 0) == 0); /* Bob derives a secret key and creates a response */ - CHECK(crypto_kem_enc(ct, key_b, pk) == 0); + CHECK(mlk_kem_enc(ct, key_b, pk, 0) == 0); /* set first public key coefficient to 4095 (0xFFF) */ pk[0] = 0xFF; pk[1] |= 0x0F; /* Bob derives a secret key and creates a response */ - CHECK(crypto_kem_enc(ct, key_b, pk) != 0); + CHECK(mlk_kem_enc(ct, key_b, pk, 0) != 0); return 0; } static int test_invalid_sk_a(void) { - uint8_t pk[CRYPTO_PUBLICKEYBYTES]; - uint8_t sk[CRYPTO_SECRETKEYBYTES]; - uint8_t ct[CRYPTO_CIPHERTEXTBYTES]; - uint8_t key_a[CRYPTO_BYTES]; - uint8_t key_b[CRYPTO_BYTES]; + uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]; + uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES]; + uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES]; + uint8_t key_a[MLKEM_SSBYTES]; + uint8_t key_b[MLKEM_SSBYTES]; /* Alice generates a public key */ - CHECK(crypto_kem_keypair(pk, sk) == 0); + CHECK(mlk_kem_keypair(pk, sk, 0) == 0); /* Bob derives a secret key and creates a response */ - CHECK(crypto_kem_enc(ct, key_b, pk) == 0); + CHECK(mlk_kem_enc(ct, key_b, pk, 0) == 0); /* Replace first part of secret key with random values */ CHECK(randombytes(sk, 10) == 0); /* Alice uses Bobs response to get her shared key * This should fail due to wrong sk */ - CHECK(crypto_kem_dec(key_a, ct, sk) == 0); + CHECK(mlk_kem_dec(key_a, ct, sk, 0) == 0); /* mark as defined, so we can compare */ - MLK_CT_TESTING_DECLASSIFY(key_a, CRYPTO_BYTES); - MLK_CT_TESTING_DECLASSIFY(key_b, CRYPTO_BYTES); + MLK_CT_TESTING_DECLASSIFY(key_a, MLKEM_SSBYTES); + MLK_CT_TESTING_DECLASSIFY(key_b, MLKEM_SSBYTES); - CHECK(memcmp(key_a, key_b, CRYPTO_BYTES) != 0); + CHECK(memcmp(key_a, key_b, MLKEM_SSBYTES) != 0); return 0; } static int test_invalid_sk_b(void) { - uint8_t pk[CRYPTO_PUBLICKEYBYTES]; - uint8_t sk[CRYPTO_SECRETKEYBYTES]; - uint8_t ct[CRYPTO_CIPHERTEXTBYTES]; - uint8_t key_a[CRYPTO_BYTES]; - uint8_t key_b[CRYPTO_BYTES]; + uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]; + uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES]; + uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES]; + uint8_t key_a[MLKEM_SSBYTES]; + uint8_t key_b[MLKEM_SSBYTES]; /* Alice generates a public key */ - CHECK(crypto_kem_keypair(pk, sk) == 0); + CHECK(mlk_kem_keypair(pk, sk, 0) == 0); /* Bob derives a secret key and creates a response */ - CHECK(crypto_kem_enc(ct, key_b, pk) == 0); + CHECK(mlk_kem_enc(ct, key_b, pk, 0) == 0); /* Replace H(pk) with radom values; */ - CHECK(randombytes(sk + CRYPTO_SECRETKEYBYTES - 64, 32) == 0); + CHECK(randombytes(sk + MLKEM_INDCCA_SECRETKEYBYTES - 64, 32) == 0); /* Alice uses Bobs response to get her shared key * This should fail due to the input validation */ - CHECK(crypto_kem_dec(key_a, ct, sk) != 0); + CHECK(mlk_kem_dec(key_a, ct, sk, 0) != 0); return 0; } static int test_invalid_ciphertext(void) { - uint8_t pk[CRYPTO_PUBLICKEYBYTES]; - uint8_t sk[CRYPTO_SECRETKEYBYTES]; - uint8_t ct[CRYPTO_CIPHERTEXTBYTES]; - uint8_t key_a[CRYPTO_BYTES]; - uint8_t key_b[CRYPTO_BYTES]; + uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]; + uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES]; + uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES]; + uint8_t key_a[MLKEM_SSBYTES]; + uint8_t key_b[MLKEM_SSBYTES]; uint8_t b; size_t pos; @@ -146,20 +147,92 @@ static int test_invalid_ciphertext(void) CHECK(randombytes((uint8_t *)&pos, sizeof(size_t)) == 0); /* Alice generates a public key */ - CHECK(crypto_kem_keypair(pk, sk) == 0); + CHECK(mlk_kem_keypair(pk, sk, 0) == 0); /* Bob derives a secret key and creates a response */ - CHECK(crypto_kem_enc(ct, key_b, pk) == 0); + CHECK(mlk_kem_enc(ct, key_b, pk, 0) == 0); /* Change some byte in the ciphertext (i.e., encapsulated key) */ - ct[pos % CRYPTO_CIPHERTEXTBYTES] ^= b; + ct[pos % MLKEM_INDCCA_CIPHERTEXTBYTES] ^= b; /* Alice uses Bobs response to get her shared key */ - CHECK(crypto_kem_dec(key_a, ct, sk) == 0); + CHECK(mlk_kem_dec(key_a, ct, sk, 0) == 0); /* mark as defined, so we can compare */ - MLK_CT_TESTING_DECLASSIFY(key_a, CRYPTO_BYTES); - MLK_CT_TESTING_DECLASSIFY(key_b, CRYPTO_BYTES); - CHECK(memcmp(key_a, key_b, CRYPTO_BYTES) != 0); + MLK_CT_TESTING_DECLASSIFY(key_a, MLKEM_SSBYTES); + MLK_CT_TESTING_DECLASSIFY(key_b, MLKEM_SSBYTES); + CHECK(memcmp(key_a, key_b, MLKEM_SSBYTES) != 0); return 0; } +#if defined(MLK_CONFIG_ENABLE_MLKEM_BRAID) +static int test_incremental_enc(void) +{ + uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]; + uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES]; + uint8_t ct_ref[MLKEM_INDCCA_CIPHERTEXTBYTES]; + uint8_t ss_ref[MLKEM_SSBYTES]; + uint8_t keygen_coins[2 * MLKEM_SYMBYTES]; + uint8_t enc_coins[MLKEM_SYMBYTES]; + + /* Incremental outputs */ + uint8_t ct_u[MLKEM_POLYVECCOMPRESSEDBYTES_DU]; + uint8_t ct_v[MLKEM_POLYCOMPRESSEDBYTES_DV]; + uint8_t ss[MLKEM_SSBYTES]; + uint8_t sp_serial[MLKEM_POLYVEC16_BYTES]; + uint8_t epp_serial[MLKEM_EPP_BYTES]; + + uint8_t hpk[MLKEM_SYMBYTES]; + const uint8_t *ek_vector; + const uint8_t *ek_seed; + + /* Generate deterministic coins */ + CHECK(randombytes(keygen_coins, 2 * MLKEM_SYMBYTES) == 0); + CHECK(randombytes(enc_coins, MLKEM_SYMBYTES) == 0); + + /* Standard keygen + encaps (reference) */ + CHECK(mlk_kem_keypair_derand(pk, sk, keygen_coins, 0) == 0); + CHECK(mlk_kem_enc_derand(ct_ref, ss_ref, pk, enc_coins, 0) == 0); + + /* Split pk: pk = ek_vector || ek_seed */ + ek_vector = pk; + ek_seed = pk + MLKEM_POLYVECBYTES; + + /* Compute H(pk) for incremental API */ + mlk_hash_h(hpk, pk, MLKEM_INDCCA_PUBLICKEYBYTES); + + /* Incremental encapsulation via KEM-level API */ + CHECK(mlk_kem_enc_derand_u(ct_u, ss, sp_serial, epp_serial, ek_seed, hpk, + enc_coins, 0) == 0); + CHECK(mlk_kem_enc_v(ct_v, sp_serial, epp_serial, enc_coins, ek_vector, 0) == + 0); + + /* Verify ct_u || ct_v matches reference ciphertext */ + MLK_CT_TESTING_DECLASSIFY(ct_u, MLKEM_POLYVECCOMPRESSEDBYTES_DU); + MLK_CT_TESTING_DECLASSIFY(ct_v, MLKEM_POLYCOMPRESSEDBYTES_DV); + MLK_CT_TESTING_DECLASSIFY(ct_ref, MLKEM_INDCCA_CIPHERTEXTBYTES); + + CHECK(memcmp(ct_u, ct_ref, MLKEM_POLYVECCOMPRESSEDBYTES_DU) == 0); + CHECK(memcmp(ct_v, ct_ref + MLKEM_POLYVECCOMPRESSEDBYTES_DU, + MLKEM_POLYCOMPRESSEDBYTES_DV) == 0); + + /* Verify shared secret matches */ + MLK_CT_TESTING_DECLASSIFY(ss, MLKEM_SSBYTES); + MLK_CT_TESTING_DECLASSIFY(ss_ref, MLKEM_SSBYTES); + CHECK(memcmp(ss, ss_ref, MLKEM_SSBYTES) == 0); + + /* Verify decaps works with reassembled ciphertext */ + { + uint8_t ct_combined[MLKEM_INDCCA_CIPHERTEXTBYTES]; + uint8_t ss_dec[MLKEM_SSBYTES]; + memcpy(ct_combined, ct_u, MLKEM_POLYVECCOMPRESSEDBYTES_DU); + memcpy(ct_combined + MLKEM_POLYVECCOMPRESSEDBYTES_DU, ct_v, + MLKEM_POLYCOMPRESSEDBYTES_DV); + CHECK(mlk_kem_dec(ss_dec, ct_combined, sk, 0) == 0); + MLK_CT_TESTING_DECLASSIFY(ss_dec, MLKEM_SSBYTES); + CHECK(memcmp(ss_dec, ss, MLKEM_SSBYTES) == 0); + } + + return 0; +} +#endif /* MLK_CONFIG_ENABLE_MLKEM_BRAID */ + int main(void) { unsigned i; @@ -176,11 +249,14 @@ int main(void) CHECK(test_invalid_sk_a() == 0); CHECK(test_invalid_sk_b() == 0); CHECK(test_invalid_ciphertext() == 0); +#if defined(MLK_CONFIG_ENABLE_MLKEM_BRAID) + CHECK(test_incremental_enc() == 0); +#endif } - printf("CRYPTO_SECRETKEYBYTES: %d\n", CRYPTO_SECRETKEYBYTES); - printf("CRYPTO_PUBLICKEYBYTES: %d\n", CRYPTO_PUBLICKEYBYTES); - printf("CRYPTO_CIPHERTEXTBYTES: %d\n", CRYPTO_CIPHERTEXTBYTES); + printf("MLKEM_INDCCA_SECRETKEYBYTES: %d\n", MLKEM_INDCCA_SECRETKEYBYTES); + printf("MLKEM_INDCCA_PUBLICKEYBYTES: %d\n", MLKEM_INDCCA_PUBLICKEYBYTES); + printf("MLKEM_INDCCA_CIPHERTEXTBYTES: %d\n", MLKEM_INDCCA_CIPHERTEXTBYTES); return 0; } From e9ea4115bcad98511149204a3ed420d58e3cb875 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Thu, 18 Jun 2026 10:27:47 +0100 Subject: [PATCH 2/2] Correct namespacing definitions for mlkem braid test Signed-off-by: Rod Chapman --- test/configs/configs.yml | 1 - test/configs/test_mlkem_braid_config.h | 5 +++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/test/configs/configs.yml b/test/configs/configs.yml index 63ed56501c..06705fba88 100644 --- a/test/configs/configs.yml +++ b/test/configs/configs.yml @@ -469,7 +469,6 @@ configs: - path: test/configs/test_mlkem_braid_config.h description: "Enable ML-KEM Braid API" defines: - MLK_CONFIG_NAMESPACE_PREFIX: mlk MLK_CONFIG_ENABLE_MLKEM_BRAID: true MLK_CONFIG_FILE: comment: "/* No need to set this -- we _are_ already in a custom config */" diff --git a/test/configs/test_mlkem_braid_config.h b/test/configs/test_mlkem_braid_config.h index 23e2f16fd2..5b7eefcda1 100644 --- a/test/configs/test_mlkem_braid_config.h +++ b/test/configs/test_mlkem_braid_config.h @@ -29,7 +29,6 @@ * * This configuration differs from the default mlkem/mlkem_native_config.h in * the following places: - * - MLK_CONFIG_NAMESPACE_PREFIX * - MLK_CONFIG_ENABLE_MLKEM_BRAID */ @@ -79,7 +78,9 @@ * * This can also be set using CFLAGS. */ -#define MLK_CONFIG_NAMESPACE_PREFIX mlk +#if !defined(MLK_CONFIG_NAMESPACE_PREFIX) +#define MLK_CONFIG_NAMESPACE_PREFIX MLK_DEFAULT_NAMESPACE_PREFIX +#endif /** * MLK_CONFIG_MULTILEVEL_BUILD