verify: Switch to constant-time memcmp

In the very 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 thi 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 selections allows us to not use any
declassifications in verification, i.e., we do not leak the verification
result through timing.

Signed-off-by: Matthias J. Kannwischer <[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,8 @@ 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 = 0;
+  ret = mld_ct_sel_int32(MLD_ERR_FAIL, 0,
+                         mld_ct_memcmp(c, c2, MLDSA_CTILDEBYTES));
 
 cleanup:
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
@@ -1056,6 +1035,9 @@ int crypto_sign_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen,
   *mlen = smlen - MLDSA_CRYPTO_BYTES;
   ret = crypto_sign_verify(sm, MLDSA_CRYPTO_BYTES, sm + MLDSA_CRYPTO_BYTES,
                            *mlen, ctx, ctxlen, pk);
+  /* Declassify the final result of the verification. */
+  /* TODO: Consider making open constant flow */
+  MLD_CT_TESTING_DECLASSIFY(&ret, sizeof(ret));
   if (ret == 0)
   {
     /* All good, copy msg, return 0 */

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