Merge pull request #293 from pq-code-package/refactor_sign_hashing

Refactor and simplify repeated hashing code in sign.c

Author: mkannwischer

mldsa/sign.c

@@ -91,6 +91,55 @@ int crypto_sign_keypair(uint8_t *pk, uint8_t *sk)
   return crypto_sign_keypair_internal(pk, sk, seed);
 }
 
+/*************************************************
+ * Name:        mld_H
+ *
+ * Description: Abstracts application of SHAKE256 to
+ *              one, two or three blocks of data,
+ *              yielding a user-requested size of
+ *              output.
+ *
+ * Arguments:   - uint8_t *out: pointer to output
+ *              - size_t outlen: requested output length in bytes
+ *              - const uint8_t *in1: pointer to input block 1
+ *                                    Must NOT be NULL
+ *              - size_t in1len: length of input in1 bytes
+ *              - const uint8_t *in2: pointer to input block 2
+ *                                    May be NULL, in which case
+ *                                    this block is ignored
+ *              - size_t in2len: length of input in2 bytes
+ *              - const uint8_t *in3: pointer to input block 3
+ *                                    May be NULL, in which case
+ *                                    this block is ignored
+ *              - size_t in3len: length of input in3 bytes
+ **************************************************/
+static void mld_H(uint8_t *out, size_t outlen, const uint8_t *in1,
+                  size_t in1len, const uint8_t *in2, size_t in2len,
+                  const uint8_t *in3, size_t in3len)
+__contract__(
+  requires(outlen <= 8 * SHAKE256_RATE /* somewhat arbitrary bound */)
+  requires(memory_no_alias(in1, in1len))
+  requires(in2 == NULL || memory_no_alias(in2, in2len))
+  requires(in3 == NULL || memory_no_alias(in3, in3len))
+  requires(memory_no_alias(out, outlen))
+  assigns(memory_slice(out, outlen))
+)
+{
+  keccak_state state;
+  shake256_init(&state);
+  shake256_absorb(&state, in1, in1len);
+  if (in2 != NULL)
+  {
+    shake256_absorb(&state, in2, in2len);
+  }
+  if (in3 != NULL)
+  {
+    shake256_absorb(&state, in3, in3len);
+  }
+  shake256_finalize(&state);
+  shake256_squeeze(out, outlen, &state);
+}
+
 int crypto_sign_signature_internal(uint8_t *sig, size_t *siglen,
                                    const uint8_t *m, size_t mlen,
                                    const uint8_t *pre, size_t prelen,
@@ -104,7 +153,6 @@ int crypto_sign_signature_internal(uint8_t *sig, size_t *siglen,
   polyvecl mat[MLDSA_K], s1, y, z;
   polyveck t0, s2, w1, w0, h;
   poly cp;
-  keccak_state state;
 
   rho = seedbuf;
   tr = rho + MLDSA_SEEDBYTES;
@@ -116,12 +164,7 @@ int crypto_sign_signature_internal(uint8_t *sig, size_t *siglen,
   if (!externalmu)
   {
     /* Compute mu = CRH(tr, pre, msg) */
-    shake256_init(&state);
-    shake256_absorb(&state, tr, MLDSA_TRBYTES);
-    shake256_absorb(&state, pre, prelen);
-    shake256_absorb(&state, m, mlen);
-    shake256_finalize(&state);
-    shake256_squeeze(mu, MLDSA_CRHBYTES, &state);
+    mld_H(mu, MLDSA_CRHBYTES, tr, MLDSA_TRBYTES, pre, prelen, m, mlen);
   }
   else
   {
@@ -130,12 +173,8 @@ int crypto_sign_signature_internal(uint8_t *sig, size_t *siglen,
   }
 
   /* Compute rhoprime = CRH(key, rnd, mu) */
-  shake256_init(&state);
-  shake256_absorb(&state, key, MLDSA_SEEDBYTES);
-  shake256_absorb(&state, rnd, MLDSA_RNDBYTES);
-  shake256_absorb(&state, mu, MLDSA_CRHBYTES);
-  shake256_finalize(&state);
-  shake256_squeeze(rhoprime, MLDSA_CRHBYTES, &state);
+  mld_H(rhoprime, MLDSA_CRHBYTES, key, MLDSA_SEEDBYTES, rnd, MLDSA_RNDBYTES, mu,
+        MLDSA_CRHBYTES);
 
   /* Expand matrix and transform vectors */
   polyvec_matrix_expand(mat, rho);
@@ -150,7 +189,7 @@ int crypto_sign_signature_internal(uint8_t *sig, size_t *siglen,
   /* place loop invariants for CBMC.                          */
   while (1)
   __loop__(
-    invariant(true); /* TODO */
+    invariant(1) /* TODO */
   )
   {
     /* Sample intermediate vector y */
@@ -168,11 +207,8 @@ int crypto_sign_signature_internal(uint8_t *sig, size_t *siglen,
     polyveck_decompose(&w1, &w0, &w1);
     polyveck_pack_w1(sig, &w1);
 
-    shake256_init(&state);
-    shake256_absorb(&state, mu, MLDSA_CRHBYTES);
-    shake256_absorb(&state, sig, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES);
-    shake256_finalize(&state);
-    shake256_squeeze(sig, MLDSA_CTILDEBYTES, &state);
+    mld_H(sig, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, sig,
+          MLDSA_K * MLDSA_POLYW1_PACKEDBYTES, NULL, 0);
     poly_challenge(&cp, sig);
     poly_ntt(&cp);
 
@@ -309,7 +345,6 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
   poly cp;
   polyvecl mat[MLDSA_K], z;
   polyveck t1, w1, h;
-  keccak_state state;
 
   if (siglen != CRYPTO_BYTES)
   {
@@ -329,13 +364,8 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
   if (!externalmu)
   {
     /* Compute CRH(H(rho, t1), pre, msg) */
-    shake256(mu, MLDSA_TRBYTES, pk, CRYPTO_PUBLICKEYBYTES);
-    shake256_init(&state);
-    shake256_absorb(&state, mu, MLDSA_TRBYTES);
-    shake256_absorb(&state, pre, prelen);
-    shake256_absorb(&state, m, mlen);
-    shake256_finalize(&state);
-    shake256_squeeze(mu, MLDSA_CRHBYTES, &state);
+    mld_H(mu, MLDSA_TRBYTES, pk, CRYPTO_PUBLICKEYBYTES, NULL, 0, NULL, 0);
+    mld_H(mu, MLDSA_CRHBYTES, mu, MLDSA_TRBYTES, pre, prelen, m, mlen);
   }
   else
   {
@@ -365,11 +395,8 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
   polyveck_pack_w1(buf, &w1);
 
   /* Call random oracle and verify challenge */
-  shake256_init(&state);
-  shake256_absorb(&state, mu, MLDSA_CRHBYTES);
-  shake256_absorb(&state, buf, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES);
-  shake256_finalize(&state);
-  shake256_squeeze(c2, MLDSA_CTILDEBYTES, &state);
+  mld_H(c2, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, buf,
+        MLDSA_K * MLDSA_POLYW1_PACKEDBYTES, NULL, 0);
   for (i = 0; i < MLDSA_CTILDEBYTES; ++i)
   {
     if (c[i] != c2[i])

proofs/cbmc/mld_h/Makefile

@@ -0,0 +1,55 @@
+# 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 = mld_h_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_h
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c
+
+CHECK_FUNCTION_CONTRACTS=mld_H
+USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_init $(FIPS202_NAMESPACE)shake256_absorb $(FIPS202_NAMESPACE)shake256_squeeze $(FIPS202_NAMESPACE)shake256_finalize
+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_h
+
+# 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 = 8
+
+# 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/mld_h/mld_h_harness.c

@@ -0,0 +1,22 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "sign.h"
+
+void mld_H(uint8_t *out, size_t outlen, const uint8_t *in1, size_t in1len,
+           const uint8_t *in2, size_t in2len, const uint8_t *in3,
+           size_t in3len);
+
+void harness(void)
+{
+  uint8_t *out;
+  size_t outlen;
+  const uint8_t *in1;
+  size_t in1len;
+  const uint8_t *in2;
+  size_t in2len;
+  const uint8_t *in3;
+  size_t in3len;
+
+  mld_H(out, outlen, in1, in1len, in2, in2len, in3, in3len);
+}