Lowram: Share buffers with non-overlapping lifetimes in verify

integration/opentitan/reduce_alloc.patch

@@ -1,7 +1,7 @@
 # Copyright (c) The mldsa-native project authors
 # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 diff --git a/sw/device/lib/crypto/include/mldsa.h b/sw/device/lib/crypto/include/mldsa.h
-index be11f20..26351ee 100644
+index be11f20..0000000 100644
 --- a/sw/device/lib/crypto/include/mldsa.h
 +++ b/sw/device/lib/crypto/include/mldsa.h
 @@ -41,16 +41,16 @@ enum {
@@ -10,20 +10,23 @@ index be11f20..26351ee 100644
    // Work buffer sizes in 32-bit words
 -  kOtcryptoMldsa44WorkBufferKeypairWords = 32992 / sizeof(uint32_t),
 -  kOtcryptoMldsa44WorkBufferSignWords = 32448 / sizeof(uint32_t),
+-  kOtcryptoMldsa44WorkBufferVerifyWords = 22464 / sizeof(uint32_t),
 +  kOtcryptoMldsa44WorkBufferKeypairWords = 28960 / sizeof(uint32_t),
 +  kOtcryptoMldsa44WorkBufferSignWords = 20256 / sizeof(uint32_t),
-   kOtcryptoMldsa44WorkBufferVerifyWords = 22464 / sizeof(uint32_t),
++  kOtcryptoMldsa44WorkBufferVerifyWords = 13248 / sizeof(uint32_t),
 
 -  kOtcryptoMldsa65WorkBufferKeypairWords = 46304 / sizeof(uint32_t),
 -  kOtcryptoMldsa65WorkBufferSignWords = 44768 / sizeof(uint32_t),
+-  kOtcryptoMldsa65WorkBufferVerifyWords = 30720 / sizeof(uint32_t),
 +  kOtcryptoMldsa65WorkBufferKeypairWords = 40224 / sizeof(uint32_t),
 +  kOtcryptoMldsa65WorkBufferSignWords = 27456 / sizeof(uint32_t),
-   kOtcryptoMldsa65WorkBufferVerifyWords = 30720 / sizeof(uint32_t),
++  kOtcryptoMldsa65WorkBufferVerifyWords = 18400 / sizeof(uint32_t),
 
 -  kOtcryptoMldsa87WorkBufferKeypairWords = 62688 / sizeof(uint32_t),
 -  kOtcryptoMldsa87WorkBufferSignWords = 59104 / sizeof(uint32_t),
+-  kOtcryptoMldsa87WorkBufferVerifyWords = 41216 / sizeof(uint32_t),
 +  kOtcryptoMldsa87WorkBufferKeypairWords = 54560 / sizeof(uint32_t),
 +  kOtcryptoMldsa87WorkBufferSignWords = 35648 / sizeof(uint32_t),
-   kOtcryptoMldsa87WorkBufferVerifyWords = 41216 / sizeof(uint32_t),
++  kOtcryptoMldsa87WorkBufferVerifyWords = 24800 / sizeof(uint32_t),
  };
 

mldsa/mldsa_native.c

@@ -261,8 +261,8 @@
 #undef mld_pack_sig_c_h
 #undef mld_pack_sig_z
 #undef mld_pack_sk
+#undef mld_unpack_hints
 #undef mld_unpack_pk
-#undef mld_unpack_sig
 #undef mld_unpack_sk
 /* mldsa/src/params.h */
 #undef MLDSA_BETA

mldsa/mldsa_native.h

