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 <matthias@kannwischer.eu>

Author: mkannwischer

mldsa/src/sign.c

@@ -782,7 +782,6 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
                                 const uint8_t pk[CRYPTO_PUBLICKEYBYTES],
                                 int externalmu)
 {
-  unsigned int i;
   int res;
   MLD_ALIGN uint8_t buf[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES];
   MLD_ALIGN uint8_t rho[MLDSA_SEEDBYTES];
@@ -853,28 +852,18 @@ 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, sizeof(c2));
-  for (i = 0; i < MLDSA_CTILDEBYTES; ++i)
-  __loop__(
-    invariant(i <= MLDSA_CTILDEBYTES)
-  )
-  {
-    if (c[i] != c2[i])
-    {
-      res = -1;
-      goto cleanup;
-    }
-  }
 
-  res = 0;
+
+  /* Constant time: Leaking the result of the signature verification is fine in
+   *                the vast majority of the cases. However, performing all
+   *                of verification in constant-time only has negligible
+   *                performance overhead. This way we do not have to declassify
+   *                the message.
+   */
+  /* Return 0 if c == c2, -1 otherwise */
+  res = mld_ct_sel_int32(
+      -1, 0,
+      mld_ct_cmask_neg_i32(-(int32_t)mld_ct_memcmp(c, c2, MLDSA_CTILDEBYTES)));
 
 cleanup:
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */

proofs/cbmc/crypto_sign_verify_internal/Makefile

@@ -39,6 +39,9 @@ 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_cmask_neg_i32
+USE_FUNCTION_CONTRACTS+=mld_ct_sel_int32
 
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1