From a260c133f7a5129660c794575a4d037dff8fd1e7 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Wed, 12 Nov 2025 13:37:16 -0800 Subject: [PATCH 1/4] ML-DSA: C Implement PK from SK Signed-off-by: Jake Massimo --- mldsa/mldsa_native.c | 1 + mldsa/src/packing.c | 78 +++++++++++++++++++ mldsa/src/packing.h | 25 ++++++ proofs/cbmc/pack_pk_from_sk/Makefile | 64 +++++++++++++++ .../pack_pk_from_sk/pack_pk_from_sk_harness.c | 11 +++ 5 files changed, 179 insertions(+) create mode 100644 proofs/cbmc/pack_pk_from_sk/Makefile create mode 100644 proofs/cbmc/pack_pk_from_sk/pack_pk_from_sk_harness.c diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index 1f5f39e4a..8d4e795dc 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -204,6 +204,7 @@ /* mldsa/src/packing.h */ #undef MLD_PACKING_H #undef mld_pack_pk +#undef mld_pack_pk_from_sk #undef mld_pack_sig #undef mld_pack_sk #undef mld_unpack_pk diff --git a/mldsa/src/packing.c b/mldsa/src/packing.c index e9cba5008..f355500b3 100644 --- a/mldsa/src/packing.c +++ b/mldsa/src/packing.c @@ -273,6 +273,84 @@ int mld_unpack_sig(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z, return mld_unpack_hints(h, sig); } +/************************************************* + * Name: mld_pack_pk_from_sk + * + * Description: Takes a private key and constructs the corresponding public key. + * Validates the reconstruction by comparing the computed t0 with + * the t0 stored in the secret key. + * + * Arguments: - uint8_t pk[]: output byte array for public key + * - const uint8_t sk[]: byte array containing bit-packed secret + *key + * + * Returns 0 on success (when computed t0 matches stored t0), -1 on failure + **************************************************/ +MLD_INTERNAL_API +int mld_pack_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 key[MLDSA_SEEDBYTES]; + mld_polyvecl mat[MLDSA_K]; + mld_polyvecl s1, s1_ntt; + mld_polyveck s2, t0, t1, t, t0_computed; + + /* Unpack secret key */ + mld_unpack_sk(rho, tr, key, &t0, &s1, &s2, sk); + + /* Expand matrix A from rho */ + mld_polyvec_matrix_expand(mat, rho); + + /* Copy s1 and convert to NTT representation */ + s1_ntt = s1; + mld_polyvecl_ntt(&s1_ntt); + + /* Matrix-vector multiplication: t = A * s1 (in NTT domain) */ + mld_polyvec_matrix_pointwise_montgomery(&t, mat, &s1_ntt); + + /* Reduce modulo field */ + mld_polyveck_reduce(&t); + + /* Take t out of NTT representation */ + mld_polyveck_invntt_tomont(&t); + + /* Add error vector: t = t + s2 */ + mld_polyveck_add(&t, &s2); + + /* Apply additional reduction for safety (as OpenSSL does) */ + mld_polyveck_reduce(&t); + + /* Extract t1 and t0 from t */ + mld_polyveck_caddq(&t); + mld_polyveck_power2round(&t1, &t0_computed, &t); + + /* Validate: compare computed t0 with t0 from secret key */ + if (memcmp(&t0, &t0_computed, sizeof(mld_polyveck)) != 0) + { + /* Validation failed - zeroize sensitive data and return error */ + mld_zeroize(&s1_ntt, sizeof(s1_ntt)); + mld_zeroize(&s1, sizeof(s1)); + mld_zeroize(&s2, sizeof(s2)); + mld_zeroize(&t0, sizeof(t0)); + mld_zeroize(key, sizeof(key)); + return -1; + } + + /* Pack public key: pk = (rho, t1) */ + mld_pack_pk(pk, rho, &t1); + + /* Zeroize secret information */ + mld_zeroize(&s1_ntt, sizeof(s1_ntt)); + mld_zeroize(&s1, sizeof(s1)); + mld_zeroize(&s2, sizeof(s2)); + mld_zeroize(&t0, sizeof(t0)); + mld_zeroize(key, sizeof(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 mld_unpack_hints diff --git a/mldsa/src/packing.h b/mldsa/src/packing.h index a5102a0dd..e4b57ab63 100644 --- a/mldsa/src/packing.h +++ b/mldsa/src/packing.h @@ -200,4 +200,29 @@ __contract__( array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2))) ensures(return_value >= 0 && return_value <= 1) ); + +#define mld_pack_pk_from_sk MLD_NAMESPACE_KL(pack_pk_from_sk) +/************************************************* + * Name: mld_pack_pk_from_sk + * + * Description: Takes a private key and constructs the corresponding public key. + * Validates the reconstruction by comparing the computed t0 with + * the t0 stored in the secret key. + * Based on OpenSSL's public_from_private implementation. + * + * Arguments: - uint8_t pk[]: output byte array for public key + * - const uint8_t sk[]: byte array containing bit-packed secret + *key + * + * Returns 0 on success (when computed t0 matches stored t0), -1 on failure + **************************************************/ +MLD_INTERNAL_API +int mld_pack_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_PACKING_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..a90207a44 --- /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 +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.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 +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); +} From d76dd951d152b287a14a5389875abd3a2b8ff585 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 13 Nov 2025 12:24:55 -0800 Subject: [PATCH 2/4] Fix CBMC proof Signed-off-by: Jake Massimo --- mldsa/src/packing.c | 27 ++++++++++++++------------- proofs/cbmc/pack_pk_from_sk/Makefile | 4 ++-- 2 files changed, 16 insertions(+), 15 deletions(-) diff --git a/mldsa/src/packing.c b/mldsa/src/packing.c index f355500b3..b3cafbcd3 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 @@ -284,7 +285,7 @@ int mld_unpack_sig(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z, * - const uint8_t sk[]: byte array containing bit-packed secret *key * - * Returns 0 on success (when computed t0 matches stored t0), -1 on failure + * Returns 0 on success, -1 on failure **************************************************/ MLD_INTERNAL_API int mld_pack_pk_from_sk(uint8_t pk[CRYPTO_PUBLICKEYBYTES], @@ -293,6 +294,7 @@ int mld_pack_pk_from_sk(uint8_t pk[CRYPTO_PUBLICKEYBYTES], MLD_ALIGN uint8_t rho[MLDSA_SEEDBYTES]; MLD_ALIGN uint8_t tr[MLDSA_TRBYTES]; MLD_ALIGN uint8_t key[MLDSA_SEEDBYTES]; + MLD_ALIGN uint8_t tr_computed[MLDSA_TRBYTES]; mld_polyvecl mat[MLDSA_K]; mld_polyvecl s1, s1_ntt; mld_polyveck s2, t0, t1, t, t0_computed; @@ -319,24 +321,23 @@ int mld_pack_pk_from_sk(uint8_t pk[CRYPTO_PUBLICKEYBYTES], /* Add error vector: t = t + s2 */ mld_polyveck_add(&t, &s2); - /* Apply additional reduction for safety (as OpenSSL does) */ + /* Apply additional reduction */ mld_polyveck_reduce(&t); /* Extract t1 and t0 from t */ mld_polyveck_caddq(&t); mld_polyveck_power2round(&t1, &t0_computed, &t); - /* Validate: compare computed t0 with t0 from secret key */ - if (memcmp(&t0, &t0_computed, sizeof(mld_polyveck)) != 0) - { - /* Validation failed - zeroize sensitive data and return error */ - mld_zeroize(&s1_ntt, sizeof(s1_ntt)); - mld_zeroize(&s1, sizeof(s1)); - mld_zeroize(&s2, sizeof(s2)); - mld_zeroize(&t0, sizeof(t0)); - mld_zeroize(key, sizeof(key)); - return -1; - } + /* TODO: Add constant time comparison to compare + * t0_computed and t0 + */ + + /* Compute shake256(tr) and check if equal to pk */ + mld_shake256(tr_computed, MLDSA_TRBYTES, pk, CRYPTO_PUBLICKEYBYTES); + + /* TODO: Add constant time comparison to compare + * tr_computed and pk + */ /* Pack public key: pk = (rho, t1) */ mld_pack_pk(pk, rho, &t1); diff --git a/proofs/cbmc/pack_pk_from_sk/Makefile b/proofs/cbmc/pack_pk_from_sk/Makefile index a90207a44..893897933 100644 --- a/proofs/cbmc/pack_pk_from_sk/Makefile +++ b/proofs/cbmc/pack_pk_from_sk/Makefile @@ -17,8 +17,6 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)pack_pk_from_sk USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)unpack_sk @@ -31,6 +29,8 @@ 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 From 0959db9b485a2c6354ab14167f59ea6abbeb21a7 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 13 Nov 2025 22:56:11 -0800 Subject: [PATCH 3/4] Second design Signed-off-by: Jake Massimo --- mldsa/mldsa_native.c | 2 +- mldsa/src/ct.h | 35 +++++++++ mldsa/src/packing.c | 78 ------------------- mldsa/src/packing.h | 24 ------ mldsa/src/sign.c | 181 ++++++++++++++++++++++++++++++++++--------- mldsa/src/sign.h | 23 ++++++ 6 files changed, 205 insertions(+), 138 deletions(-) diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index 8d4e795dc..01bee72f5 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -204,7 +204,6 @@ /* mldsa/src/packing.h */ #undef MLD_PACKING_H #undef mld_pack_pk -#undef mld_pack_pk_from_sk #undef mld_pack_sig #undef mld_pack_sk #undef mld_unpack_pk @@ -326,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 b3cafbcd3..eec3c7822 100644 --- a/mldsa/src/packing.c +++ b/mldsa/src/packing.c @@ -274,84 +274,6 @@ int mld_unpack_sig(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z, return mld_unpack_hints(h, sig); } -/************************************************* - * Name: mld_pack_pk_from_sk - * - * Description: Takes a private key and constructs the corresponding public key. - * Validates the reconstruction by comparing the computed t0 with - * the t0 stored in the secret key. - * - * Arguments: - uint8_t pk[]: output byte array for public key - * - const uint8_t sk[]: byte array containing bit-packed secret - *key - * - * Returns 0 on success, -1 on failure - **************************************************/ -MLD_INTERNAL_API -int mld_pack_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 key[MLDSA_SEEDBYTES]; - MLD_ALIGN uint8_t tr_computed[MLDSA_TRBYTES]; - mld_polyvecl mat[MLDSA_K]; - mld_polyvecl s1, s1_ntt; - mld_polyveck s2, t0, t1, t, t0_computed; - - /* Unpack secret key */ - mld_unpack_sk(rho, tr, key, &t0, &s1, &s2, sk); - - /* Expand matrix A from rho */ - mld_polyvec_matrix_expand(mat, rho); - - /* Copy s1 and convert to NTT representation */ - s1_ntt = s1; - mld_polyvecl_ntt(&s1_ntt); - - /* Matrix-vector multiplication: t = A * s1 (in NTT domain) */ - mld_polyvec_matrix_pointwise_montgomery(&t, mat, &s1_ntt); - - /* Reduce modulo field */ - mld_polyveck_reduce(&t); - - /* Take t out of NTT representation */ - mld_polyveck_invntt_tomont(&t); - - /* Add error vector: t = t + s2 */ - mld_polyveck_add(&t, &s2); - - /* Apply additional reduction */ - mld_polyveck_reduce(&t); - - /* Extract t1 and t0 from t */ - mld_polyveck_caddq(&t); - mld_polyveck_power2round(&t1, &t0_computed, &t); - - /* TODO: Add constant time comparison to compare - * t0_computed and t0 - */ - - /* Compute shake256(tr) and check if equal to pk */ - mld_shake256(tr_computed, MLDSA_TRBYTES, pk, CRYPTO_PUBLICKEYBYTES); - - /* TODO: Add constant time comparison to compare - * tr_computed and pk - */ - - /* Pack public key: pk = (rho, t1) */ - mld_pack_pk(pk, rho, &t1); - - /* Zeroize secret information */ - mld_zeroize(&s1_ntt, sizeof(s1_ntt)); - mld_zeroize(&s1, sizeof(s1)); - mld_zeroize(&s2, sizeof(s2)); - mld_zeroize(&t0, sizeof(t0)); - mld_zeroize(key, sizeof(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 mld_unpack_hints diff --git a/mldsa/src/packing.h b/mldsa/src/packing.h index e4b57ab63..84e65fd8a 100644 --- a/mldsa/src/packing.h +++ b/mldsa/src/packing.h @@ -201,28 +201,4 @@ __contract__( ensures(return_value >= 0 && return_value <= 1) ); -#define mld_pack_pk_from_sk MLD_NAMESPACE_KL(pack_pk_from_sk) -/************************************************* - * Name: mld_pack_pk_from_sk - * - * Description: Takes a private key and constructs the corresponding public key. - * Validates the reconstruction by comparing the computed t0 with - * the t0 stored in the secret key. - * Based on OpenSSL's public_from_private implementation. - * - * Arguments: - uint8_t pk[]: output byte array for public key - * - const uint8_t sk[]: byte array containing bit-packed secret - *key - * - * Returns 0 on success (when computed t0 matches stored t0), -1 on failure - **************************************************/ -MLD_INTERNAL_API -int mld_pack_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_PACKING_H */ diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c index 49eb92959..d83589161 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,82 @@ int crypto_sign_verify_pre_hash_shake256( return result; } +/************************************************* + * Name: pk_from_sk + * + * Description: Derives public key from secret key with validation. + * Checks that t0 and tr stored in sk match recomputed values. + * Based on mlkem-native's crypto_kem_check_sk pattern. + * + * 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_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 */ From 5a2dcc34dd2e4a9f2d51712aa6db609bcb799462 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 13 Nov 2025 23:02:09 -0800 Subject: [PATCH 4/4] remove double doc Signed-off-by: Jake Massimo --- mldsa/src/sign.c | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c index d83589161..f29a6011a 100644 --- a/mldsa/src/sign.c +++ b/mldsa/src/sign.c @@ -1066,18 +1066,6 @@ int crypto_sign_verify_pre_hash_shake256( return result; } -/************************************************* - * Name: pk_from_sk - * - * Description: Derives public key from secret key with validation. - * Checks that t0 and tr stored in sk match recomputed values. - * Based on mlkem-native's crypto_kem_check_sk pattern. - * - * 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_INTERNAL_API int pk_from_sk(uint8_t pk[CRYPTO_PUBLICKEYBYTES], const uint8_t sk[CRYPTO_SECRETKEYBYTES])