verify: Switch to constant-time memcmp

At the end of verify one has to compare the input challenge to the
re-computed challenge. If they are equal (and some previous checks on
h and z passed), the signature is valid.

Currently, our constant-time tests do not declassify the message and we,
hence, need to declassify in this final step. Before this commit, the
declassification would happen on the recomputed challenge just before
the memcmp.

Now that a constant-time memcmp was added in #714, we might as well
use that; that, plus a constant-time selection, allows us to not use
message-dependent branches.

For now, we still declassify the result of the verification itself to
allow branching on it, e.g. in crypto_sign_open. This may be further
improved in subsequent work, making crypto_sign_open constant flow
and leaving a potential declassification of the verification result
to the call-sites.

Signed-off-by: Matthias J. Kannwischer <[email protected]>
Signed-off-by: Hanno Becker <[email protected]>

Author: mkannwischer

mldsa/src/sign.c

@@ -874,7 +874,6 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
                                 const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
                                 int externalmu)
 {
-  unsigned int i;
   int ret;
   MLD_ALLOC(buf, uint8_t, (MLDSA_K * MLDSA_POLYW1_PACKEDBYTES));
   MLD_ALLOC(rho, uint8_t, MLDSA_SEEDBYTES);
@@ -961,28 +960,11 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
   mld_H(c2, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, buf,
         MLDSA_K * MLDSA_POLYW1_PACKEDBYTES, NULL, 0);
 
-  /* Constant time: All data in verification is usually considered public.
-   * However, in our constant-time tests we do not declassify the message and
-   * context string.
-   * The following conditional is the only place in verification whose run-time
-   * depends on the message. As all that can be leakaged here is the output of
-   * a hash call (that should behave like a random oracle), it is safe to
-   * declassify here even with a secret message.
-   */
-  MLD_CT_TESTING_DECLASSIFY(c2, MLDSA_CTILDEBYTES);
-  ret = MLD_ERR_FAIL;
-  for (i = 0; i < MLDSA_CTILDEBYTES; ++i)
-  __loop__(
-    invariant(i <= MLDSA_CTILDEBYTES)
-  )
-  {
-    if (c[i] != c2[i])
-    {
-      goto cleanup;
-    }
-  }
+  ret = mld_ct_sel_int32(MLD_ERR_FAIL, 0,
+                         mld_ct_memcmp(c, c2, MLDSA_CTILDEBYTES));
 
-  ret = 0;
+  /* Declassify the final result of the verification. */
+  MLD_CT_TESTING_DECLASSIFY(&ret, sizeof(ret));
 
 cleanup:
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */

proofs/cbmc/crypto_sign_verify_internal/Makefile

@@ -39,6 +39,8 @@ USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_caddq
 USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_use_hint
 USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_pack_w1
 USE_FUNCTION_CONTRACTS+=mld_zeroize
+USE_FUNCTION_CONTRACTS+=mld_ct_memcmp
+USE_FUNCTION_CONTRACTS+=mld_ct_sel_int32
 
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1