diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index 1f5f39e4a..01bee72f5 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -325,6 +325,7 @@ #undef crypto_sign_verify_internal #undef crypto_sign_verify_pre_hash_internal #undef crypto_sign_verify_pre_hash_shake256 +#undef pk_from_sk #if !defined(MLD_CONFIG_MONOBUILD_KEEP_SHARED_HEADERS) /* diff --git a/mldsa/src/ct.h b/mldsa/src/ct.h index dc4c9b853..afa490a80 100644 --- a/mldsa/src/ct.h +++ b/mldsa/src/ct.h @@ -240,6 +240,41 @@ __contract__( #if !defined(__ASSEMBLER__) #include +/************************************************* + * Name: mld_ct_memcmp + * + * Description: Compare two arrays for equality in constant time. + * + * Arguments: const void *a: pointer to first byte array + * const void *b: pointer to second byte array + * size_t len: length of the byte arrays + * + * Returns 0 if the byte arrays are equal, a non-zero value otherwise + **************************************************/ +static MLD_INLINE uint8_t mld_ct_memcmp(const void *a, const void *b, + const size_t len) +__contract__( + requires(len <= MLD_MAX_BUFFER_SIZE) + requires(memory_no_alias(a, len)) + requires(memory_no_alias(b, len)) +) +{ + const uint8_t *a_bytes = (const uint8_t *)a; + const uint8_t *b_bytes = (const uint8_t *)b; + uint8_t r = 0, s = 0; + size_t i; + + for (i = 0; i < len; i++) + { + r |= a_bytes[i] ^ b_bytes[i]; + /* s is useless, but prevents the loop from being aborted once r=0xff. */ + s ^= a_bytes[i] ^ b_bytes[i]; + } + + /* Convert r into a mask and XOR with s */ + return ((uint8_t)mld_value_barrier_u32((uint32_t)r) ^ s) ^ s; +} + /************************************************* * Name: mld_zeroize * diff --git a/mldsa/src/packing.c b/mldsa/src/packing.c index e9cba5008..eec3c7822 100644 --- a/mldsa/src/packing.c +++ b/mldsa/src/packing.c @@ -8,6 +8,7 @@ #include "packing.h" #include "poly.h" #include "polyvec.h" +#include "symmetric.h" /* Parameter set namespacing * This is to facilitate building multiple instances diff --git a/mldsa/src/packing.h b/mldsa/src/packing.h index a5102a0dd..84e65fd8a 100644 --- a/mldsa/src/packing.h +++ b/mldsa/src/packing.h @@ -200,4 +200,5 @@ __contract__( array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2))) ensures(return_value >= 0 && return_value <= 1) ); + #endif /* !MLD_PACKING_H */ diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c index 49eb92959..f29a6011a 100644 --- a/mldsa/src/sign.c +++ b/mldsa/src/sign.c @@ -28,6 +28,7 @@ #include #include "cbmc.h" +#include "ct.h" #include "debug.h" #include "packing.h" #include "poly.h" @@ -47,6 +48,8 @@ #define mld_H MLD_ADD_PARAM_SET(mld_H) #define mld_attempt_signature_generation \ MLD_ADD_PARAM_SET(mld_attempt_signature_generation) +#define mld_compute_t0_t1_tr_from_sk_components \ + MLD_ADD_PARAM_SET(mld_compute_t0_t1_tr_from_sk_components) /* End of parameter set namespacing */ @@ -173,6 +176,69 @@ __contract__( #endif /* !MLD_CONFIG_SERIAL_FIPS202_ONLY */ } +/************************************************* + * Name: mld_compute_t0_t1_tr_from_sk_components + * + * Description: Computes t0, t1, and tr from secret key components + * rho, s1, s2. This is the shared computation used by + * both keygen and generating the public key from the + * secret key. + * + * Arguments: - mld_polyveck *t0: output t0 + * - mld_polyveck *t1: output t1 + * - uint8_t tr[MLDSA_TRBYTES]: output tr + * - const uint8_t rho[MLDSA_SEEDBYTES]: input rho + * - const mld_polyvecl *s1: input s1 + * - const mld_polyveck *s2: input s2 + **************************************************/ +static void mld_compute_t0_t1_tr_from_sk_components( + mld_polyveck *t0, mld_polyveck *t1, uint8_t tr[MLDSA_TRBYTES], + const uint8_t rho[MLDSA_SEEDBYTES], const mld_polyvecl *s1, + const mld_polyveck *s2) +{ + mld_polyvecl mat[MLDSA_K], s1hat; + mld_polyveck t; + uint8_t pk_tmp[CRYPTO_PUBLICKEYBYTES]; + + /* Expand matrix */ + mld_polyvec_matrix_expand(mat, rho); + + /* Matrix-vector multiplication */ + s1hat = *s1; + mld_polyvecl_ntt(&s1hat); + mld_polyvec_matrix_pointwise_montgomery(&t, mat, &s1hat); + mld_polyveck_reduce(&t); + mld_polyveck_invntt_tomont(&t); + + /* Add error vector s2 */ + mld_polyveck_add(&t, s2); + + /* Reference: The following reduction is not present in the reference + * implementation. Omitting this reduction requires the output of + * the invntt to be small enough such that the addition of s2 does + * not result in absolute values >= MLDSA_Q. While our C, x86_64, + * and AArch64 invntt implementations produce small enough + * values for this to work out, it complicates the bounds + * reasoning. We instead add an additional reduction, and can + * consequently, relax the bounds requirements for the invntt. + */ + mld_polyveck_reduce(&t); + + /* Decompose to get t1, t0 */ + mld_polyveck_caddq(&t); + mld_polyveck_power2round(t1, t0, &t); + + /* Pack temporary public key and compute tr */ + mld_pack_pk(pk_tmp, rho, t1); + mld_shake256(tr, MLDSA_TRBYTES, pk_tmp, CRYPTO_PUBLICKEYBYTES); + + /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ + mld_zeroize(mat, sizeof(mat)); + mld_zeroize(&s1hat, sizeof(s1hat)); + mld_zeroize(&t, sizeof(t)); + mld_zeroize(pk_tmp, sizeof(pk_tmp)); +} + MLD_MUST_CHECK_RETURN_VALUE MLD_EXTERNAL_API int crypto_sign_keypair_internal(uint8_t pk[CRYPTO_PUBLICKEYBYTES], @@ -183,9 +249,8 @@ int crypto_sign_keypair_internal(uint8_t pk[CRYPTO_PUBLICKEYBYTES], MLD_ALIGN uint8_t inbuf[MLDSA_SEEDBYTES + 2]; MLD_ALIGN uint8_t tr[MLDSA_TRBYTES]; const uint8_t *rho, *rhoprime, *key; - mld_polyvecl mat[MLDSA_K]; - mld_polyvecl s1, s1hat; - mld_polyveck s2, t2, t1, t0; + mld_polyvecl s1; + mld_polyveck s2, t1, t0; /* Get randomness for rho, rhoprime and key */ mld_memcpy(inbuf, seed, MLDSA_SEEDBYTES); @@ -199,50 +264,24 @@ int crypto_sign_keypair_internal(uint8_t pk[CRYPTO_PUBLICKEYBYTES], /* Constant time: rho is part of the public key and, hence, public. */ MLD_CT_TESTING_DECLASSIFY(rho, MLDSA_SEEDBYTES); - /* Expand matrix */ - mld_polyvec_matrix_expand(mat, rho); - mld_sample_s1_s2(&s1, &s2, rhoprime); - - /* Matrix-vector multiplication */ - s1hat = s1; - mld_polyvecl_ntt(&s1hat); - mld_polyvec_matrix_pointwise_montgomery(&t1, mat, &s1hat); - mld_polyveck_reduce(&t1); - mld_polyveck_invntt_tomont(&t1); - /* Add error vector s2 */ - mld_polyveck_add(&t1, &s2); - - /* Reference: The following reduction is not present in the reference - * implementation. Omitting this reduction requires the output of - * the invntt to be small enough such that the addition of s2 does - * not result in absolute values >= MLDSA_Q. While our C, x86_64, - * and AArch64 invntt implementations produce small enough - * values for this to work out, it complicates the bounds - * reasoning. We instead add an additional reduction, and can - * consequently, relax the bounds requirements for the invntt. - */ - mld_polyveck_reduce(&t1); + /* Sample s1 and s2 */ + mld_sample_s1_s2(&s1, &s2, rhoprime); - /* Extract t1 and write public key */ - mld_polyveck_caddq(&t1); - mld_polyveck_power2round(&t2, &t0, &t1); - mld_pack_pk(pk, rho, &t2); + /* Compute t0, t1, tr from rho, s1, s2 */ + mld_compute_t0_t1_tr_from_sk_components(&t0, &t1, tr, rho, &s1, &s2); - /* Compute H(rho, t1) and write secret key */ - mld_shake256(tr, MLDSA_TRBYTES, pk, CRYPTO_PUBLICKEYBYTES); + /* Pack public and secret keys */ + mld_pack_pk(pk, rho, &t1); mld_pack_sk(sk, rho, tr, key, &t0, &s1, &s2); /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ mld_zeroize(seedbuf, sizeof(seedbuf)); mld_zeroize(inbuf, sizeof(inbuf)); mld_zeroize(tr, sizeof(tr)); - mld_zeroize(mat, sizeof(mat)); mld_zeroize(&s1, sizeof(s1)); - mld_zeroize(&s1hat, sizeof(s1hat)); mld_zeroize(&s2, sizeof(s2)); mld_zeroize(&t1, sizeof(t1)); - mld_zeroize(&t2, sizeof(t2)); mld_zeroize(&t0, sizeof(t0)); /* Constant time: pk is the public key, inherently public data */ @@ -1027,10 +1066,70 @@ int crypto_sign_verify_pre_hash_shake256( return result; } +MLD_INTERNAL_API +int pk_from_sk(uint8_t pk[CRYPTO_PUBLICKEYBYTES], + const uint8_t sk[CRYPTO_SECRETKEYBYTES]) +{ + MLD_ALIGN uint8_t rho[MLDSA_SEEDBYTES]; + MLD_ALIGN uint8_t tr[MLDSA_TRBYTES]; + MLD_ALIGN uint8_t tr_computed[MLDSA_TRBYTES]; + MLD_ALIGN uint8_t key[MLDSA_SEEDBYTES]; + mld_polyvecl s1; + mld_polyveck s2, t0, t0_computed, t1; + int res; + + /* Unpack secret key */ + mld_unpack_sk(rho, tr, key, &t0, &s1, &s2, sk); + + /* The parts being validated (tr) are public, so no secret info + * is leaked through the runtime or return value */ + MLD_CT_TESTING_DECLASSIFY(tr, MLDSA_TRBYTES); + + /* Recompute t0, t1, tr from rho, s1, s2 */ + mld_compute_t0_t1_tr_from_sk_components(&t0_computed, &t1, tr_computed, rho, + &s1, &s2); + + /* Validate t0 using constant-time comparison */ + res = mld_ct_memcmp(&t0, &t0_computed, sizeof(mld_polyveck)); + if (res != 0) + { + res = -1; + goto cleanup; + } + + /* Validate tr using constant-time comparison */ + res = mld_ct_memcmp(tr, tr_computed, MLDSA_TRBYTES); + if (res != 0) + { + res = -1; + goto cleanup; + } + + /* Pack public key */ + mld_pack_pk(pk, rho, &t1); + + /* Declassify public key */ + MLD_CT_TESTING_DECLASSIFY(pk, CRYPTO_PUBLICKEYBYTES); + + res = 0; + +cleanup: + /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ + mld_zeroize(&s1, sizeof(s1)); + mld_zeroize(&s2, sizeof(s2)); + mld_zeroize(&t0, sizeof(t0)); + mld_zeroize(&t0_computed, sizeof(t0_computed)); + mld_zeroize(key, sizeof(key)); + mld_zeroize(tr_computed, sizeof(tr_computed)); + + return res; +} + /* To facilitate single-compilation-unit (SCU) builds, undefine all macros. * Don't modify by hand -- this is auto-generated by scripts/autogen. */ #undef mld_check_pct #undef mld_sample_s1_s2 #undef mld_H #undef mld_attempt_signature_generation +#undef mld_compute_t0_t1_tr_from_sk_components #undef NONCE_UB diff --git a/mldsa/src/sign.h b/mldsa/src/sign.h index e4a21f58b..d97f0c6ff 100644 --- a/mldsa/src/sign.h +++ b/mldsa/src/sign.h @@ -46,6 +46,7 @@ #define crypto_sign_keypair_internal MLD_NAMESPACE_KL(keypair_internal) #define crypto_sign_keypair MLD_NAMESPACE_KL(keypair) +#define pk_from_sk MLD_NAMESPACE_KL(pk_from_sk) #define crypto_sign_signature_internal MLD_NAMESPACE_KL(signature_internal) #define crypto_sign_signature MLD_NAMESPACE_KL(signature) #define crypto_sign_signature_extmu MLD_NAMESPACE_KL(signature_extmu) @@ -625,4 +626,26 @@ __contract__( ensures(return_value == 0 || return_value == -1) ); +/************************************************* + * Name: pk_from_sk + * + * Description: Derives public key from secret key with validation. + * Checks that t0 and tr stored in sk match recomputed values. + * + * Arguments: - uint8_t pk[CRYPTO_PUBLICKEYBYTES]: output public key + * - const uint8_t sk[CRYPTO_SECRETKEYBYTES]: input secret key + * + * Returns 0 on success, -1 if validation fails (corrupted secret key) + **************************************************/ +MLD_MUST_CHECK_RETURN_VALUE +MLD_INTERNAL_API +int pk_from_sk(uint8_t pk[CRYPTO_PUBLICKEYBYTES], + const uint8_t sk[CRYPTO_SECRETKEYBYTES]) +__contract__( + requires(memory_no_alias(pk, CRYPTO_PUBLICKEYBYTES)) + requires(memory_no_alias(sk, CRYPTO_SECRETKEYBYTES)) + assigns(memory_slice(pk, CRYPTO_PUBLICKEYBYTES)) + ensures(return_value == 0 || return_value == -1) +); + #endif /* !MLD_SIGN_H */ diff --git a/proofs/cbmc/pack_pk_from_sk/Makefile b/proofs/cbmc/pack_pk_from_sk/Makefile new file mode 100644 index 000000000..893897933 --- /dev/null +++ b/proofs/cbmc/pack_pk_from_sk/Makefile @@ -0,0 +1,64 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = pack_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 = pack_pk_from_sk + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)pack_pk_from_sk +USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)unpack_sk +USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_expand +USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvecl_ntt +USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_pointwise_montgomery +USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_reduce +USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_invntt_tomont +USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_add +USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_caddq +USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_power2round +USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)pack_pk +USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256 +USE_FUNCTION_CONTRACTS+=mld_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 --no-array-field-sensitivity --slice-formula + +FUNCTION_NAME = pack_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 = 11 + +# 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 +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/pack_pk_from_sk/pack_pk_from_sk_harness.c b/proofs/cbmc/pack_pk_from_sk/pack_pk_from_sk_harness.c new file mode 100644 index 000000000..cfac82b91 --- /dev/null +++ b/proofs/cbmc/pack_pk_from_sk/pack_pk_from_sk_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "packing.h" + +void harness(void) +{ + uint8_t *pk; + const uint8_t *sk; + mld_pack_pk_from_sk(pk, sk); +}