@@ -932,17 +932,17 @@ int MLD_API_NAMESPACE(pk_from_sk)(
 #define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 28960
 #define MLD_TOTAL_ALLOC_44_PK_FROM_SK 32992
 #define MLD_TOTAL_ALLOC_44_SIGN 20256
-#define MLD_TOTAL_ALLOC_44_VERIFY 22464
+#define MLD_TOTAL_ALLOC_44_VERIFY 13248
 #define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 40224
 #define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 40224
 #define MLD_TOTAL_ALLOC_65_PK_FROM_SK 46304
 #define MLD_TOTAL_ALLOC_65_SIGN 27456
-#define MLD_TOTAL_ALLOC_65_VERIFY 30720
+#define MLD_TOTAL_ALLOC_65_VERIFY 18400
 #define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 54560
 #define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 54560
 #define MLD_TOTAL_ALLOC_87_PK_FROM_SK 62688
 #define MLD_TOTAL_ALLOC_87_SIGN 35648
-#define MLD_TOTAL_ALLOC_87_VERIFY 41216
+#define MLD_TOTAL_ALLOC_87_VERIFY 24800
 #endif /* !(MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM) */
 /* check-magic: on */
 

mldsa/mldsa_native_asm.S

@@ -264,8 +264,8 @@
 #undef mld_pack_sig_c_h
 #undef mld_pack_sig_z
 #undef mld_pack_sk
+#undef mld_unpack_hints
 #undef mld_unpack_pk
-#undef mld_unpack_sig
 #undef mld_unpack_sk
 /* mldsa/src/params.h */
 #undef MLDSA_BETA

mldsa/src/packing.c

@@ -13,7 +13,6 @@
  * This is to facilitate building multiple instances
  * of mldsa-native (e.g. with varying parameter sets)
  * within a single compilation unit. */
-#define mld_unpack_hints MLD_ADD_PARAM_SET(mld_unpack_hints)
 /* End of parameter set namespacing */
 
 MLD_INTERNAL_API
@@ -192,17 +191,9 @@ void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi,
  *
  * Returns 1 in case of malformed hints; otherwise 0.
  **************************************************/
-static int mld_unpack_hints(
-    mld_polyveck *h, const uint8_t packed_hints[MLDSA_POLYVECH_PACKEDBYTES])
-__contract__(
-  requires(memory_no_alias(packed_hints, MLDSA_POLYVECH_PACKEDBYTES))
-  requires(memory_no_alias(h, sizeof(mld_polyveck)))
-  assigns(memory_slice(h, sizeof(mld_polyveck)))
-  /* All returned coefficients are either 0 or 1 */
-  ensures(forall(k1, 0, MLDSA_K,
-    array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
-  ensures(return_value >= 0 && return_value <= 1)
-)
+MLD_INTERNAL_API
+int mld_unpack_hints(mld_polyveck *h,
+                     const uint8_t packed_hints[MLDSA_POLYVECH_PACKEDBYTES])
 {
   unsigned int i, j;
   unsigned int old_hint_count;
@@ -275,19 +266,5 @@ __contract__(
   return 0;
 }
 
-MLD_INTERNAL_API
-int mld_unpack_sig(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z,
-                   mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES])
-{
-  mld_memcpy(c, sig, MLDSA_CTILDEBYTES);
-  sig += MLDSA_CTILDEBYTES;
-
-  mld_polyvecl_unpack_z(z, sig);
-  sig += MLDSA_L * MLDSA_POLYZ_PACKEDBYTES;
-
-  return mld_unpack_hints(h, sig);
-}
-
 /* To facilitate single-compilation-unit (SCU) builds, undefine all macros.
  * Don't modify by hand -- this is auto-generated by scripts/autogen. */
-#undef mld_unpack_hints

mldsa/src/packing.h

@@ -193,36 +193,29 @@ __contract__(
     array_abs_bound(s2->vec.vec[k2].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
 );
 
-#define mld_unpack_sig MLD_NAMESPACE_KL(unpack_sig)
+#define mld_unpack_hints MLD_NAMESPACE_KL(unpack_hints)
 /*************************************************
- * Name:        mld_unpack_sig
+ * Name:        mld_unpack_hints
  *
- * Description: Unpack signature sig = (c, z, h).
+ * Description: Unpack hint vector h from packed hint bytes in signature.
  *
- * Arguments:   - uint8_t *c: pointer to output challenge hash
- *              - mld_polyvecl *z: pointer to output vector z
- *              - mld_polyveck *h: pointer to output hint vector h
- *              - const uint8_t sig[]: byte array containing
- *                bit-packed signature
+ * Arguments:   - mld_polyveck *h: pointer to output hint vector
+ *              - const uint8_t *packed_hints: pointer to
+ *                raw hint bytes (MLDSA_POLYVECH_PACKEDBYTES)
  *
- * Returns 1 in case of malformed signature; otherwise 0.
+ * Returns 1 in case of malformed hints; otherwise 0.
  **************************************************/
 MLD_INTERNAL_API
 MLD_MUST_CHECK_RETURN_VALUE
-int mld_unpack_sig(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z,
-                   mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES])
+int mld_unpack_hints(mld_polyveck *h,
+                     const uint8_t packed_hints[MLDSA_POLYVECH_PACKEDBYTES])
 __contract__(
-  requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
-  requires(memory_no_alias(c, MLDSA_CTILDEBYTES))
-  requires(memory_no_alias(z, sizeof(mld_polyvecl)))
+  requires(memory_no_alias(packed_hints, MLDSA_POLYVECH_PACKEDBYTES))
   requires(memory_no_alias(h, sizeof(mld_polyveck)))
-  assigns(memory_slice(c, MLDSA_CTILDEBYTES))
-  assigns(memory_slice(z, sizeof(mld_polyvecl)))
   assigns(memory_slice(h, sizeof(mld_polyveck)))
-  ensures(forall(k0, 0, MLDSA_L,
-    array_bound(z->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)))
   ensures(forall(k1, 0, MLDSA_K,
     array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
   ensures(return_value >= 0 && return_value <= 1)
 );
+
 #endif /* !MLD_PACKING_H */

mldsa/src/sign.c

@@ -1082,51 +1082,53 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
    * https://github.com/diffblue/cbmc/issues/8813 */
   typedef MLD_UNION_OR_STRUCT
   {
+    mld_polyvecl z;
+    mld_poly cp;
+  }
+  zcp_u;
+  mld_polyvecl *z;
+  mld_poly *cp;
+
+  /* TODO: Remove the following workaround for
+   * https://github.com/diffblue/cbmc/issues/8813 */
+  typedef MLD_UNION_OR_STRUCT
+  {
+    mld_polymat mat;
     mld_polyveck t1;
-    mld_polyveck w1;
+    mld_polyveck tmp;
+    mld_polyveck h;
   }
-  t1w1_u;
-  mld_polyveck *t1;
-  mld_polyveck *w1;
+  reuse_u;
 
   MLD_ALLOC(buf, uint8_t, (MLDSA_K * MLDSA_POLYW1_PACKEDBYTES), context);
   MLD_ALLOC(rho, uint8_t, MLDSA_SEEDBYTES, context);
   MLD_ALLOC(mu, uint8_t, MLDSA_CRHBYTES, context);
   MLD_ALLOC(c, uint8_t, MLDSA_CTILDEBYTES, context);
   MLD_ALLOC(c2, uint8_t, MLDSA_CTILDEBYTES, context);
-  MLD_ALLOC(cp, mld_poly, 1, context);
-  MLD_ALLOC(mat, mld_polymat, 1, context);
-  MLD_ALLOC(z, mld_polyvecl, 1, context);
-  MLD_ALLOC(t1w1, t1w1_u, 1, context);
-  MLD_ALLOC(tmp, mld_polyveck, 1, context);
-  MLD_ALLOC(h, mld_polyveck, 1, context);
+  MLD_ALLOC(zcp, zcp_u, 1, context);
+  MLD_ALLOC(w1, mld_polyveck, 1, context);
+  MLD_ALLOC(reuse, reuse_u, 1, context);
 
   if (buf == NULL || rho == NULL || mu == NULL || c == NULL || c2 == NULL ||
-      cp == NULL || mat == NULL || z == NULL || t1w1 == NULL || tmp == NULL ||
-      h == NULL)
+      zcp == NULL || w1 == NULL || reuse == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
   }
-  t1 = &t1w1->t1;
-  w1 = &t1w1->w1;
+  z = &zcp->z;
+  cp = &zcp->cp;
 
   if (siglen != MLDSA_CRYPTO_BYTES)
   {
     ret = MLD_ERR_FAIL;
     goto cleanup;
   }
 
-  mld_unpack_pk(rho, t1, pk);
+  mld_memcpy(rho, pk, MLDSA_SEEDBYTES);
+
+  mld_memcpy(c, sig, MLDSA_CTILDEBYTES);
+  mld_polyvecl_unpack_z(z, sig + MLDSA_CTILDEBYTES);
 
-  /* mld_unpack_sig and mld_polyvecl_chknorm signal failure through a
-   * single non-zero error code that's not yet aligned with MLD_ERR_XXX.
-   * Map it to MLD_ERR_FAIL explicitly. */
-  if (mld_unpack_sig(c, z, h, sig))
-  {
-    ret = MLD_ERR_FAIL;
-    goto cleanup;
-  }
   if (mld_polyvecl_chknorm(z, MLDSA_GAMMA1 - MLDSA_BETA))
   {
     ret = MLD_ERR_FAIL;
@@ -1151,23 +1153,31 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
   }
 
   /* Matrix-vector multiplication; compute Az - c2^dt1 */
+  mld_polyvecl_ntt(z);
+  mld_polyvec_matrix_expand(&reuse->mat, rho);
+  mld_polyvec_matrix_pointwise_montgomery(w1, &reuse->mat, z);
+
   mld_poly_challenge(cp, c);
   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_unpack_pk(rho, &reuse->t1, pk);
+  mld_polyveck_shiftl(&reuse->t1);
+  mld_polyveck_ntt(&reuse->t1);
+  mld_polyveck_pointwise_poly_montgomery(&reuse->tmp, cp, &reuse->t1);
+  mld_polyveck_sub(w1, &reuse->tmp);
   mld_polyveck_reduce(w1);
   mld_polyveck_invntt_tomont(w1);
 
   /* Reconstruct w1 */
   mld_polyveck_caddq(w1);
-  mld_polyveck_use_hint(tmp, w1, h);
-  mld_polyveck_pack_w1(buf, tmp);
+  if (mld_unpack_hints(&reuse->h, sig + MLDSA_CTILDEBYTES +
+                                      MLDSA_L * MLDSA_POLYZ_PACKEDBYTES))
+  {
+    ret = MLD_ERR_FAIL;
+    goto cleanup;
+  }
+  mld_polyveck_use_hint(&reuse->tmp, w1, &reuse->h);
+  mld_polyveck_pack_w1(buf, &reuse->tmp);
+
   /* Call random oracle and verify challenge */
   mld_H(c2, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, buf,
         MLDSA_K * MLDSA_POLYW1_PACKEDBYTES, NULL, 0);
@@ -1181,12 +1191,9 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
 
 cleanup:
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
-  MLD_FREE(h, mld_polyveck, 1, context);
-  MLD_FREE(tmp, mld_polyveck, 1, context);
-  MLD_FREE(t1w1, t1w1_u, 1, context);
-  MLD_FREE(z, mld_polyvecl, 1, context);
-  MLD_FREE(mat, mld_polymat, 1, context);
-  MLD_FREE(cp, mld_poly, 1, context);
+  MLD_FREE(reuse, reuse_u, 1, context);
+  MLD_FREE(w1, mld_polyveck, 1, context);
+  MLD_FREE(zcp, zcp_u, 1, context);
   MLD_FREE(c2, uint8_t, MLDSA_CTILDEBYTES, context);
   MLD_FREE(c, uint8_t, MLDSA_CTILDEBYTES, context);
   MLD_FREE(mu, uint8_t, MLDSA_CRHBYTES, context);

proofs/cbmc/sign_verify_internal/Makefile

@@ -21,8 +21,9 @@ PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c
 
 CHECK_FUNCTION_CONTRACTS=mld_verify_internal
 USE_FUNCTION_CONTRACTS=mld_unpack_pk
-USE_FUNCTION_CONTRACTS+=mld_unpack_sig
+USE_FUNCTION_CONTRACTS+=mld_polyvecl_unpack_z
 USE_FUNCTION_CONTRACTS+=mld_polyvecl_chknorm
+USE_FUNCTION_CONTRACTS+=mld_unpack_hints
 USE_FUNCTION_CONTRACTS+=mld_H
 USE_FUNCTION_CONTRACTS+=mld_poly_challenge
 USE_FUNCTION_CONTRACTS+=mld_polyvec_matrix_expand