Serial FIPS202 2/3: Adapt mld_sample_s1_s2

This commit changes mld_sample_s1_s2 to use poly_uniform_eta only in case
MLD_CONFIG_SERIAL_FIPS202_ONLY is set.

poly_uniform_eta was previously removed because we don't need it in case
batching is enabled. It is re-added here.

A new CBMC proof for poly_uniform_eta is added.
An additional CBMC proof for sample_s1_s2 with MLD_CONFIG_SERIAL_FIPS202_ONLY
set is added.

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

Author: mkannwischer

mldsa/poly.h

@@ -425,6 +425,30 @@ __contract__(
   ensures(array_abs_bound(r3->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
 );
 
+#define mld_poly_uniform_eta MLD_NAMESPACE_KL(poly_uniform_eta)
+/*************************************************
+ * Name:        mld_poly_uniform_eta
+ *
+ * Description: Sample polynomial with uniformly random coefficients
+ *              in [-MLDSA_ETA,MLDSA_ETA] by performing rejection sampling on
+ *              the output stream from SHAKE256(seed|nonce)
+ *
+ * Arguments:   - mld_poly *r: pointer to output polynomial
+ *              - const uint8_t seed[]: byte array with seed of length
+ *                MLDSA_CRHBYTES
+ *              - uint8_t nonce: nonce
+ **************************************************/
+MLD_INTERNAL_API
+void mld_poly_uniform_eta(mld_poly *r, const uint8_t seed[MLDSA_CRHBYTES],
+                          uint8_t nonce)
+__contract__(
+  requires(memory_no_alias(r, sizeof(mld_poly)))
+  requires(memory_no_alias(seed, MLDSA_CRHBYTES))
+  assigns(memory_slice(r, sizeof(mld_poly)))
+  ensures(array_abs_bound(r->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
+);
+
+
 #define mld_poly_uniform_gamma1 MLD_NAMESPACE_KL(poly_uniform_gamma1)
 /*************************************************
  * Name:        mld_poly_uniform_gamma1

mldsa/poly_kl.c

@@ -318,6 +318,7 @@ __contract__(
   return ctr;
 }
 
+#if !defined(MLD_CONFIG_SERIAL_FIPS202_ONLY)
 MLD_INTERNAL_API
 void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
                              mld_poly *r3, const uint8_t seed[MLDSA_CRHBYTES],
@@ -401,6 +402,62 @@ void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
   mld_zeroize(buf, sizeof(buf));
   mld_zeroize(extseed, sizeof(extseed));
 }
+#else  /* !MLD_CONFIG_SERIAL_FIPS202_ONLY */
+MLD_INTERNAL_API
+void mld_poly_uniform_eta(mld_poly *r, const uint8_t seed[MLDSA_CRHBYTES],
+                          uint8_t nonce)
+{
+  /* Temporary buffer for XOF output before rejection sampling */
+  MLD_ALIGN uint8_t buf[POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES];
+  MLD_ALIGN uint8_t extseed[MLDSA_CRHBYTES + 2];
+
+  /* Tracks the number of coefficients we have already sampled */
+  unsigned ctr;
+  mld_xof256_ctx state;
+  unsigned buflen;
+
+  mld_memcpy(extseed, seed, MLDSA_CRHBYTES);
+  extseed[MLDSA_CRHBYTES] = nonce;
+  extseed[MLDSA_CRHBYTES + 1] = 0;
+
+  mld_xof256_init(&state);
+  mld_xof256_absorb_once(&state, extseed, MLDSA_CRHBYTES + 2);
+
+  /*
+   * Initially, squeeze heuristic number of POLY_UNIFORM_ETA_NBLOCKS.
+   * This should generate the coefficients with high probability.
+   */
+  mld_xof256_squeezeblocks(buf, POLY_UNIFORM_ETA_NBLOCKS, &state);
+  buflen = POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES;
+
+  ctr = mld_rej_eta(r->coeffs, MLDSA_N, 0, buf, buflen);
+
+  /*
+   * So long as not all entries have been generated, squeeze
+   * one more block a time until we're done.
+   */
+  buflen = STREAM256_BLOCKBYTES;
+  while (ctr < MLDSA_N)
+  __loop__(
+    assigns(ctr, memory_slice(&state, sizeof(mld_xof256_ctx)),
+      memory_slice(buf, STREAM256_BLOCKBYTES), memory_slice(r, sizeof(mld_poly)))
+    invariant(ctr <= MLDSA_N)
+    invariant(state.pos <= SHAKE256_RATE)
+    invariant(array_abs_bound(r->coeffs, 0, ctr, MLDSA_ETA + 1)))
+  {
+    mld_xof256_squeezeblocks(buf, 1, &state);
+    ctr = mld_rej_eta(r->coeffs, MLDSA_N, ctr, buf, buflen);
+  }
+
+  mld_xof256_release(&state);
+
+  mld_assert_abs_bound(r->coeffs, MLDSA_N, MLDSA_ETA + 1);
+
+  /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
+  mld_zeroize(buf, sizeof(buf));
+  mld_zeroize(extseed, sizeof(extseed));
+}
+#endif /* MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 
 #define POLY_UNIFORM_GAMMA1_NBLOCKS \

mldsa/sign.c

@@ -119,6 +119,20 @@ __contract__(
 )
 {
 /* Sample short vectors s1 and s2 */
+#if defined(MLD_CONFIG_SERIAL_FIPS202_ONLY)
+  int i;
+  uint16_t nonce = 0;
+  /* Safety: The nonces are at most 14 (MLDSA_L + MLDSA_K - 1), and, hence, the
+   * casts are safe. */
+  for (i = 0; i < MLDSA_L; i++)
+  {
+    mld_poly_uniform_eta(&s1->vec[i], seed, (uint8_t)(nonce + i));
+  }
+  for (i = 0; i < MLDSA_K; i++)
+  {
+    mld_poly_uniform_eta(&s2->vec[i], seed, (uint8_t)(nonce + MLDSA_L + i));
+  }
+#else /* MLD_CONFIG_SERIAL_FIPS202_ONLY */
 #if MLD_CONFIG_PARAMETER_SET == 44
   mld_poly_uniform_eta_4x(&s1->vec[0], &s1->vec[1], &s1->vec[2], &s1->vec[3],
                           seed, 0, 1, 2, 3);
@@ -143,6 +157,7 @@ __contract__(
   mld_poly_uniform_eta_4x(&s2->vec[4], &s2->vec[5], &s2->vec[6], &s2->vec[7],
                           seed, 11, 12, 13, 14);
 #endif /* MLD_CONFIG_PARAMETER_SET == 87 */
+#endif /* !MLD_CONFIG_SERIAL_FIPS202_ONLY */
 }
 
 MLD_MUST_CHECK_RETURN_VALUE

proofs/cbmc/poly_uniform_eta/Makefile

@@ -0,0 +1,61 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = poly_uniform_eta_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = poly_uniform_eta
+
+DEFINES += -DMLD_CONFIG_SERIAL_FIPS202_ONLY
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_eta
+USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_init
+USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256_absorb
+USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256_finalize
+USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256_squeeze
+USE_FUNCTION_CONTRACTS+=mld_rej_eta
+USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256_release 
+USE_FUNCTION_CONTRACTS+=mld_zeroize
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = poly_uniform_eta
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 9
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common

proofs/cbmc/poly_uniform_eta/poly_uniform_eta_harness.c

@@ -0,0 +1,13 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "poly.h"
+
+void harness(void)
+{
+  mld_poly *r0;
+  const uint8_t *seed;
+  uint8_t n0;
+
+  mld_poly_uniform_eta(r0, seed, n0);
+}

proofs/cbmc/sample_s1_s2_serial/Makefile

@@ -0,0 +1,56 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = sample_s1_s2_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = mld_sample_s1_s2_serial
+
+DEFINES += -DMLD_CONFIG_SERIAL_FIPS202_ONLY
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += mld_sample_s1_s2.0:7 # Largest value of MLDSA_L
+UNWINDSET += mld_sample_s1_s2.1:8 # Largest value of MLDSA_K
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c
+
+CHECK_FUNCTION_CONTRACTS=mld_sample_s1_s2
+USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_eta
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = mld_sample_s1_s2_serial
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 10
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common

proofs/cbmc/sample_s1_s2_serial/sample_s1_s2_harness.c

@@ -0,0 +1,16 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "sign.h"
+
+static void mld_sample_s1_s2(mld_polyvecl *s1, mld_polyveck *s2,
+                             const uint8_t seed[MLDSA_CRHBYTES]);
+
+void harness(void)
+{
+  mld_polyvecl *s1;
+  mld_polyveck *s2;
+  uint8_t *seed;
+
+  mld_sample_s1_s2(s1, s2, seed);
+}