C: Public Key from Secret Key function

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)
 /*

mldsa/src/ct.h

@@ -240,6 +240,41 @@ __contract__(
 #if !defined(__ASSEMBLER__)
 #include <string.h>
 
+/*************************************************
+ * 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
  *

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

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 */

mldsa/src/sign.c

@@ -28,6 +28,7 @@
 #include <string.h>
 
 #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

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 */

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