pk_from_sk: Add validation of s1 and s2

Altenative to #807

This commit adds validation of the s1 and s2 components of the secret key
to the pk_from_sk function. It checks if coefficients are within the valid
bound [-MLDSA_ETA, MLDSA_ETA] by using the chknorm function that is
already present in the code.

Documentation and CBMC proofs are adjusted accordingly.

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

Author: mkannwischer

mldsa/mldsa_native.h

@@ -735,8 +735,12 @@ size_t MLD_API_NAMESPACE(prepare_domain_separation_prefix)(
 /*************************************************
  * Name:        crypto_sign_pk_from_sk
  *
- * Description: Derives public key from secret key with validation.
- *              Checks that t0 and tr stored in sk match recomputed values.
+ * Description: Derives public key from secret key.
+ *              Validity of the the secret key is checked with the following
+ *              tests:
+ *                - Check that s0 and s1 have coefficients in
+ *                  [-MLDSA_ETA, MLDSA_ETA]
+ *                - Check 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

mldsa/src/sign.c

@@ -1297,7 +1297,7 @@ MLD_EXTERNAL_API
 int crypto_sign_pk_from_sk(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
                            const uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES])
 {
-  uint8_t cmp, cmp0, cmp1;
+  uint8_t cmp, cmp0, cmp1, cmp2, cmp3;
   int ret;
   MLD_ALLOC(rho, uint8_t, MLDSA_SEEDBYTES);
   MLD_ALLOC(tr, uint8_t, MLDSA_TRBYTES);
@@ -1320,6 +1320,10 @@ int crypto_sign_pk_from_sk(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
   /* Unpack secret key */
   mld_unpack_sk(rho, tr, key, t0, s1, s2, sk);
 
+  /* Validate s1 and s2 coefficients are within [-MLDSA_ETA, MLDSA_ETA] */
+  cmp2 = mld_polyvecl_chknorm(s1, MLDSA_ETA + 1) & 0xFF;
+  cmp3 = mld_polyveck_chknorm(s2, MLDSA_ETA + 1) & 0xFF;
+
   /* Recompute t0, t1, tr, and pk from rho, s1, s2 */
   ret = mld_compute_t0_t1_tr_from_sk_components(t0_computed, t1, tr_computed,
                                                 pk, rho, s1, s2);
@@ -1333,7 +1337,7 @@ int crypto_sign_pk_from_sk(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
                        sizeof(mld_polyveck));
   cmp1 = mld_ct_memcmp((const uint8_t *)tr, (const uint8_t *)tr_computed,
                        MLDSA_TRBYTES);
-  cmp = mld_value_barrier_u8(cmp0 | cmp1);
+  cmp = mld_value_barrier_u8(cmp0 | cmp1 | cmp2 | cmp3);
 
   /* Declassify the final result of the validity check. */
   MLD_CT_TESTING_DECLASSIFY(&cmp, sizeof(cmp));

mldsa/src/sign.h

@@ -745,8 +745,12 @@ __contract__(
 /*************************************************
  * Name:        crypto_sign_pk_from_sk
  *
- * Description: Derives public key from secret key with validation.
- *              Checks that t0 and tr stored in sk match recomputed values.
+ * Description: Derives public key from secret key.
+ *              Validity of the the secret key is checked with the following
+ *              tests:
+ *                - Check that s0 and s1 have coefficients in
+ *                  [-MLDSA_ETA, MLDSA_ETA]
+ *                - Check that t0 and tr stored in sk match recomputed values.
  *
  * Arguments:   - uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES]: output public key
  *              - const uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES]: input secret

proofs/cbmc/crypto_sign_pk_from_sk/Makefile

@@ -22,6 +22,8 @@ PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c
 CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)pk_from_sk
 USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)unpack_sk
 USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)pack_pk
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvecl_chknorm
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_chknorm
 USE_FUNCTION_CONTRACTS+=mld_compute_t0_t1_tr_from_sk_components
 USE_FUNCTION_CONTRACTS+=mld_value_barrier_u8
 USE_FUNCTION_CONTRACTS+=mld_ct_memcmp