diff --git a/.github/actions/config-variations/action.yml b/.github/actions/config-variations/action.yml index b776d605f..3966a33c1 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 f6e06f571..770a7b37f 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 e1249b2e5..a53513033 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 8c072921f..d5c9f63a3 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 31333aa66..23bf3bf1a 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 85adffa9b..1325b513c 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 9598cdc3e..3c2f48b8c 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 619c176b7..f7a931849 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 6be461e4d..41add6b63 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 3853806d2..ad3aa37cb 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 ac478b2ba..4f2eb38dc 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 7b731cd6a..33afaf21d 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 d5474ad77..9edc26a5e 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 2a0467f09..7bc877a80 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 000000000..a830f16dd --- /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 d8b0fd539..03d33d97d 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 9bbb3e2d5..839c4280d 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 c2edd2b16..2c7aadd84 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 e9e5b12df..8b2a907ab 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 463029bde..cc4b10a85 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 50d2b92c0..5d840c652 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 5fe5e22e9..808b56f7c 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 3c82d6df7..022564749 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 5310dc8b4..116401a86 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 000000000..f08792f8c --- /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 000000000..85d753c1e --- /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 000000000..b67c3ccc0 --- /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 000000000..03f265624 --- /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 b6233db7a..000000000 --- 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 836df9f72..000000000 --- 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 e9ac63b84..10afd2d9c 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 000000000..66ef380c8 --- /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 000000000..210f0cb36 --- /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 000000000..077c73a18 --- /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 000000000..3556db3be --- /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 000000000..1d05ff099 --- /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 000000000..f93fb97da --- /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 000000000..09d25f034 --- /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 000000000..a667fdd9c --- /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 e7272221d..af9b87624 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 000000000..cefa72cc1 --- /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 000000000..64cd383be --- /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 000000000..2f69562b5 --- /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 000000000..e1fa5e238 --- /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 b955b6308..238a4e9a2 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 8ad847f82..06705fba8 100644 --- a/test/configs/configs.yml +++ b/test/configs/configs.yml @@ -465,3 +465,10 @@ 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_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 b4aa854b1..0e7743340 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 74fcdbf41..3d431272f 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 3d783454b..0ec47ccce 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 d0c05a178..4cb83f519 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 5b72911f6..ee2f245ed 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 afde1e7d8..8e473ec06 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 72ce10104..77683c12e 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 093503eb8..39568dcf7 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 0e0673068..b5065a710 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 ea7f4194b..c16eecfff 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 7c5ca7f50..37b015fc7 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 4f6a17144..7bf42de8a 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 55daffc0c..7aedce3e3 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 000000000..5b7eefcda --- /dev/null +++ b/test/configs/test_mlkem_braid_config.h @@ -0,0 +1,671 @@ +/* + * 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_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. + */ +#if !defined(MLK_CONFIG_NAMESPACE_PREFIX) +#define MLK_CONFIG_NAMESPACE_PREFIX MLK_DEFAULT_NAMESPACE_PREFIX +#endif + +/** + * 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 88564b4df..eca7c2a05 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; }