Verify memory usage: Re-use t1/w1 buffer

This commit is the first of a series of commits reducing the stack usage of
verification.
It is hoisted out from #751

This commit places the t1 and w1 buffers into a union saving K KiB of memory.
Operations using it are slightly reordered such that their lifetime does not
overlap.
As CBMC struggles with unions (issue 8813), we use the same workaround
present in signing: Use a struct by default, and a union when
MLD_CONFIG_REDUCE_RAM is set.

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

Author: mkannwischer

mldsa/mldsa_native.h

@@ -839,13 +839,13 @@ int MLD_API_NAMESPACE(pk_from_sk)(
 #else /* MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM */
 #define MLD_TOTAL_ALLOC_44_KEYPAIR 36192
 #define MLD_TOTAL_ALLOC_44_SIGN 32448
-#define MLD_TOTAL_ALLOC_44_VERIFY 26560
+#define MLD_TOTAL_ALLOC_44_VERIFY 22464
 #define MLD_TOTAL_ALLOC_65_KEYPAIR 50048
 #define MLD_TOTAL_ALLOC_65_SIGN 44768
-#define MLD_TOTAL_ALLOC_65_VERIFY 36864
+#define MLD_TOTAL_ALLOC_65_VERIFY 30720
 #define MLD_TOTAL_ALLOC_87_KEYPAIR 66336
 #define MLD_TOTAL_ALLOC_87_SIGN 59104
-#define MLD_TOTAL_ALLOC_87_VERIFY 49408
+#define MLD_TOTAL_ALLOC_87_VERIFY 41216
 #endif /* !(MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM) */
 /* check-magic: on */
 

mldsa/src/sign.c

@@ -965,6 +965,18 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
                                 int externalmu)
 {
   int ret, cmp;
+
+  /* TODO: Remove the following workaround for
+   * https://github.com/diffblue/cbmc/issues/8813 */
+  typedef MLK_UNION_OR_STRUCT
+  {
+    mld_polyveck t1;
+    mld_polyveck w1;
+  }
+  t1w1_u;
+  mld_polyveck *t1;
+  mld_polyveck *w1;
+
   MLD_ALLOC(buf, uint8_t, (MLDSA_K * MLDSA_POLYW1_PACKEDBYTES));
   MLD_ALLOC(rho, uint8_t, MLDSA_SEEDBYTES);
   MLD_ALLOC(mu, uint8_t, MLDSA_CRHBYTES);
@@ -973,18 +985,19 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
   MLD_ALLOC(cp, mld_poly, 1);
   MLD_ALLOC(mat, mld_polymat, 1);
   MLD_ALLOC(z, mld_polyvecl, 1);
-  MLD_ALLOC(t1, mld_polyveck, 1);
-  MLD_ALLOC(w1, mld_polyveck, 1);
+  MLD_ALLOC(t1w1, t1w1_u, 1);
   MLD_ALLOC(tmp, mld_polyveck, 1);
   MLD_ALLOC(h, mld_polyveck, 1);
 
   if (buf == NULL || rho == NULL || mu == NULL || c == NULL || c2 == NULL ||
-      cp == NULL || mat == NULL || z == NULL || t1 == NULL || w1 == NULL ||
-      tmp == NULL || h == NULL)
+      cp == NULL || mat == NULL || z == NULL || t1w1 == NULL || tmp == NULL ||
+      h == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
   }
+  t1 = &t1w1->t1;
+  w1 = &t1w1->w1;
 
   if (siglen != MLDSA_CRYPTO_BYTES)
   {
@@ -1027,17 +1040,14 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
 
   /* Matrix-vector multiplication; compute Az - c2^dt1 */
   mld_poly_challenge(cp, c);
-  mld_polyvec_matrix_expand(mat, rho);
-
-  mld_polyvecl_ntt(z);
-  mld_polyvec_matrix_pointwise_montgomery(w1, mat, z);
-
   mld_poly_ntt(cp);
   mld_polyveck_shiftl(t1);
   mld_polyveck_ntt(t1);
-
   mld_polyveck_pointwise_poly_montgomery(tmp, cp, t1);
 
+  mld_polyvec_matrix_expand(mat, rho);
+  mld_polyvecl_ntt(z);
+  mld_polyvec_matrix_pointwise_montgomery(w1, mat, z);
   mld_polyveck_sub(w1, tmp);
   mld_polyveck_reduce(w1);
   mld_polyveck_invntt_tomont(w1);
@@ -1061,8 +1071,7 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
   MLD_FREE(h, mld_polyveck, 1);
   MLD_FREE(tmp, mld_polyveck, 1);
-  MLD_FREE(w1, mld_polyveck, 1);
-  MLD_FREE(t1, mld_polyveck, 1);
+  MLD_FREE(t1w1, t1w1_u, 1);
   MLD_FREE(z, mld_polyvecl, 1);
   MLD_FREE(mat, mld_polymat, 1);
   MLD_FREE(cp, mld_poly, 1);