From 51fb36c2419354aef90d75c22a1b1928d0f0df4f Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Tue, 25 Feb 2025 12:14:45 +0800 Subject: [PATCH 1/7] Extended API Signed-off-by: Matthias J. Kannwischer --- .github/workflows/integration-awslc.yml | 6 + .../monolithic_build/mlkem_native_monobuild.c | 19 ++ .../Makefile | 1 + mlkem/indcpa.c | 148 +++++----- mlkem/indcpa.h | 50 +++- mlkem/kem.c | 274 +++++++++++++++--- mlkem/kem.h | 86 ++++++ test/test_mlkem.c | 7 +- 8 files changed, 463 insertions(+), 128 deletions(-) diff --git a/.github/workflows/integration-awslc.yml b/.github/workflows/integration-awslc.yml index 72c033480..00022c11c 100644 --- a/.github/workflows/integration-awslc.yml +++ b/.github/workflows/integration-awslc.yml @@ -44,6 +44,8 @@ jobs: run: | cd $AWSLC_DIR/crypto/fipsmodule/ml_kem rm -rf mlkem + # patch mlkem_native_config.h to allow unused external API functions + sed -i.bak 's/^#define MLK_CONFIG_EXTERNAL_API_QUALIFIER static$/#define MLK_CONFIG_EXTERNAL_API_QUALIFIER static __attribute__((unused))/' mlkem_native_config.h GITHUB_REPOSITORY=$GITHUB_REPOSITORY GITHUB_SHA=$GITHUB_SHA ./importer.sh --force - name: Build+Test AWS-LC (FIPS=${{ matrix.fips }}) run: | @@ -91,6 +93,8 @@ jobs: - name: Run importer run: | cd $AWSLC_DIR/crypto/fipsmodule/ml_kem + # patch mlkem_native_config.h to allow unused external API functions + sed -i.bak 's/^#define MLK_CONFIG_EXTERNAL_API_QUALIFIER static$/#define MLK_CONFIG_EXTERNAL_API_QUALIFIER static __attribute__((unused))/' mlkem_native_config.h GITHUB_REPOSITORY=$GITHUB_REPOSITORY GITHUB_SHA=$GITHUB_SHA ./importer.sh --force - name: Run test run: | @@ -123,6 +127,8 @@ jobs: - name: Run importer run: | cd $AWSLC_DIR/crypto/fipsmodule/ml_kem + # patch mlkem_native_config.h to allow unused external API functions + sed -i.bak 's/^#define MLK_CONFIG_EXTERNAL_API_QUALIFIER static$/#define MLK_CONFIG_EXTERNAL_API_QUALIFIER static __attribute__((unused))/' mlkem_native_config.h GITHUB_REPOSITORY=$GITHUB_REPOSITORY GITHUB_SHA=$GITHUB_SHA ./importer.sh --force - name: Run test run: | diff --git a/examples/monolithic_build/mlkem_native_monobuild.c b/examples/monolithic_build/mlkem_native_monobuild.c index 9c771e736..964bce202 100644 --- a/examples/monolithic_build/mlkem_native_monobuild.c +++ b/examples/monolithic_build/mlkem_native_monobuild.c @@ -126,14 +126,33 @@ #undef mlk_indcpa_dec #undef mlk_indcpa_enc #undef mlk_indcpa_keypair_derand +#undef mlk_indcpa_marshal_pk +#undef mlk_indcpa_marshal_sk +#undef mlk_indcpa_parse_pk +#undef mlk_indcpa_parse_sk +#undef mlk_indcpa_public_key +#undef mlk_indcpa_secret_key /* mlkem/kem.h */ #undef MLK_CONFIG_API_NO_SUPERCOP #undef MLK_KEM_H #undef crypto_kem_dec +#undef crypto_kem_dec_struct #undef crypto_kem_enc #undef crypto_kem_enc_derand +#undef crypto_kem_enc_derand_struct +#undef crypto_kem_enc_struct #undef crypto_kem_keypair #undef crypto_kem_keypair_derand +#undef crypto_kem_keypair_derand_struct +#undef crypto_kem_keypair_struct +#undef crypto_kem_marshal_pk +#undef crypto_kem_marshal_sk +#undef crypto_kem_parse_pk +#undef crypto_kem_parse_sk +#undef crypto_kem_pk_from_sk +#undef crypto_kem_sk_from_seed +#undef mlk_public_key +#undef mlk_secret_key /* mlkem/mlkem_native.h */ #undef CRYPTO_BYTES #undef CRYPTO_CIPHERTEXTBYTES diff --git a/examples/monolithic_build_multilevel_native/Makefile b/examples/monolithic_build_multilevel_native/Makefile index 823dd846b..abe4894e0 100644 --- a/examples/monolithic_build_multilevel_native/Makefile +++ b/examples/monolithic_build_multilevel_native/Makefile @@ -93,6 +93,7 @@ CFLAGS := \ -Wpointer-arith \ -Wno-long-long \ -Wno-unknown-pragmas \ + -Wno-unused-function \ -Wredundant-decls \ -Wno-unused-command-line-argument \ -fomit-frame-pointer \ diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c index d0bb42588..fac97a9be 100644 --- a/mlkem/indcpa.c +++ b/mlkem/indcpa.c @@ -34,17 +34,16 @@ * This is to facilitate building multiple instances * 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) -/* End of parameter set namespacing */ +#define mlk_transpose_matrix MLK_ADD_PARAM_SET(mlk_transpose_matrix) +/* End of level namespacing */ /************************************************* - * Name: mlk_pack_pk + * Name: mlk_indcpa_marshal_pk * * Description: Serialize the public key as concatenation of the * serialized vector of polynomials pk @@ -59,16 +58,18 @@ * Implements [@FIPS203, Algorithm 13 (K-PKE.KeyGen), L19] * **************************************************/ -static void mlk_pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], mlk_polyvec pk, - const uint8_t seed[MLKEM_SYMBYTES]) +MLK_INTERNAL_API +void mlk_indcpa_marshal_pk(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], + const mlk_indcpa_public_key *pks) { - mlk_assert_bound_2d(pk, MLKEM_K, MLKEM_N, 0, MLKEM_Q); - mlk_polyvec_tobytes(r, pk); - memcpy(r + MLKEM_POLYVECBYTES, seed, MLKEM_SYMBYTES); + mlk_assert_bound_2d(pks->pkpv, MLKEM_K, MLKEM_N, 0, MLKEM_Q); + mlk_polyvec_tobytes(pk, pks->pkpv); + memcpy(pk + MLKEM_POLYVECBYTES, pks->seed, MLKEM_SYMBYTES); } + /************************************************* - * Name: mlk_unpack_pk + * Name: mlk_indcpa_parse_pk * * Description: De-serialize public key from a byte array; * approximate inverse of mlk_pack_pk @@ -83,11 +84,13 @@ static void mlk_pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], mlk_polyvec pk, * Implements [@FIPS203, Algorithm 14 (K-PKE.Encrypt), L2-3] * **************************************************/ -static void mlk_unpack_pk(mlk_polyvec pk, uint8_t seed[MLKEM_SYMBYTES], - const uint8_t packedpk[MLKEM_INDCPA_PUBLICKEYBYTES]) +MLK_INTERNAL_API +void mlk_indcpa_parse_pk(mlk_indcpa_public_key *pks, + const uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES]) { - mlk_polyvec_frombytes(pk, packedpk); - memcpy(seed, packedpk + MLKEM_POLYVECBYTES, MLKEM_SYMBYTES); + mlk_polyvec_frombytes(pks->pkpv, pk); + memcpy(pks->seed, pk + MLKEM_POLYVECBYTES, MLKEM_SYMBYTES); + mlk_gen_matrix(pks->at, pks->seed, 1); /* NOTE: If a modulus check was conducted on the PK, we know at this * point that the coefficients of `pk` are unsigned canonical. The @@ -96,7 +99,7 @@ static void mlk_unpack_pk(mlk_polyvec pk, uint8_t seed[MLKEM_SYMBYTES], } /************************************************* - * Name: mlk_pack_sk + * Name: mlk_indcpa_marshal_sk * * Description: Serialize the secret key * @@ -108,14 +111,16 @@ static void mlk_unpack_pk(mlk_polyvec pk, uint8_t seed[MLKEM_SYMBYTES], * Implements [@FIPS203, Algorithm 13 (K-PKE.KeyGen), L20] * **************************************************/ -static void mlk_pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES], mlk_polyvec sk) +MLK_INTERNAL_API +void mlk_indcpa_marshal_sk(uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES], + const mlk_indcpa_secret_key *sks) { - mlk_assert_bound_2d(sk, MLKEM_K, MLKEM_N, 0, MLKEM_Q); - mlk_polyvec_tobytes(r, sk); + mlk_assert_bound_2d(sks->skpv, MLKEM_K, MLKEM_N, 0, MLKEM_Q); + mlk_polyvec_tobytes(sk, sks->skpv); } /************************************************* - * Name: mlk_unpack_sk + * Name: mlk_indcpa_parse_sk * * Description: De-serialize the secret key; inverse of mlk_pack_sk * @@ -128,10 +133,11 @@ static void mlk_pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES], mlk_polyvec sk) * Implements [@FIPS203, Algorithm 15 (K-PKE.Decrypt), L5] * **************************************************/ -static void mlk_unpack_sk(mlk_polyvec sk, - const uint8_t packedsk[MLKEM_INDCPA_SECRETKEYBYTES]) +MLK_INTERNAL_API +void mlk_indcpa_parse_sk(mlk_indcpa_secret_key *sks, + const uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES]) { - mlk_polyvec_frombytes(sk, packedsk); + mlk_polyvec_frombytes(sks->skpv, sk); } /************************************************* @@ -193,6 +199,24 @@ __contract__( ensures(array_bound(data, 0, MLKEM_N, 0, MLKEM_Q))) { ((void)data); } #endif /* !MLK_USE_NATIVE_NTT_CUSTOM_ORDER */ +static void mlk_transpose_matrix(mlk_polymat a) +{ + unsigned int i, j, k; + int16_t t; + for (i = 0; i < MLKEM_K; i++) + { + for (j = i + 1; j < MLKEM_K; j++) + { + for (k = 0; k < MLKEM_N; k++) + { + t = a[i * MLKEM_K + j].coeffs[k]; + a[i * MLKEM_K + j].coeffs[k] = a[j * MLKEM_K + i].coeffs[k]; + a[j * MLKEM_K + i].coeffs[k] = t; + } + } + } +} + /* Reference: `gen_matrix()` in the reference implementation [@REF]. * - We use a special subroutine to generate 4 polynomials * at a time, to be able to leverage batched Keccak-f1600 @@ -331,15 +355,15 @@ __contract__( * - We include buffer zeroization. */ MLK_INTERNAL_API -void mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], - uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES], +void mlk_indcpa_keypair_derand(mlk_indcpa_public_key *pk, + mlk_indcpa_secret_key *sk, const uint8_t coins[MLKEM_SYMBYTES]) { MLK_ALIGN uint8_t buf[2 * MLKEM_SYMBYTES]; const uint8_t *publicseed = buf; const uint8_t *noiseseed = buf + MLKEM_SYMBYTES; - mlk_polymat a; - mlk_polyvec e, pkpv, skpv; + + mlk_polyvec e; mlk_polyvec_mulcache skpv_cache; MLK_ALIGN uint8_t coins_with_domain_separator[MLKEM_SYMBYTES + 1]; @@ -357,49 +381,48 @@ void mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], */ MLK_CT_TESTING_DECLASSIFY(publicseed, MLKEM_SYMBYTES); - mlk_gen_matrix(a, publicseed, 0 /* no transpose */); + mlk_gen_matrix(pk->at, publicseed, 0 /* no transpose */); #if MLKEM_K == 2 - mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &e[0], &e[1], noiseseed, 0, 1, - 2, 3); + mlk_poly_getnoise_eta1_4x(&sk->skpv[0], &sk->skpv[1], &e[0], &e[1], noiseseed, + 0, 1, 2, 3); #elif MLKEM_K == 3 /* * Only the first three output buffers are needed. * The laster parameter is a dummy that's overwritten later. */ - mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &skpv[2], - &pkpv[0] /* irrelevant */, noiseseed, 0, 1, 2, + mlk_poly_getnoise_eta1_4x(&sk->skpv[0], &sk->skpv[1], &sk->skpv[2], + &pk->pkpv[0] /* irrelevant */, noiseseed, 0, 1, 2, 0xFF /* irrelevant */); /* Same here */ - mlk_poly_getnoise_eta1_4x(&e[0], &e[1], &e[2], &pkpv[0] /* irrelevant */, + mlk_poly_getnoise_eta1_4x(&e[0], &e[1], &e[2], &pk->pkpv[0] /* irrelevant */, noiseseed, 3, 4, 5, 0xFF /* irrelevant */); #elif MLKEM_K == 4 - mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &skpv[2], &skpv[3], noiseseed, - 0, 1, 2, 3); + mlk_poly_getnoise_eta1_4x(&sk->skpv[0], &sk->skpv[1], &sk->skpv[2], + &sk->skpv[3], noiseseed, 0, 1, 2, 3); mlk_poly_getnoise_eta1_4x(&e[0], &e[1], &e[2], &e[3], noiseseed, 4, 5, 6, 7); #endif - mlk_polyvec_ntt(skpv); + mlk_polyvec_ntt(sk->skpv); mlk_polyvec_ntt(e); - mlk_polyvec_mulcache_compute(skpv_cache, skpv); - mlk_matvec_mul(pkpv, a, skpv, skpv_cache); - mlk_polyvec_tomont(pkpv); + mlk_polyvec_mulcache_compute(skpv_cache, sk->skpv); + mlk_matvec_mul(pk->pkpv, pk->at, sk->skpv, skpv_cache); + mlk_polyvec_tomont(pk->pkpv); + + mlk_polyvec_add(pk->pkpv, e); + mlk_polyvec_reduce(pk->pkpv); + mlk_polyvec_reduce(sk->skpv); - mlk_polyvec_add(pkpv, e); - mlk_polyvec_reduce(pkpv); - mlk_polyvec_reduce(skpv); + mlk_transpose_matrix(pk->at); + memcpy(pk->seed, publicseed, MLKEM_SYMBYTES); - mlk_pack_sk(sk, skpv); - mlk_pack_pk(pk, pkpv, publicseed); /* Specification: Partially implements * [@FIPS203, Section 3.3, Destruction of intermediate values] */ mlk_zeroize(buf, sizeof(buf)); mlk_zeroize(coins_with_domain_separator, sizeof(coins_with_domain_separator)); - mlk_zeroize(a, sizeof(a)); mlk_zeroize(&e, sizeof(e)); - mlk_zeroize(&skpv, sizeof(skpv)); mlk_zeroize(&skpv_cache, sizeof(skpv_cache)); } @@ -414,28 +437,14 @@ void mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], MLK_INTERNAL_API void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], const uint8_t m[MLKEM_INDCPA_MSGBYTES], - const uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], + const mlk_indcpa_public_key *pk, const uint8_t coins[MLKEM_SYMBYTES]) { - MLK_ALIGN uint8_t seed[MLKEM_SYMBYTES]; - mlk_polymat at; - mlk_polyvec sp, pkpv, ep, b; + mlk_polyvec sp, ep, b; mlk_poly v, k, epp; mlk_polyvec_mulcache sp_cache; - - 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. - * This is needed because in re-encryption the publicseed originated from sk - * which is marked undefined. - */ - MLK_CT_TESTING_DECLASSIFY(seed, MLKEM_SYMBYTES); - - mlk_gen_matrix(at, seed, 1 /* transpose */); - #if MLKEM_K == 2 mlk_poly_getnoise_eta1122_4x(&sp[0], &sp[1], &ep[0], &ep[1], coins, 0, 1, 2, 3); @@ -458,8 +467,8 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], 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_matvec_mul(b, pk->at, sp, sp_cache); + mlk_polyvec_basemul_acc_montgomery_cached(&v, pk->pkpv, sp, sp_cache); mlk_polyvec_invntt_tomont(b); mlk_poly_invntt_tomont(&v); @@ -475,12 +484,10 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], /* Specification: Partially implements * [@FIPS203, Section 3.3, Destruction of intermediate values] */ - mlk_zeroize(seed, sizeof(seed)); mlk_zeroize(&sp, sizeof(sp)); mlk_zeroize(&sp_cache, sizeof(sp_cache)); mlk_zeroize(&b, sizeof(b)); mlk_zeroize(&v, sizeof(v)); - mlk_zeroize(at, sizeof(at)); mlk_zeroize(&k, sizeof(k)); mlk_zeroize(&ep, sizeof(ep)); mlk_zeroize(&epp, sizeof(epp)); @@ -492,18 +499,17 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], MLK_INTERNAL_API void mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES], const uint8_t c[MLKEM_INDCPA_BYTES], - const uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES]) + const mlk_indcpa_secret_key *sk) { - mlk_polyvec b, skpv; + mlk_polyvec b; mlk_poly v, sb; mlk_polyvec_mulcache b_cache; mlk_unpack_ciphertext(b, &v, c); - mlk_unpack_sk(skpv, sk); mlk_polyvec_ntt(b); mlk_polyvec_mulcache_compute(b_cache, b); - mlk_polyvec_basemul_acc_montgomery_cached(&sb, skpv, b, b_cache); + mlk_polyvec_basemul_acc_montgomery_cached(&sb, sk->skpv, b, b_cache); mlk_poly_invntt_tomont(&sb); mlk_poly_sub(&v, &sb); @@ -513,7 +519,6 @@ void mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES], /* Specification: Partially implements * [@FIPS203, Section 3.3, Destruction of intermediate values] */ - mlk_zeroize(&skpv, sizeof(skpv)); mlk_zeroize(&b, sizeof(b)); mlk_zeroize(&b_cache, sizeof(b_cache)); mlk_zeroize(&v, sizeof(v)); @@ -522,11 +527,10 @@ void 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_transpose_matrix #undef mlk_poly_permute_bitrev_to_custom diff --git a/mlkem/indcpa.h b/mlkem/indcpa.h index 0fc285005..c1313c21c 100644 --- a/mlkem/indcpa.h +++ b/mlkem/indcpa.h @@ -20,6 +20,40 @@ #include "common.h" #include "poly_k.h" +#define mlk_indcpa_secret_key MLK_NAMESPACE_K(mlk_indcpa_secret_key) +typedef struct +{ + mlk_polyvec skpv; +} MLK_ALIGN mlk_indcpa_secret_key; + +#define mlk_indcpa_public_key MLK_NAMESPACE_K(mlk_indcpa_public_key) +typedef struct +{ + mlk_polymat at; /* transposed matrix */ + mlk_polyvec pkpv; + MLK_ALIGN uint8_t seed[MLKEM_SYMBYTES]; +} MLK_ALIGN mlk_indcpa_public_key; + +#define mlk_indcpa_marshal_pk MLK_NAMESPACE_K(indcpa_marshal_pk) +MLK_INTERNAL_API +void mlk_indcpa_marshal_pk(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], + const mlk_indcpa_public_key *pks); + +#define mlk_indcpa_parse_pk MLK_NAMESPACE_K(indcpa_parse_pk) +MLK_INTERNAL_API +void mlk_indcpa_parse_pk(mlk_indcpa_public_key *pks, + const uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES]); + +#define mlk_indcpa_marshal_sk MLK_NAMESPACE_K(indcpa_marshal_sk) +MLK_INTERNAL_API +void mlk_indcpa_marshal_sk(uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES], + const mlk_indcpa_secret_key *sks); + +#define mlk_indcpa_parse_sk MLK_NAMESPACE_K(indcpa_parse_sk) +MLK_INTERNAL_API +void mlk_indcpa_parse_sk(mlk_indcpa_secret_key *sks, + const uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES]); + #define mlk_gen_matrix MLK_NAMESPACE_K(gen_matrix) /************************************************* * Name: mlk_gen_matrix @@ -68,12 +102,12 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], - uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES], +void mlk_indcpa_keypair_derand(mlk_indcpa_public_key *pk, + mlk_indcpa_secret_key *sk, const uint8_t coins[MLKEM_SYMBYTES]) __contract__( - requires(memory_no_alias(pk, MLKEM_INDCPA_PUBLICKEYBYTES)) - requires(memory_no_alias(sk, MLKEM_INDCPA_SECRETKEYBYTES)) + requires(memory_no_alias(pk, sizeof(mlk_indcpa_public_key))) + requires(memory_no_alias(sk, sizeof(mlk_indcpa_secret_key))) requires(memory_no_alias(coins, MLKEM_SYMBYTES)) assigns(object_whole(pk)) assigns(object_whole(sk)) @@ -102,12 +136,12 @@ __contract__( MLK_INTERNAL_API void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], const uint8_t m[MLKEM_INDCPA_MSGBYTES], - const uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], + const mlk_indcpa_public_key *pk, const uint8_t coins[MLKEM_SYMBYTES]) __contract__( requires(memory_no_alias(c, MLKEM_INDCPA_BYTES)) requires(memory_no_alias(m, MLKEM_INDCPA_MSGBYTES)) - requires(memory_no_alias(pk, MLKEM_INDCPA_PUBLICKEYBYTES)) + requires(memory_no_alias(pk, sizeof(mlk_indcpa_public_key))) requires(memory_no_alias(coins, MLKEM_SYMBYTES)) assigns(object_whole(c)) ); @@ -132,11 +166,11 @@ __contract__( MLK_INTERNAL_API void mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES], const uint8_t c[MLKEM_INDCPA_BYTES], - const uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES]) + const mlk_indcpa_secret_key *sk) __contract__( requires(memory_no_alias(c, MLKEM_INDCPA_BYTES)) requires(memory_no_alias(m, MLKEM_INDCPA_MSGBYTES)) - requires(memory_no_alias(sk, MLKEM_INDCPA_SECRETKEYBYTES)) + requires(memory_no_alias(sk, sizeof(mlk_indcpa_secret_key))) assigns(object_whole(m)) ); diff --git a/mlkem/kem.c b/mlkem/kem.c index a2f6f72da..97b757ce8 100644 --- a/mlkem/kem.c +++ b/mlkem/kem.c @@ -203,6 +203,120 @@ static int mlk_check_pct(uint8_t const pk[MLKEM_INDCCA_PUBLICKEYBYTES], } #endif /* !MLK_CONFIG_KEYGEN_PCT */ + +MLK_EXTERNAL_API +void crypto_kem_marshal_pk(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES], + const mlk_public_key *pks) +{ + mlk_indcpa_marshal_pk(pk, &pks->indcpa_pk); +} + +MLK_EXTERNAL_API +int crypto_kem_parse_pk(mlk_public_key *pks, + const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]) +{ + /* Specification: Implements [@FIPS203, Section 7.2, Modulus check] */ + if (mlk_check_pk(pk)) + { + memset(pks, 0, sizeof(mlk_public_key)); + return -1; + } + mlk_indcpa_parse_pk(&pks->indcpa_pk, pk); + mlk_hash_h(pks->hpk, pk, MLKEM_INDCCA_PUBLICKEYBYTES); + return 0; +} + +MLK_EXTERNAL_API +void crypto_kem_marshal_sk(uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES], + const mlk_secret_key *sks) +{ + mlk_indcpa_marshal_sk(sk, &sks->indcpa_sk); + mlk_indcpa_marshal_pk(sk + MLKEM_INDCPA_SECRETKEYBYTES, &sks->indcpa_pk); + memcpy(sk + MLKEM_INDCPA_SECRETKEYBYTES + MLKEM_INDCPA_PUBLICKEYBYTES, + sks->hpk, MLKEM_SYMBYTES); + memcpy(sk + MLKEM_INDCPA_SECRETKEYBYTES + MLKEM_INDCPA_PUBLICKEYBYTES + + MLKEM_SYMBYTES, + sks->z, MLKEM_SYMBYTES); +} + +MLK_EXTERNAL_API +int crypto_kem_parse_sk(mlk_secret_key *sks, + const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES]) +{ + /* Specification: Implements [@FIPS203, Section 7.3, Hash check] */ + if (mlk_check_sk(sk)) + { + memset(sks, 0, sizeof(mlk_secret_key)); + return -1; + } + mlk_indcpa_parse_sk(&sks->indcpa_sk, sk); + mlk_indcpa_parse_pk(&sks->indcpa_pk, sk + MLKEM_INDCPA_SECRETKEYBYTES); + memcpy(sks->hpk, + sk + MLKEM_INDCPA_SECRETKEYBYTES + MLKEM_INDCPA_PUBLICKEYBYTES, + MLKEM_SYMBYTES); + memcpy(sks->z, + sk + MLKEM_INDCPA_SECRETKEYBYTES + MLKEM_INDCPA_PUBLICKEYBYTES + + MLKEM_SYMBYTES, + MLKEM_SYMBYTES); + return 0; +} + + +MLK_EXTERNAL_API +int crypto_kem_keypair_derand_struct(mlk_public_key *pk, mlk_secret_key *sk, + const uint8_t coins[2 * MLKEM_SYMBYTES]) +{ + MLK_ALIGN uint8_t pks[MLKEM_INDCCA_PUBLICKEYBYTES]; + + mlk_indcpa_keypair_derand(&sk->indcpa_pk, &sk->indcpa_sk, coins); + + /* pre-compute H(pk) */ + mlk_indcpa_marshal_pk(pks, &sk->indcpa_pk); + mlk_hash_h(sk->hpk, pks, MLKEM_INDCCA_PUBLICKEYBYTES); + + /* + * copy over indcpa pk and H(pk) to public key + * pk is NULL during parsing before decaps as the pk is not needed + **/ + if (pk != NULL) + { + memcpy(&pk->indcpa_pk, &sk->indcpa_pk, sizeof(mlk_indcpa_public_key)); + memcpy(pk->hpk, sk->hpk, MLKEM_SYMBYTES); + } + + /* Value z for pseudo-random output on reject */ + memcpy(sk->z, coins + MLKEM_SYMBYTES, MLKEM_SYMBYTES); + + /* Declassify public key */ + MLK_CT_TESTING_DECLASSIFY(&pk->indcpa_pk, sizeof(mlk_indcpa_public_key)); + + + /* Specification: Partially implements + * [FIPS 203, Section 3.3, Destruction of intermediate values] */ + mlk_zeroize(pks, sizeof(pks)); + return 0; +} + +MLK_EXTERNAL_API +int crypto_kem_keypair_struct(mlk_public_key *pk, mlk_secret_key *sk) +{ + int res; + MLK_ALIGN uint8_t coins[2 * MLKEM_SYMBYTES]; + + /* Acquire necessary randomness, and mark it as secret. */ + mlk_randombytes(coins, 2 * MLKEM_SYMBYTES); + MLK_CT_TESTING_SECRET(coins, sizeof(coins)); + + res = crypto_kem_keypair_derand_struct(pk, sk, coins); + + + /* Specification: Partially implements + * [FIPS 203, Section 3.3, Destruction of intermediate values] */ + mlk_zeroize(coins, sizeof(coins)); + return res; +} + + /* Reference: `crypto_kem_keypair_derand()` in the reference implementation * [@REF]. * - We optionally include PCT which is not present in @@ -212,16 +326,16 @@ int crypto_kem_keypair_derand(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES], uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES], const uint8_t coins[2 * MLKEM_SYMBYTES]) { - mlk_indcpa_keypair_derand(pk, sk, coins); - memcpy(sk + MLKEM_INDCPA_SECRETKEYBYTES, pk, MLKEM_INDCCA_PUBLICKEYBYTES); - mlk_hash_h(sk + MLKEM_INDCCA_SECRETKEYBYTES - 2 * MLKEM_SYMBYTES, pk, - MLKEM_INDCCA_PUBLICKEYBYTES); - /* Value z for pseudo-random output on reject */ - memcpy(sk + MLKEM_INDCCA_SECRETKEYBYTES - MLKEM_SYMBYTES, - coins + MLKEM_SYMBYTES, MLKEM_SYMBYTES); + int res; + mlk_public_key pks; + mlk_secret_key sks; - /* Declassify public key */ - MLK_CT_TESTING_DECLASSIFY(pk, MLKEM_INDCCA_PUBLICKEYBYTES); + + res = crypto_kem_keypair_derand_struct(&pks, &sks, coins); + + + crypto_kem_marshal_pk(pk, &pks); + crypto_kem_marshal_sk(sk, &sks); /* Pairwise Consistency Test (PCT) [@FIPS140_3_IG, p.87] */ if (mlk_check_pct(pk, sk)) @@ -229,7 +343,11 @@ int crypto_kem_keypair_derand(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES], return -1; } - return 0; + /* Specification: Partially implements + * [FIPS 203, Section 3.3, Destruction of intermediate values] */ + mlk_zeroize(&pks, sizeof(mlk_public_key)); + mlk_zeroize(&sks, sizeof(mlk_secret_key)); + return res; } /* Reference: `crypto_kem_keypair()` in the reference implementation [@REF] @@ -253,44 +371,79 @@ int crypto_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES], return res; } -/* Reference: `crypto_kem_enc_derand()` in the reference implementation [@REF] - * - We include public key check - * - We include stack buffer zeroization */ MLK_EXTERNAL_API -int crypto_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], - uint8_t ss[MLKEM_SSBYTES], - const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES], - const uint8_t coins[MLKEM_SYMBYTES]) +int crypto_kem_enc_derand_struct(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], + uint8_t ss[MLKEM_SSBYTES], + const mlk_public_key *pk, + const uint8_t coins[MLKEM_SYMBYTES]) { MLK_ALIGN uint8_t buf[2 * MLKEM_SYMBYTES]; /* Will contain key, coins */ MLK_ALIGN uint8_t kr[2 * MLKEM_SYMBYTES]; - /* Specification: Implements [@FIPS203, Section 7.2, Modulus check] */ - if (mlk_check_pk(pk)) - { - return -1; - } - memcpy(buf, coins, MLKEM_SYMBYTES); /* Multitarget countermeasure for coins + contributory KEM */ - mlk_hash_h(buf + MLKEM_SYMBYTES, pk, MLKEM_INDCCA_PUBLICKEYBYTES); + memcpy(buf + MLKEM_SYMBYTES, pk->hpk, MLKEM_SYMBYTES); mlk_hash_g(kr, buf, 2 * MLKEM_SYMBYTES); /* coins are in kr+MLKEM_SYMBYTES */ - mlk_indcpa_enc(ct, buf, pk, kr + MLKEM_SYMBYTES); + mlk_indcpa_enc(ct, buf, &pk->indcpa_pk, kr + MLKEM_SYMBYTES); memcpy(ss, kr, MLKEM_SYMBYTES); /* Specification: Partially implements - * [@FIPS203, Section 3.3, Destruction of intermediate values] */ + * [FIPS 203, Section 3.3, Destruction of intermediate values] */ mlk_zeroize(buf, sizeof(buf)); mlk_zeroize(kr, sizeof(kr)); - return 0; } +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int crypto_kem_enc_struct(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], + uint8_t ss[MLKEM_SSBYTES], const mlk_public_key *pk) +{ + int res; + MLK_ALIGN uint8_t coins[MLKEM_SYMBYTES]; + + mlk_randombytes(coins, MLKEM_SYMBYTES); + MLK_CT_TESTING_SECRET(coins, sizeof(coins)); + + res = crypto_kem_enc_derand_struct(ct, ss, pk, coins); + + /* Specification: Partially implements + * [FIPS 203, Section 3.3, Destruction of intermediate values] */ + mlk_zeroize(coins, sizeof(coins)); + return res; +} + +/* Reference: `crypto_kem_enc_derand()` in the reference implementation [@REF] + * - We include public key check + * - We include stack buffer zeroization */ +MLK_EXTERNAL_API +int crypto_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], + uint8_t ss[MLKEM_SSBYTES], + const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES], + const uint8_t coins[MLKEM_SYMBYTES]) +{ + int res; + mlk_public_key pks; + if (crypto_kem_parse_pk(&pks, pk)) + { + return -1; + } + + res = crypto_kem_enc_derand_struct(ct, ss, &pks, coins); + + /* Specification: Partially implements + * [@FIPS203, Section 3.3, Destruction of intermediate values] */ + mlk_zeroize(&pks, sizeof(mlk_public_key)); + return res; +} + + + /* Reference: `crypto_kem_enc()` in the reference implementation [@REF] * - We include stack buffer zeroization */ MLK_EXTERNAL_API @@ -312,13 +465,11 @@ int crypto_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], return res; } -/* Reference: `crypto_kem_dec()` in the reference implementation [@REF] - * - We include secret key check - * - We include stack buffer zeroization */ MLK_EXTERNAL_API -int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES], - const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], - const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES]) +MLK_MUST_CHECK_RETURN_VALUE +int crypto_kem_dec_struct(uint8_t ss[MLKEM_SSBYTES], + const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], + const mlk_secret_key *sk) { uint8_t fail; MLK_ALIGN uint8_t buf[2 * MLKEM_SYMBYTES]; @@ -326,29 +477,19 @@ int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES], MLK_ALIGN uint8_t kr[2 * MLKEM_SYMBYTES]; MLK_ALIGN uint8_t tmp[MLKEM_SYMBYTES + MLKEM_INDCCA_CIPHERTEXTBYTES]; - const uint8_t *pk = sk + MLKEM_INDCPA_SECRETKEYBYTES; - - /* Specification: Implements [@FIPS203, Section 7.3, Hash check] */ - if (mlk_check_sk(sk)) - { - return -1; - } - - mlk_indcpa_dec(buf, ct, sk); + mlk_indcpa_dec(buf, ct, &sk->indcpa_sk); /* Multitarget countermeasure for coins + contributory KEM */ - memcpy(buf + MLKEM_SYMBYTES, - sk + MLKEM_INDCCA_SECRETKEYBYTES - 2 * MLKEM_SYMBYTES, MLKEM_SYMBYTES); + memcpy(buf + MLKEM_SYMBYTES, sk->hpk, MLKEM_SYMBYTES); mlk_hash_g(kr, buf, 2 * MLKEM_SYMBYTES); /* Recompute and compare ciphertext */ /* coins are in kr+MLKEM_SYMBYTES */ - mlk_indcpa_enc(tmp, buf, pk, kr + MLKEM_SYMBYTES); + mlk_indcpa_enc(tmp, buf, &sk->indcpa_pk, kr + MLKEM_SYMBYTES); fail = mlk_ct_memcmp(ct, tmp, MLKEM_INDCCA_CIPHERTEXTBYTES); /* Compute rejection key */ - memcpy(tmp, sk + MLKEM_INDCCA_SECRETKEYBYTES - MLKEM_SYMBYTES, - MLKEM_SYMBYTES); + memcpy(tmp, sk->z, MLKEM_SYMBYTES); memcpy(tmp + MLKEM_SYMBYTES, ct, MLKEM_INDCCA_CIPHERTEXTBYTES); mlk_hash_j(ss, tmp, sizeof(tmp)); @@ -360,10 +501,49 @@ int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES], mlk_zeroize(buf, sizeof(buf)); mlk_zeroize(kr, sizeof(kr)); mlk_zeroize(tmp, sizeof(tmp)); + return 0; +} +/* Reference: `crypto_kem_dec()` in the reference implementation [@REF] + * - We include secret key check + * - We include stack buffer zeroization */ +MLK_EXTERNAL_API +int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES], + const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], + const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES]) +{ + int res; + mlk_secret_key sks; + + if (crypto_kem_parse_sk(&sks, sk)) + { + return -1; + } + + res = crypto_kem_dec_struct(ss, ct, &sks); + mlk_zeroize(&sks, sizeof(mlk_secret_key)); + return res; +} + +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int crypto_kem_sk_from_seed(mlk_secret_key *sk, + const uint8_t coins[2 * MLKEM_SYMBYTES]) +{ + return crypto_kem_keypair_derand_struct(NULL, sk, coins); +} + +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int crypto_kem_pk_from_sk(mlk_public_key *pk, const mlk_secret_key *sk) +{ + memcpy(pk->hpk, sk->hpk, MLKEM_SYMBYTES); + memcpy(&pk->indcpa_pk, &sk->indcpa_pk, sizeof(mlk_indcpa_public_key)); return 0; } + + /* 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_pk diff --git a/mlkem/kem.h b/mlkem/kem.h index 1273d1859..eed07bcda 100644 --- a/mlkem/kem.h +++ b/mlkem/kem.h @@ -18,6 +18,7 @@ #include #include "cbmc.h" #include "common.h" +#include "indcpa.h" #include "sys.h" #if defined(MLK_CHECK_APIS) @@ -50,6 +51,91 @@ #define crypto_kem_enc MLK_NAMESPACE_K(enc) #define crypto_kem_dec MLK_NAMESPACE_K(dec) +#define crypto_kem_marshal_pk MLK_NAMESPACE_K(marshal_pk) +#define crypto_kem_parse_pk MLK_NAMESPACE_K(parse_pk) +#define crypto_kem_marshal_sk MLK_NAMESPACE_K(marshal_sk) +#define crypto_kem_parse_sk MLK_NAMESPACE_K(parse_sk) +#define crypto_kem_keypair_derand_struct MLK_NAMESPACE_K(keypair_derand_struct) +#define crypto_kem_keypair_struct MLK_NAMESPACE_K(keypair_struct) +#define crypto_kem_enc_derand_struct MLK_NAMESPACE_K(enc_derand_struct) +#define crypto_kem_enc_struct MLK_NAMESPACE_K(enc_struct) +#define crypto_kem_dec_struct MLK_NAMESPACE_K(dec_struct) +#define crypto_kem_sk_from_seed MLK_NAMESPACE_K(sk_from_seed) +#define crypto_kem_pk_from_sk MLK_NAMESPACE_K(pk_from_sk) + +#define mlk_secret_key MLK_NAMESPACE_K(mlk_secret_key) +typedef struct +{ + mlk_indcpa_secret_key indcpa_sk; + mlk_indcpa_public_key indcpa_pk; + MLK_ALIGN uint8_t z[MLKEM_SYMBYTES]; + MLK_ALIGN uint8_t hpk[MLKEM_SYMBYTES]; +} MLK_ALIGN mlk_secret_key; + +#define mlk_public_key MLK_NAMESPACE_K(mlk_public_key) +typedef struct +{ + mlk_indcpa_public_key indcpa_pk; + MLK_ALIGN uint8_t hpk[MLKEM_SYMBYTES]; +} MLK_ALIGN mlk_public_key; + +MLK_EXTERNAL_API +void crypto_kem_marshal_pk(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES], + const mlk_public_key *pks); + +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int crypto_kem_parse_pk(mlk_public_key *pks, + const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]); + + +MLK_EXTERNAL_API +void crypto_kem_marshal_sk(uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES], + const mlk_secret_key *sks); + +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int crypto_kem_parse_sk(mlk_secret_key *sks, + const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES]); + + +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int crypto_kem_keypair_derand_struct(mlk_public_key *pk, mlk_secret_key *sk, + const uint8_t coins[2 * MLKEM_SYMBYTES]); + +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int crypto_kem_keypair_struct(mlk_public_key *pk, mlk_secret_key *sk); + +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int crypto_kem_enc_derand_struct(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], + uint8_t ss[MLKEM_SSBYTES], + const mlk_public_key *pk, + const uint8_t coins[MLKEM_SYMBYTES]); + +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int crypto_kem_enc_struct(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], + uint8_t ss[MLKEM_SSBYTES], const mlk_public_key *pk); + +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int crypto_kem_dec_struct(uint8_t ss[MLKEM_SSBYTES], + const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], + const mlk_secret_key *sk); + + +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int crypto_kem_sk_from_seed(mlk_secret_key *sk, + const uint8_t coins[2 * MLKEM_SYMBYTES]); + +MLK_EXTERNAL_API +MLK_MUST_CHECK_RETURN_VALUE +int crypto_kem_pk_from_sk(mlk_public_key *pk, const mlk_secret_key *sk); + /************************************************* * Name: crypto_kem_keypair_derand * diff --git a/test/test_mlkem.c b/test/test_mlkem.c index fc81076b0..dbd42b68c 100644 --- a/test/test_mlkem.c +++ b/test/test_mlkem.c @@ -6,7 +6,12 @@ #include #include #include "../mlkem/compress.h" -#include "../mlkem/mlkem_native.h" +#include "../mlkem/kem.h" + +#define CRYPTO_PUBLICKEYBYTES MLKEM_INDCCA_PUBLICKEYBYTES +#define CRYPTO_SECRETKEYBYTES MLKEM_INDCCA_SECRETKEYBYTES +#define CRYPTO_CIPHERTEXTBYTES MLKEM_INDCCA_CIPHERTEXTBYTES +#define CRYPTO_BYTES MLKEM_SYMBYTES #include "notrandombytes/notrandombytes.h" From ae1cf2f27859424469b72fbf523e301553838d0f Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Tue, 25 Feb 2025 14:46:35 +0800 Subject: [PATCH 2/7] Extended API: Adjust tests and benchmarks Signed-off-by: Matthias J. Kannwischer --- test/bench_mlkem.c | 158 +++++++++++++++++++++++++++++++++++++++++++-- test/test_mlkem.c | 60 +++++++++++++++++ 2 files changed, 214 insertions(+), 4 deletions(-) diff --git a/test/bench_mlkem.c b/test/bench_mlkem.c index da6ae98f7..9076b9d94 100644 --- a/test/bench_mlkem.c +++ b/test/bench_mlkem.c @@ -8,10 +8,15 @@ #include #include #include "../mlkem/common.h" -#include "../mlkem/mlkem_native.h" +#include "../mlkem/kem.h" #include "../mlkem/randombytes.h" #include "hal.h" +#define CRYPTO_PUBLICKEYBYTES MLKEM_INDCCA_PUBLICKEYBYTES +#define CRYPTO_SECRETKEYBYTES MLKEM_INDCCA_SECRETKEYBYTES +#define CRYPTO_CIPHERTEXTBYTES MLKEM_INDCCA_CIPHERTEXTBYTES +#define CRYPTO_BYTES MLKEM_SYMBYTES + #define NWARMUP 50 #define NITERATIONS 300 #define NTESTS 500 @@ -35,7 +40,7 @@ static int cmp_uint64_t(const void *a, const void *b) static void print_median(const char *txt, uint64_t cyc[NTESTS]) { - printf("%10s cycles = %" PRIu64 "\n", txt, cyc[NTESTS >> 1] / NITERATIONS); + printf("%14s cycles = %" PRIu64 "\n", txt, cyc[NTESTS >> 1] / NITERATIONS); } static int percentiles[] = {1, 10, 20, 30, 40, 50, 60, 70, 80, 90, 99}; @@ -43,7 +48,7 @@ static int percentiles[] = {1, 10, 20, 30, 40, 50, 60, 70, 80, 90, 99}; static void print_percentile_legend(void) { unsigned i; - printf("%21s", "percentile"); + printf("%25s", "percentile"); for (i = 0; i < sizeof(percentiles) / sizeof(percentiles[0]); i++) { printf("%7d", percentiles[i]); @@ -54,7 +59,7 @@ static void print_percentile_legend(void) static void print_percentiles(const char *txt, uint64_t cyc[NTESTS]) { unsigned i; - printf("%10s percentiles:", txt); + printf("%14s percentiles:", txt); for (i = 0; i < sizeof(percentiles) / sizeof(percentiles[0]); i++) { printf("%7" PRIu64, (cyc)[NTESTS * percentiles[i] / 100] / NITERATIONS); @@ -72,6 +77,19 @@ static int bench(void) unsigned char kg_rand[2 * CRYPTO_BYTES], enc_rand[CRYPTO_BYTES]; uint64_t cycles_kg[NTESTS], cycles_enc[NTESTS], cycles_dec[NTESTS]; + + mlk_public_key pks; + mlk_secret_key sks; + uint64_t cycles_kg_struct[NTESTS]; + uint64_t cycles_pk_marshal[NTESTS]; + uint64_t cycles_sk_marshal[NTESTS]; + + uint64_t cycles_pk_parse[NTESTS]; + uint64_t cycles_enc_struct[NTESTS]; + + uint64_t cycles_sk_parse[NTESTS]; + uint64_t cycles_dec_struct[NTESTS]; + unsigned i, j; uint64_t t0, t1; @@ -125,16 +143,140 @@ static int bench(void) CHECK(ret == 0); CHECK(memcmp(key_a, key_b, CRYPTO_BYTES) == 0); + + + /* Key-pair generation */ + for (j = 0; j < NWARMUP; j++) + { + ret |= crypto_kem_keypair_derand_struct(&pks, &sks, kg_rand); + } + + t0 = get_cyclecounter(); + for (j = 0; j < NITERATIONS; j++) + { + ret |= crypto_kem_keypair_derand_struct(&pks, &sks, kg_rand); + } + t1 = get_cyclecounter(); + cycles_kg_struct[i] = t1 - t0; + + + /* Marshal public key */ + for (j = 0; j < NWARMUP; j++) + { + crypto_kem_marshal_pk(pk, &pks); + } + + t0 = get_cyclecounter(); + for (j = 0; j < NITERATIONS; j++) + { + crypto_kem_marshal_pk(pk, &pks); + } + t1 = get_cyclecounter(); + cycles_pk_marshal[i] = t1 - t0; + + /* Marshal secret key */ + for (j = 0; j < NWARMUP; j++) + { + crypto_kem_marshal_sk(sk, &sks); + } + + t0 = get_cyclecounter(); + for (j = 0; j < NITERATIONS; j++) + { + crypto_kem_marshal_sk(sk, &sks); + } + t1 = get_cyclecounter(); + cycles_sk_marshal[i] = t1 - t0; + + + /* pk parse */ + for (j = 0; j < NWARMUP; j++) + { + ret |= crypto_kem_parse_pk(&pks, pk); + } + + t0 = get_cyclecounter(); + for (j = 0; j < NITERATIONS; j++) + { + ret |= crypto_kem_parse_pk(&pks, pk); + } + t1 = get_cyclecounter(); + cycles_pk_parse[i] = t1 - t0; + + + /* encaps */ + for (j = 0; j < NWARMUP; j++) + { + ret |= crypto_kem_enc_derand_struct(ct, key_a, &pks, enc_rand); + } + + t0 = get_cyclecounter(); + for (j = 0; j < NITERATIONS; j++) + { + ret |= crypto_kem_enc_derand_struct(ct, key_a, &pks, enc_rand); + } + t1 = get_cyclecounter(); + cycles_enc_struct[i] = t1 - t0; + + + /* sk prase */ + for (j = 0; j < NWARMUP; j++) + { + ret |= crypto_kem_parse_sk(&sks, sk); + } + + t0 = get_cyclecounter(); + for (j = 0; j < NITERATIONS; j++) + { + ret |= crypto_kem_parse_sk(&sks, sk); + } + t1 = get_cyclecounter(); + cycles_sk_parse[i] = t1 - t0; + + + /* decaps */ + for (j = 0; j < NWARMUP; j++) + { + ret |= crypto_kem_dec_struct(key_b, ct, &sks); + } + + t0 = get_cyclecounter(); + for (j = 0; j < NITERATIONS; j++) + { + ret |= crypto_kem_dec_struct(key_b, ct, &sks); + } + t1 = get_cyclecounter(); + cycles_dec_struct[i] = t1 - t0; + + CHECK(ret == 0); + CHECK(memcmp(key_a, key_b, CRYPTO_BYTES) == 0); } qsort(cycles_kg, NTESTS, sizeof(uint64_t), cmp_uint64_t); qsort(cycles_enc, NTESTS, sizeof(uint64_t), cmp_uint64_t); qsort(cycles_dec, NTESTS, sizeof(uint64_t), cmp_uint64_t); + qsort(cycles_kg_struct, NTESTS, sizeof(uint64_t), cmp_uint64_t); + qsort(cycles_pk_marshal, NTESTS, sizeof(uint64_t), cmp_uint64_t); + qsort(cycles_sk_marshal, NTESTS, sizeof(uint64_t), cmp_uint64_t); + qsort(cycles_pk_parse, NTESTS, sizeof(uint64_t), cmp_uint64_t); + qsort(cycles_enc_struct, NTESTS, sizeof(uint64_t), cmp_uint64_t); + qsort(cycles_sk_parse, NTESTS, sizeof(uint64_t), cmp_uint64_t); + qsort(cycles_dec_struct, NTESTS, sizeof(uint64_t), cmp_uint64_t); + + print_median("keypair", cycles_kg); print_median("encaps", cycles_enc); print_median("decaps", cycles_dec); + print_median("keypair_struct", cycles_kg_struct); + print_median("marshal_pk", cycles_pk_marshal); + print_median("marshal_sk", cycles_sk_marshal); + print_median("parse_pk", cycles_pk_parse); + print_median("encaps_struct", cycles_enc_struct); + print_median("parse_sk", cycles_sk_parse); + print_median("decaps_struct", cycles_dec_struct); + printf("\n"); print_percentile_legend(); @@ -143,6 +285,14 @@ static int bench(void) print_percentiles("encaps", cycles_enc); print_percentiles("decaps", cycles_dec); + print_percentiles("keypair_struct", cycles_kg_struct); + print_percentiles("marshal_pk", cycles_pk_marshal); + print_percentiles("marshal_sk", cycles_sk_marshal); + print_percentiles("parse_pk", cycles_pk_parse); + print_percentiles("encaps_struct", cycles_enc_struct); + print_percentiles("parse_sk", cycles_sk_parse); + print_percentiles("decaps_struct", cycles_dec_struct); + return 0; } diff --git a/test/test_mlkem.c b/test/test_mlkem.c index dbd42b68c..e4eda96ac 100644 --- a/test/test_mlkem.c +++ b/test/test_mlkem.c @@ -55,6 +55,64 @@ static int test_keys(void) return 0; } +static int test_keys_struct_no_marshal(void) +{ + mlk_public_key pk; + mlk_secret_key sk; + uint8_t ct[CRYPTO_CIPHERTEXTBYTES]; + uint8_t key_a[CRYPTO_BYTES]; + uint8_t key_b[CRYPTO_BYTES]; + + + /* Alice generates a public key */ + CHECK(crypto_kem_keypair_struct(&pk, &sk) == 0); + /* Bob derives a secret key and creates a response */ + CHECK(crypto_kem_enc_struct(ct, key_b, &pk) == 0); + /* Alice uses Bobs response to get her shared key */ + CHECK(crypto_kem_dec_struct(key_a, ct, &sk) == 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); + return 0; +} + +static int test_keys_struct_marshal(void) +{ + mlk_public_key pk; + mlk_secret_key sk; + uint8_t pkb[CRYPTO_PUBLICKEYBYTES]; + uint8_t skb[CRYPTO_SECRETKEYBYTES]; + uint8_t ct[CRYPTO_CIPHERTEXTBYTES]; + uint8_t key_a[CRYPTO_BYTES]; + uint8_t key_b[CRYPTO_BYTES]; + + /* Alice generates a public key */ + CHECK(crypto_kem_keypair_struct(&pk, &sk) == 0); + + crypto_kem_marshal_pk(pkb, &pk); + crypto_kem_marshal_sk(skb, &sk); + memset(&pk, 0, sizeof(mlk_public_key)); + memset(&sk, 0, sizeof(mlk_secret_key)); + + /* Bob derives a secret key and creates a response */ + CHECK(crypto_kem_parse_pk(&pk, pkb) == 0); + CHECK(crypto_kem_enc_struct(ct, key_b, &pk) == 0); + + /* Alice uses Bobs response to get her shared key */ + CHECK(crypto_kem_parse_sk(&sk, skb) == 0); + CHECK(crypto_kem_dec_struct(key_a, ct, &sk) == 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); + return 0; +} + static int test_invalid_pk(void) { uint8_t pk[CRYPTO_PUBLICKEYBYTES]; @@ -228,6 +286,8 @@ int main(void) for (i = 0; i < NTESTS; i++) { CHECK(test_keys() == 0); + CHECK(test_keys_struct_no_marshal() == 0); + CHECK(test_keys_struct_marshal() == 0); CHECK(test_invalid_pk() == 0); CHECK(test_invalid_sk_a() == 0); CHECK(test_invalid_sk_b() == 0); From f4f1b98fa36ef98267bdde6cdec9eabce688e23d Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Wed, 26 Feb 2025 11:54:05 +0800 Subject: [PATCH 3/7] Extended API: Adjust CBMC proofs Signed-off-by: Matthias J. Kannwischer --- mlkem/indcpa.c | 12 +- mlkem/indcpa.h | 56 ++++++- mlkem/kem.c | 11 +- mlkem/kem.h | 153 ++++++++++++++++-- mlkem/poly_k.h | 7 +- proofs/cbmc/crypto_kem_dec/Makefile | 2 +- proofs/cbmc/crypto_kem_dec_struct/Makefile | 54 +++++++ .../crypto_kem_dec_struct_harness.c | 12 ++ proofs/cbmc/crypto_kem_enc_derand/Makefile | 2 +- .../crypto_kem_enc_derand_struct/Makefile | 54 +++++++ .../crypto_kem_enc_derand_struct_harness.c | 12 ++ proofs/cbmc/crypto_kem_enc_struct/Makefile | 54 +++++++ .../crypto_kem_enc_struct_harness.c | 12 ++ .../cbmc/crypto_kem_keypair_derand/Makefile | 2 +- .../crypto_kem_keypair_derand_struct/Makefile | 54 +++++++ ...crypto_kem_keypair_derand_struct_harness.c | 13 ++ .../cbmc/crypto_kem_keypair_struct/Makefile | 54 +++++++ .../crypto_kem_keypair_struct_harness.c | 12 ++ proofs/cbmc/crypto_kem_marshal_pk/Makefile | 54 +++++++ .../crypto_kem_marshal_pk_harness.c | 12 ++ proofs/cbmc/crypto_kem_marshal_sk/Makefile | 54 +++++++ .../crypto_kem_marshal_sk_harness.c | 12 ++ proofs/cbmc/crypto_kem_parse_pk/Makefile | 54 +++++++ .../crypto_kem_parse_pk_harness.c | 12 ++ proofs/cbmc/crypto_kem_parse_sk/Makefile | 54 +++++++ .../crypto_kem_parse_sk_harness.c | 12 ++ proofs/cbmc/crypto_kem_pk_from_sk/Makefile | 54 +++++++ .../crypto_kem_pk_from_sk_harness.c | 12 ++ proofs/cbmc/crypto_kem_sk_from_seed/Makefile | 54 +++++++ .../crypto_kem_sk_from_seed_harness.c | 12 ++ proofs/cbmc/indcpa_dec/indcpa_dec_harness.c | 3 +- proofs/cbmc/indcpa_enc/indcpa_enc_harness.c | 5 +- proofs/cbmc/indcpa_keypair_derand/Makefile | 2 +- .../indcpa_keypair_derand_harness.c | 4 +- proofs/cbmc/indcpa_marshal_pk/Makefile | 54 +++++++ .../indcpa_marshal_pk_harness.c | 12 ++ proofs/cbmc/indcpa_marshal_sk/Makefile | 54 +++++++ .../indcpa_marshal_sk_harness.c | 12 ++ proofs/cbmc/indcpa_parse_pk/Makefile | 54 +++++++ .../indcpa_parse_pk/indcpa_parse_pk_harness.c | 12 ++ proofs/cbmc/indcpa_parse_sk/Makefile | 54 +++++++ .../indcpa_parse_sk/indcpa_parse_sk_harness.c | 12 ++ proofs/cbmc/transpose_matrix/Makefile | 54 +++++++ .../transpose_matrix_harness.c | 12 ++ scripts/tests | 5 + 45 files changed, 1286 insertions(+), 35 deletions(-) create mode 100644 proofs/cbmc/crypto_kem_dec_struct/Makefile create mode 100644 proofs/cbmc/crypto_kem_dec_struct/crypto_kem_dec_struct_harness.c create mode 100644 proofs/cbmc/crypto_kem_enc_derand_struct/Makefile create mode 100644 proofs/cbmc/crypto_kem_enc_derand_struct/crypto_kem_enc_derand_struct_harness.c create mode 100644 proofs/cbmc/crypto_kem_enc_struct/Makefile create mode 100644 proofs/cbmc/crypto_kem_enc_struct/crypto_kem_enc_struct_harness.c create mode 100644 proofs/cbmc/crypto_kem_keypair_derand_struct/Makefile create mode 100644 proofs/cbmc/crypto_kem_keypair_derand_struct/crypto_kem_keypair_derand_struct_harness.c create mode 100644 proofs/cbmc/crypto_kem_keypair_struct/Makefile create mode 100644 proofs/cbmc/crypto_kem_keypair_struct/crypto_kem_keypair_struct_harness.c create mode 100644 proofs/cbmc/crypto_kem_marshal_pk/Makefile create mode 100644 proofs/cbmc/crypto_kem_marshal_pk/crypto_kem_marshal_pk_harness.c create mode 100644 proofs/cbmc/crypto_kem_marshal_sk/Makefile create mode 100644 proofs/cbmc/crypto_kem_marshal_sk/crypto_kem_marshal_sk_harness.c create mode 100644 proofs/cbmc/crypto_kem_parse_pk/Makefile create mode 100644 proofs/cbmc/crypto_kem_parse_pk/crypto_kem_parse_pk_harness.c create mode 100644 proofs/cbmc/crypto_kem_parse_sk/Makefile create mode 100644 proofs/cbmc/crypto_kem_parse_sk/crypto_kem_parse_sk_harness.c create mode 100644 proofs/cbmc/crypto_kem_pk_from_sk/Makefile create mode 100644 proofs/cbmc/crypto_kem_pk_from_sk/crypto_kem_pk_from_sk_harness.c create mode 100644 proofs/cbmc/crypto_kem_sk_from_seed/Makefile create mode 100644 proofs/cbmc/crypto_kem_sk_from_seed/crypto_kem_sk_from_seed_harness.c create mode 100644 proofs/cbmc/indcpa_marshal_pk/Makefile create mode 100644 proofs/cbmc/indcpa_marshal_pk/indcpa_marshal_pk_harness.c create mode 100644 proofs/cbmc/indcpa_marshal_sk/Makefile create mode 100644 proofs/cbmc/indcpa_marshal_sk/indcpa_marshal_sk_harness.c create mode 100644 proofs/cbmc/indcpa_parse_pk/Makefile create mode 100644 proofs/cbmc/indcpa_parse_pk/indcpa_parse_pk_harness.c create mode 100644 proofs/cbmc/indcpa_parse_sk/Makefile create mode 100644 proofs/cbmc/indcpa_parse_sk/indcpa_parse_sk_harness.c create mode 100644 proofs/cbmc/transpose_matrix/Makefile create mode 100644 proofs/cbmc/transpose_matrix/transpose_matrix_harness.c diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c index fac97a9be..602617dd2 100644 --- a/mlkem/indcpa.c +++ b/mlkem/indcpa.c @@ -90,7 +90,7 @@ void mlk_indcpa_parse_pk(mlk_indcpa_public_key *pks, { mlk_polyvec_frombytes(pks->pkpv, pk); memcpy(pks->seed, pk + MLKEM_POLYVECBYTES, MLKEM_SYMBYTES); - mlk_gen_matrix(pks->at, pks->seed, 1); + mlk_gen_matrix(pks->at, pk + MLKEM_POLYVECBYTES, 1); /* NOTE: If a modulus check was conducted on the PK, we know at this * point that the coefficients of `pk` are unsigned canonical. The @@ -200,6 +200,14 @@ __contract__( #endif /* !MLK_USE_NATIVE_NTT_CUSTOM_ORDER */ static void mlk_transpose_matrix(mlk_polymat a) +__contract__( + requires(memory_no_alias(a, MLKEM_K*MLKEM_K*sizeof(mlk_poly))) + requires(forall(k0, 0, MLKEM_K * MLKEM_K, + array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + assigns(memory_slice(a, MLKEM_K*MLKEM_K*sizeof(mlk_poly))) + ensures(forall(k0, 0, MLKEM_K * MLKEM_K, + array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) +) { unsigned int i, j, k; int16_t t; @@ -334,7 +342,7 @@ __contract__( requires(memory_no_alias(vc, sizeof(mlk_polyvec_mulcache))) requires(forall(k0, 0, MLKEM_K * MLKEM_K, array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) - assigns(object_whole(out))) + assigns(memory_slice(out, sizeof(mlk_polyvec)))) { unsigned i; for (i = 0; i < MLKEM_K; i++) diff --git a/mlkem/indcpa.h b/mlkem/indcpa.h index c1313c21c..57c8b0484 100644 --- a/mlkem/indcpa.h +++ b/mlkem/indcpa.h @@ -37,22 +37,52 @@ typedef struct #define mlk_indcpa_marshal_pk MLK_NAMESPACE_K(indcpa_marshal_pk) MLK_INTERNAL_API void mlk_indcpa_marshal_pk(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], - const mlk_indcpa_public_key *pks); + const mlk_indcpa_public_key *pks) +__contract__( + requires(memory_no_alias(pk, MLKEM_INDCPA_PUBLICKEYBYTES)) + requires(memory_no_alias(pks, sizeof(mlk_indcpa_public_key))) + requires(forall(k0, 0, MLKEM_K, + array_bound(pks->pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + assigns(object_whole(pk)) +); #define mlk_indcpa_parse_pk MLK_NAMESPACE_K(indcpa_parse_pk) MLK_INTERNAL_API void mlk_indcpa_parse_pk(mlk_indcpa_public_key *pks, - const uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES]); + const uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES]) +__contract__( + requires(memory_no_alias(pks, sizeof(mlk_indcpa_public_key))) + requires(memory_no_alias(pk, MLKEM_INDCPA_PUBLICKEYBYTES)) + assigns(memory_slice(pks, sizeof(mlk_indcpa_public_key))) + ensures(forall(k1, 0, MLKEM_K, + array_bound(pks->pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + ensures(forall(x, 0, MLKEM_K * MLKEM_K, + array_bound(pks->at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) +); #define mlk_indcpa_marshal_sk MLK_NAMESPACE_K(indcpa_marshal_sk) MLK_INTERNAL_API void mlk_indcpa_marshal_sk(uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES], - const mlk_indcpa_secret_key *sks); + const mlk_indcpa_secret_key *sks) +__contract__( + requires(memory_no_alias(sk, MLKEM_INDCPA_SECRETKEYBYTES)) + requires(memory_no_alias(sks, sizeof(mlk_indcpa_secret_key))) + requires(forall(k0, 0, MLKEM_K, + array_bound(sks->skpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + assigns(object_whole(sk)) +); #define mlk_indcpa_parse_sk MLK_NAMESPACE_K(indcpa_parse_sk) MLK_INTERNAL_API void mlk_indcpa_parse_sk(mlk_indcpa_secret_key *sks, - const uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES]); + const uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES]) +__contract__( + requires(memory_no_alias(sks, sizeof(mlk_indcpa_secret_key))) + requires(memory_no_alias(sk, MLKEM_INDCPA_SECRETKEYBYTES)) + assigns(memory_slice(sks, sizeof(mlk_indcpa_secret_key))) + ensures(forall(k0, 0, MLKEM_K, + array_bound(sks->skpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) +); #define mlk_gen_matrix MLK_NAMESPACE_K(gen_matrix) /************************************************* @@ -79,7 +109,7 @@ __contract__( requires(memory_no_alias(a, sizeof(mlk_polymat))) requires(memory_no_alias(seed, MLKEM_SYMBYTES)) requires(transposed == 0 || transposed == 1) - assigns(object_whole(a)) + assigns(memory_slice(a, sizeof(mlk_poly) * MLKEM_K * MLKEM_K)) ensures(forall(x, 0, MLKEM_K * MLKEM_K, array_bound(a[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) ); @@ -109,8 +139,14 @@ __contract__( requires(memory_no_alias(pk, sizeof(mlk_indcpa_public_key))) requires(memory_no_alias(sk, sizeof(mlk_indcpa_secret_key))) requires(memory_no_alias(coins, MLKEM_SYMBYTES)) - assigns(object_whole(pk)) - assigns(object_whole(sk)) + assigns(memory_slice(pk, sizeof(mlk_indcpa_public_key))) + assigns(memory_slice(sk, sizeof(mlk_indcpa_secret_key))) + ensures(forall(k0, 0, MLKEM_K, + array_bound(pk->pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + ensures(forall(x, 0, MLKEM_K * MLKEM_K, + array_bound(pk->at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + ensures(forall(k1, 0, MLKEM_K, + array_bound(sk->skpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) ); #define mlk_indcpa_enc MLK_NAMESPACE_K(indcpa_enc) @@ -142,6 +178,10 @@ __contract__( requires(memory_no_alias(c, MLKEM_INDCPA_BYTES)) requires(memory_no_alias(m, MLKEM_INDCPA_MSGBYTES)) requires(memory_no_alias(pk, sizeof(mlk_indcpa_public_key))) + requires(forall(k0, 0, MLKEM_K, + array_bound(pk->pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + requires(forall(x, 0, MLKEM_K * MLKEM_K, + array_bound(pk->at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) requires(memory_no_alias(coins, MLKEM_SYMBYTES)) assigns(object_whole(c)) ); @@ -171,6 +211,8 @@ __contract__( requires(memory_no_alias(c, MLKEM_INDCPA_BYTES)) requires(memory_no_alias(m, MLKEM_INDCPA_MSGBYTES)) requires(memory_no_alias(sk, sizeof(mlk_indcpa_secret_key))) + requires(forall(k0, 0, MLKEM_K, + array_bound(sk->skpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) assigns(object_whole(m)) ); diff --git a/mlkem/kem.c b/mlkem/kem.c index 97b757ce8..36da96d95 100644 --- a/mlkem/kem.c +++ b/mlkem/kem.c @@ -290,7 +290,6 @@ int crypto_kem_keypair_derand_struct(mlk_public_key *pk, mlk_secret_key *sk, /* Declassify public key */ MLK_CT_TESTING_DECLASSIFY(&pk->indcpa_pk, sizeof(mlk_indcpa_public_key)); - /* Specification: Partially implements * [FIPS 203, Section 3.3, Destruction of intermediate values] */ mlk_zeroize(pks, sizeof(pks)); @@ -521,6 +520,8 @@ int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES], } res = crypto_kem_dec_struct(ss, ct, &sks); + /* Specification: Partially implements + * [FIPS 203, Section 3.3, Destruction of intermediate values] */ mlk_zeroize(&sks, sizeof(mlk_secret_key)); return res; } @@ -530,7 +531,13 @@ MLK_MUST_CHECK_RETURN_VALUE int crypto_kem_sk_from_seed(mlk_secret_key *sk, const uint8_t coins[2 * MLKEM_SYMBYTES]) { - return crypto_kem_keypair_derand_struct(NULL, sk, coins); + mlk_public_key pk; + int ret; + ret = crypto_kem_keypair_derand_struct(&pk, sk, coins); + /* Specification: Partially implements + * [FIPS 203, Section 3.3, Destruction of intermediate values] */ + mlk_zeroize(&pk, sizeof(mlk_public_key)); + return ret; } MLK_EXTERNAL_API diff --git a/mlkem/kem.h b/mlkem/kem.h index eed07bcda..953788a4d 100644 --- a/mlkem/kem.h +++ b/mlkem/kem.h @@ -81,60 +81,189 @@ typedef struct MLK_EXTERNAL_API void crypto_kem_marshal_pk(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES], - const mlk_public_key *pks); + const mlk_public_key *pks) +__contract__( + requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES)) + requires(memory_no_alias(pks, sizeof(mlk_public_key))) + requires(forall(k0, 0, MLKEM_K, + array_bound(pks->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + assigns(object_whole(pk)) +); MLK_EXTERNAL_API MLK_MUST_CHECK_RETURN_VALUE int crypto_kem_parse_pk(mlk_public_key *pks, - const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]); + const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]) +__contract__( + requires(memory_no_alias(pks, sizeof(mlk_public_key))) + requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES)) + assigns(object_whole(pks)) + ensures(forall(k0, 0, MLKEM_K, + array_bound(pks->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + ensures(forall(x, 0, MLKEM_K * MLKEM_K, + array_bound(pks->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) +); MLK_EXTERNAL_API void crypto_kem_marshal_sk(uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES], - const mlk_secret_key *sks); + const mlk_secret_key *sks) +__contract__( + requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES)) + requires(memory_no_alias(sks, sizeof(mlk_secret_key))) + requires(forall(k0, 0, MLKEM_K, + array_bound(sks->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + requires(forall(k1, 0, MLKEM_K, + array_bound(sks->indcpa_sk.skpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + assigns(object_whole(sk)) +); MLK_EXTERNAL_API MLK_MUST_CHECK_RETURN_VALUE int crypto_kem_parse_sk(mlk_secret_key *sks, - const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES]); + const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES]) +__contract__( + requires(memory_no_alias(sks, sizeof(mlk_secret_key))) + requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES)) + assigns(object_whole(sks)) + ensures(forall(k0, 0, MLKEM_K, + array_bound(sks->indcpa_sk.skpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + ensures(forall(k1, 0, MLKEM_K, + array_bound(sks->indcpa_pk.pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + ensures(forall(x, 0, MLKEM_K * MLKEM_K, + array_bound(sks->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) +); MLK_EXTERNAL_API MLK_MUST_CHECK_RETURN_VALUE int crypto_kem_keypair_derand_struct(mlk_public_key *pk, mlk_secret_key *sk, - const uint8_t coins[2 * MLKEM_SYMBYTES]); + const uint8_t coins[2 * MLKEM_SYMBYTES]) +__contract__( + requires(memory_no_alias(pk, sizeof(mlk_public_key))) + requires(memory_no_alias(sk, sizeof(mlk_secret_key))) + requires(memory_no_alias(coins, 2 * MLKEM_SYMBYTES)) + assigns(object_whole(pk)) + assigns(object_whole(sk)) + ensures(forall(k0, 0, MLKEM_K, + array_bound(pk->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + ensures(forall(x, 0, MLKEM_K * MLKEM_K, + array_bound(pk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + ensures(forall(k1, 0, MLKEM_K, + array_bound(sk->indcpa_pk.pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + ensures(forall(k2, 0, MLKEM_K, + array_bound(sk->indcpa_sk.skpv[k2].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + ensures(forall(y, 0, MLKEM_K * MLKEM_K, + array_bound(sk->indcpa_pk.at[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) +); MLK_EXTERNAL_API MLK_MUST_CHECK_RETURN_VALUE -int crypto_kem_keypair_struct(mlk_public_key *pk, mlk_secret_key *sk); +int crypto_kem_keypair_struct(mlk_public_key *pk, mlk_secret_key *sk) +__contract__( + requires(memory_no_alias(pk, sizeof(mlk_public_key))) + requires(memory_no_alias(sk, sizeof(mlk_secret_key))) + assigns(object_whole(pk)) + assigns(object_whole(sk)) + ensures(forall(k0, 0, MLKEM_K, + array_bound(pk->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + ensures(forall(x, 0, MLKEM_K * MLKEM_K, + array_bound(pk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + ensures(forall(k1, 0, MLKEM_K, + array_bound(sk->indcpa_pk.pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + ensures(forall(k2, 0, MLKEM_K, + array_bound(sk->indcpa_sk.skpv[k2].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + ensures(forall(y, 0, MLKEM_K * MLKEM_K, + array_bound(sk->indcpa_pk.at[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) +); + MLK_EXTERNAL_API MLK_MUST_CHECK_RETURN_VALUE int crypto_kem_enc_derand_struct(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], uint8_t ss[MLKEM_SSBYTES], const mlk_public_key *pk, - const uint8_t coins[MLKEM_SYMBYTES]); + const uint8_t coins[MLKEM_SYMBYTES]) +__contract__( + requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES)) + requires(memory_no_alias(ss, MLKEM_SSBYTES)) + requires(memory_no_alias(pk, sizeof(mlk_public_key))) + requires(memory_no_alias(coins, MLKEM_SYMBYTES)) + requires(forall(k0, 0, MLKEM_K, + array_bound(pk->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + requires(forall(x, 0, MLKEM_K * MLKEM_K, + array_bound(pk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + assigns(object_whole(ct)) + assigns(object_whole(ss)) +); MLK_EXTERNAL_API MLK_MUST_CHECK_RETURN_VALUE int crypto_kem_enc_struct(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], - uint8_t ss[MLKEM_SSBYTES], const mlk_public_key *pk); + uint8_t ss[MLKEM_SSBYTES], const mlk_public_key *pk) +__contract__( + requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES)) + requires(memory_no_alias(ss, MLKEM_SSBYTES)) + requires(memory_no_alias(pk, sizeof(mlk_public_key))) + requires(forall(k0, 0, MLKEM_K, + array_bound(pk->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + requires(forall(x, 0, MLKEM_K * MLKEM_K, + array_bound(pk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + assigns(object_whole(ct)) + assigns(object_whole(ss)) +); MLK_EXTERNAL_API MLK_MUST_CHECK_RETURN_VALUE int crypto_kem_dec_struct(uint8_t ss[MLKEM_SSBYTES], const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES], - const mlk_secret_key *sk); - + const mlk_secret_key *sk) +__contract__( + requires(memory_no_alias(ss, MLKEM_SSBYTES)) + requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES)) + requires(memory_no_alias(sk, sizeof(mlk_secret_key))) + requires(forall(k0, 0, MLKEM_K, + array_bound(sk->indcpa_sk.skpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + requires(forall(k1, 0, MLKEM_K, + array_bound(sk->indcpa_pk.pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + requires(forall(x, 0, MLKEM_K * MLKEM_K, + array_bound(sk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + assigns(object_whole(ss)) +); MLK_EXTERNAL_API MLK_MUST_CHECK_RETURN_VALUE int crypto_kem_sk_from_seed(mlk_secret_key *sk, - const uint8_t coins[2 * MLKEM_SYMBYTES]); + const uint8_t coins[2 * MLKEM_SYMBYTES]) +__contract__( + requires(memory_no_alias(sk, sizeof(mlk_secret_key))) + requires(memory_no_alias(coins, 2 * MLKEM_SYMBYTES)) + assigns(object_whole(sk)) + assigns(object_whole(coins)) + ensures(forall(k0, 0, MLKEM_K, + array_bound(sk->indcpa_sk.skpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + ensures(forall(k1, 0, MLKEM_K, + array_bound(sk->indcpa_pk.pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + ensures(forall(x, 0, MLKEM_K * MLKEM_K, + array_bound(sk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) +); MLK_EXTERNAL_API MLK_MUST_CHECK_RETURN_VALUE -int crypto_kem_pk_from_sk(mlk_public_key *pk, const mlk_secret_key *sk); +int crypto_kem_pk_from_sk(mlk_public_key *pk, const mlk_secret_key *sk) +__contract__( + requires(memory_no_alias(pk, sizeof(mlk_public_key))) + requires(memory_no_alias(sk, sizeof(mlk_secret_key))) + requires(forall(k1, 0, MLKEM_K, + array_bound(sk->indcpa_pk.pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + requires(forall(x, 0, MLKEM_K * MLKEM_K, + array_bound(sk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + assigns(object_whole(pk)) + ensures(forall(k0, 0, MLKEM_K, + array_bound(pk->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + ensures(forall(y, 0, MLKEM_K * MLKEM_K, + array_bound(pk->indcpa_pk.at[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) +); /************************************************* * Name: crypto_kem_keypair_derand diff --git a/mlkem/poly_k.h b/mlkem/poly_k.h index 3130ae352..fea387e16 100644 --- a/mlkem/poly_k.h +++ b/mlkem/poly_k.h @@ -318,7 +318,7 @@ __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) requires(forall(j, 0, MLKEM_K, array_abs_bound(r[j].coeffs, 0, MLKEM_N, MLKEM_Q))) - assigns(object_whole(r)) + assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(j, 0, MLKEM_K, array_abs_bound(r[j].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) ); @@ -456,7 +456,7 @@ MLK_INTERNAL_API void mlk_polyvec_reduce(mlk_polyvec r) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) - assigns(object_whole(r)) + assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(k0, 0, MLKEM_K, array_bound(r[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) ); @@ -495,7 +495,7 @@ __contract__( requires(forall(j1, 0, MLKEM_K, forall(k1, 0, MLKEM_N, (int32_t)r[j1].coeffs[k1] + b[j1].coeffs[k1] >= INT16_MIN))) - assigns(object_whole(r)) + assigns(memory_slice(r, sizeof(mlk_polyvec))) ); #define mlk_polyvec_tomont MLK_NAMESPACE_K(polyvec_tomont) @@ -518,7 +518,6 @@ void mlk_polyvec_tomont(mlk_polyvec r) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) assigns(memory_slice(r, sizeof(mlk_polyvec))) - assigns(object_whole(r)) ensures(forall(j, 0, MLKEM_K, array_abs_bound(r[j].coeffs, 0, MLKEM_N, MLKEM_Q))) ); diff --git a/proofs/cbmc/crypto_kem_dec/Makefile b/proofs/cbmc/crypto_kem_dec/Makefile index 77ab140d1..2068d8f22 100644 --- a/proofs/cbmc/crypto_kem_dec/Makefile +++ b/proofs/cbmc/crypto_kem_dec/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c CHECK_FUNCTION_CONTRACTS=mlk_dec -USE_FUNCTION_CONTRACTS=mlk_sha3_512 mlk_sha3_256 mlk_indcpa_enc mlk_indcpa_dec mlk_shake256 mlk_ct_memcmp mlk_ct_cmov_zero memcmp mlk_zeroize +USE_FUNCTION_CONTRACTS=mlk_parse_sk mlk_dec_struct mlk_zeroize APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/crypto_kem_dec_struct/Makefile b/proofs/cbmc/crypto_kem_dec_struct/Makefile new file mode 100644 index 000000000..815cd7c6c --- /dev/null +++ b/proofs/cbmc/crypto_kem_dec_struct/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = crypto_kem_dec_struct_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 = crypto_kem_dec_struct + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_dec_struct +USE_FUNCTION_CONTRACTS=mlk_sha3_512 mlk_sha3_256 mlk_indcpa_enc mlk_indcpa_dec mlk_shake256 mlk_ct_memcmp mlk_ct_cmov_zero memcmp 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_dec_struct + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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. Hdece, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/crypto_kem_dec_struct/crypto_kem_dec_struct_harness.c b/proofs/cbmc/crypto_kem_dec_struct/crypto_kem_dec_struct_harness.c new file mode 100644 index 000000000..971121f67 --- /dev/null +++ b/proofs/cbmc/crypto_kem_dec_struct/crypto_kem_dec_struct_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint8_t *a, *b; + mlk_secret_key *sk; + crypto_kem_dec_struct(a, b, sk); +} diff --git a/proofs/cbmc/crypto_kem_enc_derand/Makefile b/proofs/cbmc/crypto_kem_enc_derand/Makefile index 5a760f73d..082b1767b 100644 --- a/proofs/cbmc/crypto_kem_enc_derand/Makefile +++ b/proofs/cbmc/crypto_kem_enc_derand/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c CHECK_FUNCTION_CONTRACTS=mlk_enc_derand -USE_FUNCTION_CONTRACTS=mlk_sha3_256 mlk_sha3_512 mlk_indcpa_enc mlk_polyvec_frombytes mlk_polyvec_reduce mlk_polyvec_tobytes memcmp mlk_zeroize +USE_FUNCTION_CONTRACTS=mlk_parse_pk mlk_enc_derand_struct mlk_zeroize APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/crypto_kem_enc_derand_struct/Makefile b/proofs/cbmc/crypto_kem_enc_derand_struct/Makefile new file mode 100644 index 000000000..466d9b787 --- /dev/null +++ b/proofs/cbmc/crypto_kem_enc_derand_struct/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = crypto_kem_enc_derand_struct_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 = crypto_kem_enc_derand_struct + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_enc_derand_struct +USE_FUNCTION_CONTRACTS=mlk_indcpa_enc mlk_sha3_512 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_struct + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/crypto_kem_enc_derand_struct/crypto_kem_enc_derand_struct_harness.c b/proofs/cbmc/crypto_kem_enc_derand_struct/crypto_kem_enc_derand_struct_harness.c new file mode 100644 index 000000000..706098527 --- /dev/null +++ b/proofs/cbmc/crypto_kem_enc_derand_struct/crypto_kem_enc_derand_struct_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint8_t *a, *b, *c; + mlk_public_key *pk; + crypto_kem_enc_derand_struct(a, b, pk, c); +} diff --git a/proofs/cbmc/crypto_kem_enc_struct/Makefile b/proofs/cbmc/crypto_kem_enc_struct/Makefile new file mode 100644 index 000000000..aa36a1caa --- /dev/null +++ b/proofs/cbmc/crypto_kem_enc_struct/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = crypto_kem_enc_struct_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 = crypto_kem_enc_struct + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_enc_struct +USE_FUNCTION_CONTRACTS=mlk_enc_derand_struct randombytes 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_struct + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/crypto_kem_enc_struct/crypto_kem_enc_struct_harness.c b/proofs/cbmc/crypto_kem_enc_struct/crypto_kem_enc_struct_harness.c new file mode 100644 index 000000000..5df6691d2 --- /dev/null +++ b/proofs/cbmc/crypto_kem_enc_struct/crypto_kem_enc_struct_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint8_t *a, *b; + mlk_public_key *pk; + crypto_kem_enc_struct(a, b, pk); +} diff --git a/proofs/cbmc/crypto_kem_keypair_derand/Makefile b/proofs/cbmc/crypto_kem_keypair_derand/Makefile index 79be52da7..3f68e547a 100644 --- a/proofs/cbmc/crypto_kem_keypair_derand/Makefile +++ b/proofs/cbmc/crypto_kem_keypair_derand/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c CHECK_FUNCTION_CONTRACTS=mlk_keypair_derand -USE_FUNCTION_CONTRACTS=mlk_sha3_256 mlk_indcpa_keypair_derand mlk_check_pct +USE_FUNCTION_CONTRACTS=mlk_keypair_derand_struct mlk_marshal_pk mlk_marshal_sk mlk_check_pct mlk_zeroize APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/crypto_kem_keypair_derand_struct/Makefile b/proofs/cbmc/crypto_kem_keypair_derand_struct/Makefile new file mode 100644 index 000000000..3a4ff8ed9 --- /dev/null +++ b/proofs/cbmc/crypto_kem_keypair_derand_struct/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = crypto_kem_keypair_derand_struct_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 = crypto_kem_keypair_derand_struct + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_keypair_derand_struct +USE_FUNCTION_CONTRACTS=mlk_indcpa_keypair_derand mlk_indcpa_marshal_pk mlk_sha3_256 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_keypair_derand_struct + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/crypto_kem_keypair_derand_struct/crypto_kem_keypair_derand_struct_harness.c b/proofs/cbmc/crypto_kem_keypair_derand_struct/crypto_kem_keypair_derand_struct_harness.c new file mode 100644 index 000000000..037c8def1 --- /dev/null +++ b/proofs/cbmc/crypto_kem_keypair_derand_struct/crypto_kem_keypair_derand_struct_harness.c @@ -0,0 +1,13 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint8_t *a; + mlk_secret_key *sk; + mlk_public_key *pk; + crypto_kem_keypair_derand_struct(pk, sk, a); +} diff --git a/proofs/cbmc/crypto_kem_keypair_struct/Makefile b/proofs/cbmc/crypto_kem_keypair_struct/Makefile new file mode 100644 index 000000000..f791000cb --- /dev/null +++ b/proofs/cbmc/crypto_kem_keypair_struct/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = crypto_kem_keypair_struct_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 = crypto_kem_keypair_struct + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_keypair_struct +USE_FUNCTION_CONTRACTS=randombytes mlk_keypair_derand_struct 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_keypair_struct + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/crypto_kem_keypair_struct/crypto_kem_keypair_struct_harness.c b/proofs/cbmc/crypto_kem_keypair_struct/crypto_kem_keypair_struct_harness.c new file mode 100644 index 000000000..316e3da52 --- /dev/null +++ b/proofs/cbmc/crypto_kem_keypair_struct/crypto_kem_keypair_struct_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + mlk_public_key *a; + mlk_secret_key *b; + crypto_kem_keypair_struct(a, b); +} diff --git a/proofs/cbmc/crypto_kem_marshal_pk/Makefile b/proofs/cbmc/crypto_kem_marshal_pk/Makefile new file mode 100644 index 000000000..0e174eede --- /dev/null +++ b/proofs/cbmc/crypto_kem_marshal_pk/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = crypto_kem_marshal_pk_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 = crypto_kem_marshal_pk + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_marshal_pk +USE_FUNCTION_CONTRACTS=mlk_indcpa_marshal_pk +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_marshal_pk + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/crypto_kem_marshal_pk/crypto_kem_marshal_pk_harness.c b/proofs/cbmc/crypto_kem_marshal_pk/crypto_kem_marshal_pk_harness.c new file mode 100644 index 000000000..654733a0f --- /dev/null +++ b/proofs/cbmc/crypto_kem_marshal_pk/crypto_kem_marshal_pk_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint8_t *pk; + mlk_public_key *pks; + crypto_kem_marshal_pk(pk, pks); +} diff --git a/proofs/cbmc/crypto_kem_marshal_sk/Makefile b/proofs/cbmc/crypto_kem_marshal_sk/Makefile new file mode 100644 index 000000000..0a45d6230 --- /dev/null +++ b/proofs/cbmc/crypto_kem_marshal_sk/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = crypto_kem_marshal_sk_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 = crypto_kem_marshal_sk + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_marshal_sk +USE_FUNCTION_CONTRACTS=mlk_indcpa_marshal_sk mlk_indcpa_marshal_pk +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_marshal_sk + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/crypto_kem_marshal_sk/crypto_kem_marshal_sk_harness.c b/proofs/cbmc/crypto_kem_marshal_sk/crypto_kem_marshal_sk_harness.c new file mode 100644 index 000000000..0bf5b0f8c --- /dev/null +++ b/proofs/cbmc/crypto_kem_marshal_sk/crypto_kem_marshal_sk_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint8_t *sk; + mlk_secret_key *sks; + crypto_kem_marshal_sk(sk, sks); +} diff --git a/proofs/cbmc/crypto_kem_parse_pk/Makefile b/proofs/cbmc/crypto_kem_parse_pk/Makefile new file mode 100644 index 000000000..0db17571e --- /dev/null +++ b/proofs/cbmc/crypto_kem_parse_pk/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = crypto_kem_parse_pk_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 = crypto_kem_parse_pk + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_parse_pk +USE_FUNCTION_CONTRACTS=mlk_indcpa_parse_pk mlk_sha3_256 mlk_polyvec_frombytes mlk_polyvec_reduce mlk_polyvec_tobytes +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_parse_pk + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/crypto_kem_parse_pk/crypto_kem_parse_pk_harness.c b/proofs/cbmc/crypto_kem_parse_pk/crypto_kem_parse_pk_harness.c new file mode 100644 index 000000000..61afe9d5e --- /dev/null +++ b/proofs/cbmc/crypto_kem_parse_pk/crypto_kem_parse_pk_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint8_t *pk; + mlk_public_key *pks; + crypto_kem_parse_pk(pks, pk); +} diff --git a/proofs/cbmc/crypto_kem_parse_sk/Makefile b/proofs/cbmc/crypto_kem_parse_sk/Makefile new file mode 100644 index 000000000..b796d5dd0 --- /dev/null +++ b/proofs/cbmc/crypto_kem_parse_sk/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = crypto_kem_parse_sk_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 = crypto_kem_parse_sk + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_parse_sk +USE_FUNCTION_CONTRACTS=mlk_indcpa_parse_sk mlk_indcpa_parse_pk mlk_sha3_256 memcmp +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_parse_sk + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/crypto_kem_parse_sk/crypto_kem_parse_sk_harness.c b/proofs/cbmc/crypto_kem_parse_sk/crypto_kem_parse_sk_harness.c new file mode 100644 index 000000000..4bba29656 --- /dev/null +++ b/proofs/cbmc/crypto_kem_parse_sk/crypto_kem_parse_sk_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint8_t *sk; + mlk_secret_key *sks; + crypto_kem_parse_sk(sks, sk); +} diff --git a/proofs/cbmc/crypto_kem_pk_from_sk/Makefile b/proofs/cbmc/crypto_kem_pk_from_sk/Makefile new file mode 100644 index 000000000..db932b6f5 --- /dev/null +++ b/proofs/cbmc/crypto_kem_pk_from_sk/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = crypto_kem_pk_from_sk_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 = crypto_kem_pk_from_sk + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_pk_from_sk +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_pk_from_sk + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/crypto_kem_pk_from_sk/crypto_kem_pk_from_sk_harness.c b/proofs/cbmc/crypto_kem_pk_from_sk/crypto_kem_pk_from_sk_harness.c new file mode 100644 index 000000000..ddc66b7b8 --- /dev/null +++ b/proofs/cbmc/crypto_kem_pk_from_sk/crypto_kem_pk_from_sk_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + mlk_secret_key *sk; + mlk_public_key *pk; + mlk_pk_from_sk(pk, sk); +} diff --git a/proofs/cbmc/crypto_kem_sk_from_seed/Makefile b/proofs/cbmc/crypto_kem_sk_from_seed/Makefile new file mode 100644 index 000000000..20b6c4f5a --- /dev/null +++ b/proofs/cbmc/crypto_kem_sk_from_seed/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = crypto_kem_sk_from_seed_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 = crypto_kem_sk_from_seed + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c + +CHECK_FUNCTION_CONTRACTS=mlk_sk_from_seed +USE_FUNCTION_CONTRACTS=mlk_keypair_derand_struct 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_sk_from_seed + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/crypto_kem_sk_from_seed/crypto_kem_sk_from_seed_harness.c b/proofs/cbmc/crypto_kem_sk_from_seed/crypto_kem_sk_from_seed_harness.c new file mode 100644 index 000000000..a22ec5f32 --- /dev/null +++ b/proofs/cbmc/crypto_kem_sk_from_seed/crypto_kem_sk_from_seed_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + mlk_secret_key *sk; + uint8_t *seed; + mlk_sk_from_seed(sk, seed); +} diff --git a/proofs/cbmc/indcpa_dec/indcpa_dec_harness.c b/proofs/cbmc/indcpa_dec/indcpa_dec_harness.c index 779e6a9fb..a91bb1f8d 100644 --- a/proofs/cbmc/indcpa_dec/indcpa_dec_harness.c +++ b/proofs/cbmc/indcpa_dec/indcpa_dec_harness.c @@ -7,6 +7,7 @@ void harness(void) { - uint8_t *m, *c, *sk; + uint8_t *m, *c; + mlk_indcpa_secret_key *sk; mlk_indcpa_dec(m, c, sk); } diff --git a/proofs/cbmc/indcpa_enc/indcpa_enc_harness.c b/proofs/cbmc/indcpa_enc/indcpa_enc_harness.c index 16fdbd080..f6fdceabc 100644 --- a/proofs/cbmc/indcpa_enc/indcpa_enc_harness.c +++ b/proofs/cbmc/indcpa_enc/indcpa_enc_harness.c @@ -7,6 +7,7 @@ void harness(void) { - uint8_t *a, *b, *c, *d; - mlk_indcpa_enc(a, b, c, d); + uint8_t *a, *b, *d; + mlk_indcpa_public_key *pk; + mlk_indcpa_enc(a, b, pk, d); } diff --git a/proofs/cbmc/indcpa_keypair_derand/Makefile b/proofs/cbmc/indcpa_keypair_derand/Makefile index 15c319a51..d7b2f8ad1 100644 --- a/proofs/cbmc/indcpa_keypair_derand/Makefile +++ b/proofs/cbmc/indcpa_keypair_derand/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c CHECK_FUNCTION_CONTRACTS=mlk_indcpa_keypair_derand -USE_FUNCTION_CONTRACTS=mlk_zeroize mlk_sha3_512 mlk_gen_matrix mlk_poly_getnoise_eta1_4x mlk_polyvec_ntt mlk_polyvec_mulcache_compute mlk_matvec_mul mlk_polyvec_tomont mlk_polyvec_add mlk_polyvec_reduce mlk_polyvec_tobytes +USE_FUNCTION_CONTRACTS=mlk_zeroize mlk_sha3_512 mlk_gen_matrix mlk_poly_getnoise_eta1_4x mlk_polyvec_ntt mlk_polyvec_mulcache_compute mlk_matvec_mul mlk_polyvec_tomont mlk_polyvec_add mlk_polyvec_reduce mlk_polyvec_tobytes mlk_transpose_matrix APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/indcpa_keypair_derand/indcpa_keypair_derand_harness.c b/proofs/cbmc/indcpa_keypair_derand/indcpa_keypair_derand_harness.c index 60aa0ea95..e1b0b171b 100644 --- a/proofs/cbmc/indcpa_keypair_derand/indcpa_keypair_derand_harness.c +++ b/proofs/cbmc/indcpa_keypair_derand/indcpa_keypair_derand_harness.c @@ -6,6 +6,8 @@ void harness(void) { - uint8_t *a, *b, *c; + uint8_t *c; + mlk_indcpa_public_key *a; + mlk_indcpa_secret_key *b; mlk_indcpa_keypair_derand(a, b, c); } diff --git a/proofs/cbmc/indcpa_marshal_pk/Makefile b/proofs/cbmc/indcpa_marshal_pk/Makefile new file mode 100644 index 000000000..fc81ed9f1 --- /dev/null +++ b/proofs/cbmc/indcpa_marshal_pk/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = indcpa_marshal_pk_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 = indcpa_marshal_pk + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c + +CHECK_FUNCTION_CONTRACTS=mlk_indcpa_marshal_pk +USE_FUNCTION_CONTRACTS=mlk_polyvec_tobytes +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 = indcpa_marshal_pk + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/indcpa_marshal_pk/indcpa_marshal_pk_harness.c b/proofs/cbmc/indcpa_marshal_pk/indcpa_marshal_pk_harness.c new file mode 100644 index 000000000..a29df28fc --- /dev/null +++ b/proofs/cbmc/indcpa_marshal_pk/indcpa_marshal_pk_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint8_t *pk; + mlk_indcpa_public_key *pks; + mlk_indcpa_marshal_pk(pk, pks); +} diff --git a/proofs/cbmc/indcpa_marshal_sk/Makefile b/proofs/cbmc/indcpa_marshal_sk/Makefile new file mode 100644 index 000000000..0692fabf7 --- /dev/null +++ b/proofs/cbmc/indcpa_marshal_sk/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = indcpa_marshal_sk_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 = indcpa_marshal_sk + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c + +CHECK_FUNCTION_CONTRACTS=mlk_indcpa_marshal_sk +USE_FUNCTION_CONTRACTS=mlk_polyvec_tobytes +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 = indcpa_marshal_sk + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/indcpa_marshal_sk/indcpa_marshal_sk_harness.c b/proofs/cbmc/indcpa_marshal_sk/indcpa_marshal_sk_harness.c new file mode 100644 index 000000000..f7e9acd5f --- /dev/null +++ b/proofs/cbmc/indcpa_marshal_sk/indcpa_marshal_sk_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint8_t *sk; + mlk_indcpa_secret_key *sks; + mlk_indcpa_marshal_sk(sk, sks); +} diff --git a/proofs/cbmc/indcpa_parse_pk/Makefile b/proofs/cbmc/indcpa_parse_pk/Makefile new file mode 100644 index 000000000..d6c44a98a --- /dev/null +++ b/proofs/cbmc/indcpa_parse_pk/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = indcpa_parse_pk_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 = indcpa_parse_pk + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c + +CHECK_FUNCTION_CONTRACTS=mlk_indcpa_parse_pk +USE_FUNCTION_CONTRACTS=mlk_polyvec_frombytes mlk_gen_matrix +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 = indcpa_parse_pk + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/indcpa_parse_pk/indcpa_parse_pk_harness.c b/proofs/cbmc/indcpa_parse_pk/indcpa_parse_pk_harness.c new file mode 100644 index 000000000..3512c0e12 --- /dev/null +++ b/proofs/cbmc/indcpa_parse_pk/indcpa_parse_pk_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint8_t *pk; + mlk_indcpa_public_key *pks; + mlk_indcpa_parse_pk(pks, pk); +} diff --git a/proofs/cbmc/indcpa_parse_sk/Makefile b/proofs/cbmc/indcpa_parse_sk/Makefile new file mode 100644 index 000000000..c5ec7bb02 --- /dev/null +++ b/proofs/cbmc/indcpa_parse_sk/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = indcpa_parse_sk_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 = indcpa_parse_sk + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c + +CHECK_FUNCTION_CONTRACTS=mlk_indcpa_parse_sk +USE_FUNCTION_CONTRACTS=mlk_polyvec_frombytes +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 = indcpa_parse_sk + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/indcpa_parse_sk/indcpa_parse_sk_harness.c b/proofs/cbmc/indcpa_parse_sk/indcpa_parse_sk_harness.c new file mode 100644 index 000000000..1a0e75a98 --- /dev/null +++ b/proofs/cbmc/indcpa_parse_sk/indcpa_parse_sk_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint8_t *sk; + mlk_indcpa_secret_key *sks; + mlk_indcpa_parse_sk(sks, sk); +} diff --git a/proofs/cbmc/transpose_matrix/Makefile b/proofs/cbmc/transpose_matrix/Makefile new file mode 100644 index 000000000..5a2385743 --- /dev/null +++ b/proofs/cbmc/transpose_matrix/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = transpose_matrix_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 = transpose_matrix + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET +=mlk_transpose_matrix.1:4 mlk_transpose_matrix.2:4 mlk_transpose_matrix.0:256 + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c + +CHECK_FUNCTION_CONTRACTS=mlk_transpose_matrix +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=--bitwuzla + +FUNCTION_NAME = mlk_transpose_matrix + +# 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/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/transpose_matrix/transpose_matrix_harness.c b/proofs/cbmc/transpose_matrix/transpose_matrix_harness.c new file mode 100644 index 000000000..3b0de847d --- /dev/null +++ b/proofs/cbmc/transpose_matrix/transpose_matrix_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void mlk_transpose_matrix(mlk_polymat a); +void harness(void) +{ + mlk_polymat a; + mlk_transpose_matrix(a); +} diff --git a/scripts/tests b/scripts/tests index 48e0e491c..fb19c4b2b 100755 --- a/scripts/tests +++ b/scripts/tests @@ -761,6 +761,11 @@ class Tests: if p.stderr is not None: log.error(p.stderr.decode()) self.fail(f"CBMC proof for {func}") + if self.args.fail_upon_error: + log.error( + "Aborting proofs, as requested by -f/--fail-upon-error" + ) + exit(1) else: log.info(f" SUCCESS (after {dur}s)") From 7875c832cac79a3c736a7d65d8ccaec86297ec49 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Fri, 2 May 2025 15:18:58 +0800 Subject: [PATCH 4/7] test: use larger cbmc runners Signed-off-by: Matthias J. Kannwischer --- .github/workflows/cbmc.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml index e415c4bbf..6c5b46a91 100644 --- a/.github/workflows/cbmc.yml +++ b/.github/workflows/cbmc.yml @@ -17,7 +17,7 @@ jobs: uses: ./.github/workflows/ci_ec2_reusable.yml with: name: CBMC (MLKEM-512) - ec2_instance_type: c7g.4xlarge + ec2_instance_type: c7g.8xlarge ec2_ami: ubuntu-latest (custom AMI) ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g compile_mode: native @@ -40,7 +40,7 @@ jobs: uses: ./.github/workflows/ci_ec2_reusable.yml with: name: CBMC (MLKEM-768) - ec2_instance_type: c7g.4xlarge + ec2_instance_type: c7g.8xlarge ec2_ami: ubuntu-latest (custom AMI) ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g compile_mode: native @@ -63,7 +63,7 @@ jobs: uses: ./.github/workflows/ci_ec2_reusable.yml with: name: CBMC (MLKEM-1024) - ec2_instance_type: c7g.4xlarge + ec2_instance_type: c7g.8xlarge ec2_ami: ubuntu-latest (custom AMI) ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g compile_mode: native From b9e82efde5bb0e43861c7aa85af0609ce44dcbd8 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 5 May 2025 06:37:35 +0100 Subject: [PATCH 5/7] [TEST] Add marshalled PK to structured PK, defer transpose - Add marshalled pkpv to structured PK presentation, avoiding double-marshalling. - Transpose lazily -- avoids transposition in common keypair -> marshal pk -> parse pk -> enc flow Signed-off-by: Hanno Becker --- mlkem/indcpa.c | 40 +++++++++++++++++++--------------------- mlkem/indcpa.h | 2 ++ 2 files changed, 21 insertions(+), 21 deletions(-) diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c index 602617dd2..ea88a4f3e 100644 --- a/mlkem/indcpa.c +++ b/mlkem/indcpa.c @@ -63,7 +63,7 @@ void mlk_indcpa_marshal_pk(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], const mlk_indcpa_public_key *pks) { mlk_assert_bound_2d(pks->pkpv, MLKEM_K, MLKEM_N, 0, MLKEM_Q); - mlk_polyvec_tobytes(pk, pks->pkpv); + memcpy(pk, pks->pkpv_compressed, MLKEM_POLYVECBYTES); memcpy(pk + MLKEM_POLYVECBYTES, pks->seed, MLKEM_SYMBYTES); } @@ -89,8 +89,10 @@ void mlk_indcpa_parse_pk(mlk_indcpa_public_key *pks, const uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES]) { mlk_polyvec_frombytes(pks->pkpv, pk); + memcpy(pks->pkpv_compressed, pk, MLKEM_POLYVECBYTES); memcpy(pks->seed, pk + MLKEM_POLYVECBYTES, MLKEM_SYMBYTES); mlk_gen_matrix(pks->at, pk + MLKEM_POLYVECBYTES, 1); + pks->transposed = 1; /* NOTE: If a modulus check was conducted on the PK, we know at this * point that the coefficients of `pk` are unsigned canonical. The @@ -199,28 +201,14 @@ __contract__( ensures(array_bound(data, 0, MLKEM_N, 0, MLKEM_Q))) { ((void)data); } #endif /* !MLK_USE_NATIVE_NTT_CUSTOM_ORDER */ -static void mlk_transpose_matrix(mlk_polymat a) -__contract__( - requires(memory_no_alias(a, MLKEM_K*MLKEM_K*sizeof(mlk_poly))) - requires(forall(k0, 0, MLKEM_K * MLKEM_K, - array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) - assigns(memory_slice(a, MLKEM_K*MLKEM_K*sizeof(mlk_poly))) - ensures(forall(k0, 0, MLKEM_K * MLKEM_K, - array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) -) +static void mlk_transpose_matrix(mlk_polymat out, const mlk_polymat in) { - unsigned int i, j, k; - int16_t t; + unsigned int i, j; for (i = 0; i < MLKEM_K; i++) { - for (j = i + 1; j < MLKEM_K; j++) + for (j = 0; j < MLKEM_K; j++) { - for (k = 0; k < MLKEM_N; k++) - { - t = a[i * MLKEM_K + j].coeffs[k]; - a[i * MLKEM_K + j].coeffs[k] = a[j * MLKEM_K + i].coeffs[k]; - a[j * MLKEM_K + i].coeffs[k] = t; - } + memcpy(&out[i * MLKEM_K + j], &in[j * MLKEM_K + i], sizeof(mlk_poly)); } } } @@ -422,8 +410,10 @@ void mlk_indcpa_keypair_derand(mlk_indcpa_public_key *pk, mlk_polyvec_reduce(pk->pkpv); mlk_polyvec_reduce(sk->skpv); - mlk_transpose_matrix(pk->at); + pk->transposed = 0; + memcpy(pk->seed, publicseed, MLKEM_SYMBYTES); + mlk_polyvec_tobytes(pk->pkpv_compressed, pk->pkpv); /* Specification: Partially implements @@ -451,8 +441,16 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], mlk_polyvec sp, ep, b; mlk_poly v, k, epp; mlk_polyvec_mulcache sp_cache; + mlk_polymat at; + mlk_poly_frommsg(&k, m); + if (pk->transposed == 0) { + mlk_transpose_matrix(at, pk->at); + } else { + memcpy(at, pk->at, sizeof(mlk_polymat)); + } + #if MLKEM_K == 2 mlk_poly_getnoise_eta1122_4x(&sp[0], &sp[1], &ep[0], &ep[1], coins, 0, 1, 2, 3); @@ -475,7 +473,7 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], mlk_polyvec_ntt(sp); mlk_polyvec_mulcache_compute(sp_cache, sp); - mlk_matvec_mul(b, pk->at, sp, sp_cache); + mlk_matvec_mul(b, at, sp, sp_cache); mlk_polyvec_basemul_acc_montgomery_cached(&v, pk->pkpv, sp, sp_cache); mlk_polyvec_invntt_tomont(b); diff --git a/mlkem/indcpa.h b/mlkem/indcpa.h index 57c8b0484..02b991b63 100644 --- a/mlkem/indcpa.h +++ b/mlkem/indcpa.h @@ -31,7 +31,9 @@ typedef struct { mlk_polymat at; /* transposed matrix */ mlk_polyvec pkpv; + MLK_ALIGN uint8_t pkpv_compressed[MLKEM_POLYVECBYTES]; MLK_ALIGN uint8_t seed[MLKEM_SYMBYTES]; + int transposed; } MLK_ALIGN mlk_indcpa_public_key; #define mlk_indcpa_marshal_pk MLK_NAMESPACE_K(indcpa_marshal_pk) From 1628a544d093274d37f5fbce106f163b5f397893 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 5 May 2025 06:35:39 +0100 Subject: [PATCH 6/7] [TEST] Add skpv mulcache to structured SK Signed-off-by: Hanno Becker --- mlkem/indcpa.c | 13 ++++--------- mlkem/indcpa.h | 1 + 2 files changed, 5 insertions(+), 9 deletions(-) diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c index ea88a4f3e..5028577f8 100644 --- a/mlkem/indcpa.c +++ b/mlkem/indcpa.c @@ -140,6 +140,7 @@ void mlk_indcpa_parse_sk(mlk_indcpa_secret_key *sks, const uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES]) { mlk_polyvec_frombytes(sks->skpv, sk); + mlk_polyvec_mulcache_compute(sks->skpv_cache, sks->skpv); } /************************************************* @@ -360,7 +361,6 @@ void mlk_indcpa_keypair_derand(mlk_indcpa_public_key *pk, const uint8_t *noiseseed = buf + MLKEM_SYMBYTES; mlk_polyvec e; - mlk_polyvec_mulcache skpv_cache; MLK_ALIGN uint8_t coins_with_domain_separator[MLKEM_SYMBYTES + 1]; /* Concatenate coins with MLKEM_K for domain separation of security levels */ @@ -402,8 +402,8 @@ void mlk_indcpa_keypair_derand(mlk_indcpa_public_key *pk, mlk_polyvec_ntt(sk->skpv); mlk_polyvec_ntt(e); - mlk_polyvec_mulcache_compute(skpv_cache, sk->skpv); - mlk_matvec_mul(pk->pkpv, pk->at, sk->skpv, skpv_cache); + mlk_polyvec_mulcache_compute(sk->skpv_cache, sk->skpv); + mlk_matvec_mul(pk->pkpv, pk->at, sk->skpv, sk->skpv_cache); mlk_polyvec_tomont(pk->pkpv); mlk_polyvec_add(pk->pkpv, e); @@ -415,13 +415,11 @@ void mlk_indcpa_keypair_derand(mlk_indcpa_public_key *pk, memcpy(pk->seed, publicseed, MLKEM_SYMBYTES); mlk_polyvec_tobytes(pk->pkpv_compressed, pk->pkpv); - /* Specification: Partially implements * [@FIPS203, Section 3.3, Destruction of intermediate values] */ mlk_zeroize(buf, sizeof(buf)); mlk_zeroize(coins_with_domain_separator, sizeof(coins_with_domain_separator)); mlk_zeroize(&e, sizeof(e)); - mlk_zeroize(&skpv_cache, sizeof(skpv_cache)); } /* Reference: `indcpa_enc()` in the reference implementation [@REF]. @@ -509,13 +507,11 @@ void mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES], { mlk_polyvec b; mlk_poly v, sb; - mlk_polyvec_mulcache b_cache; mlk_unpack_ciphertext(b, &v, c); mlk_polyvec_ntt(b); - mlk_polyvec_mulcache_compute(b_cache, b); - mlk_polyvec_basemul_acc_montgomery_cached(&sb, sk->skpv, b, b_cache); + mlk_polyvec_basemul_acc_montgomery_cached(&sb, b, sk->skpv, sk->skpv_cache); mlk_poly_invntt_tomont(&sb); mlk_poly_sub(&v, &sb); @@ -526,7 +522,6 @@ void mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES], /* Specification: Partially implements * [@FIPS203, Section 3.3, Destruction of intermediate values] */ mlk_zeroize(&b, sizeof(b)); - mlk_zeroize(&b_cache, sizeof(b_cache)); mlk_zeroize(&v, sizeof(v)); mlk_zeroize(&sb, sizeof(sb)); } diff --git a/mlkem/indcpa.h b/mlkem/indcpa.h index 02b991b63..b645f405d 100644 --- a/mlkem/indcpa.h +++ b/mlkem/indcpa.h @@ -24,6 +24,7 @@ typedef struct { mlk_polyvec skpv; + mlk_polyvec_mulcache skpv_cache; } MLK_ALIGN mlk_indcpa_secret_key; #define mlk_indcpa_public_key MLK_NAMESPACE_K(mlk_indcpa_public_key) From d2d04aee3ba16313d83547c19869f5962608c4ff Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 5 May 2025 06:59:50 +0100 Subject: [PATCH 7/7] [TEST] Store marshalled PK (seed+vec) in structured PK presentation Signed-off-by: Hanno Becker --- mlkem/indcpa.c | 19 ++++++++++--------- mlkem/indcpa.h | 3 +-- mlkem/kem.c | 8 +------- 3 files changed, 12 insertions(+), 18 deletions(-) diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c index 5028577f8..7a0658b48 100644 --- a/mlkem/indcpa.c +++ b/mlkem/indcpa.c @@ -63,11 +63,9 @@ void mlk_indcpa_marshal_pk(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], const mlk_indcpa_public_key *pks) { mlk_assert_bound_2d(pks->pkpv, MLKEM_K, MLKEM_N, 0, MLKEM_Q); - memcpy(pk, pks->pkpv_compressed, MLKEM_POLYVECBYTES); - memcpy(pk + MLKEM_POLYVECBYTES, pks->seed, MLKEM_SYMBYTES); + memcpy(pk, pks->marshalled, MLKEM_INDCPA_PUBLICKEYBYTES); } - /************************************************* * Name: mlk_indcpa_parse_pk * @@ -89,8 +87,7 @@ void mlk_indcpa_parse_pk(mlk_indcpa_public_key *pks, const uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES]) { mlk_polyvec_frombytes(pks->pkpv, pk); - memcpy(pks->pkpv_compressed, pk, MLKEM_POLYVECBYTES); - memcpy(pks->seed, pk + MLKEM_POLYVECBYTES, MLKEM_SYMBYTES); + memcpy(pks->marshalled, pk, MLKEM_INDCPA_PUBLICKEYBYTES); mlk_gen_matrix(pks->at, pk + MLKEM_POLYVECBYTES, 1); pks->transposed = 1; @@ -412,8 +409,9 @@ void mlk_indcpa_keypair_derand(mlk_indcpa_public_key *pk, pk->transposed = 0; - memcpy(pk->seed, publicseed, MLKEM_SYMBYTES); - mlk_polyvec_tobytes(pk->pkpv_compressed, pk->pkpv); + /* Pack & marshal PK */ + mlk_polyvec_tobytes(pk->marshalled, pk->pkpv); + memcpy(pk->marshalled + MLKEM_POLYVECBYTES, publicseed, MLKEM_SYMBYTES); /* Specification: Partially implements * [@FIPS203, Section 3.3, Destruction of intermediate values] */ @@ -443,9 +441,12 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], mlk_poly_frommsg(&k, m); - if (pk->transposed == 0) { + if (pk->transposed == 0) + { mlk_transpose_matrix(at, pk->at); - } else { + } + else + { memcpy(at, pk->at, sizeof(mlk_polymat)); } diff --git a/mlkem/indcpa.h b/mlkem/indcpa.h index b645f405d..5a34e4460 100644 --- a/mlkem/indcpa.h +++ b/mlkem/indcpa.h @@ -32,8 +32,7 @@ typedef struct { mlk_polymat at; /* transposed matrix */ mlk_polyvec pkpv; - MLK_ALIGN uint8_t pkpv_compressed[MLKEM_POLYVECBYTES]; - MLK_ALIGN uint8_t seed[MLKEM_SYMBYTES]; + MLK_ALIGN uint8_t marshalled[MLKEM_INDCCA_PUBLICKEYBYTES]; int transposed; } MLK_ALIGN mlk_indcpa_public_key; diff --git a/mlkem/kem.c b/mlkem/kem.c index 36da96d95..1bacb720a 100644 --- a/mlkem/kem.c +++ b/mlkem/kem.c @@ -266,13 +266,10 @@ MLK_EXTERNAL_API int crypto_kem_keypair_derand_struct(mlk_public_key *pk, mlk_secret_key *sk, const uint8_t coins[2 * MLKEM_SYMBYTES]) { - MLK_ALIGN uint8_t pks[MLKEM_INDCCA_PUBLICKEYBYTES]; - mlk_indcpa_keypair_derand(&sk->indcpa_pk, &sk->indcpa_sk, coins); /* pre-compute H(pk) */ - mlk_indcpa_marshal_pk(pks, &sk->indcpa_pk); - mlk_hash_h(sk->hpk, pks, MLKEM_INDCCA_PUBLICKEYBYTES); + mlk_hash_h(sk->hpk, sk->indcpa_pk.marshalled, MLKEM_INDCPA_PUBLICKEYBYTES); /* * copy over indcpa pk and H(pk) to public key @@ -290,9 +287,6 @@ int crypto_kem_keypair_derand_struct(mlk_public_key *pk, mlk_secret_key *sk, /* Declassify public key */ MLK_CT_TESTING_DECLASSIFY(&pk->indcpa_pk, sizeof(mlk_indcpa_public_key)); - /* Specification: Partially implements - * [FIPS 203, Section 3.3, Destruction of intermediate values] */ - mlk_zeroize(pks, sizeof(pks)); return 0; }