Add support for PreHash ML-DSA

This commit adds two functions crypto_sign_signature_pre_hash
and crypto_sign_verify_pre_hash implementing the pre-hashing mode of ML-DSA.
Instead of receiving a message, they receive a pre-hashed message.
Details can be found in Algorithm 4 and 5 in FIPS204.

The message to signed is formatted as
0x01 || ctxlen (1 byte) || ctx || oid || ph
where ph is the pre-hash and oid is the object identifier of the used hash
algorithm.

The ACVP client is adjusted to support the pre-hashing test cases. Note that
the ACVP testvectors only contain the message, not the pre-hash. I opted for
computing the hash in the ACVP Python client as for that we do not have to
add implementations for the 12 hash functions.

CBMC proofs for the new functions are added.

Resolves #39

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

Author: mkannwischer

mldsa/sign.c

@@ -835,3 +835,197 @@ int crypto_sign_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen,
 
   return -1;
 }
+
+/*************************************************
+ * Name:        sha_oid
+ *
+ * Description: Writes the OID of a given SHA-2/SHA-3 hash function
+ *              to oid and checks that the given hash length matches
+ *              the given hash function.
+ *
+ * Arguments:   - uint8_t oid[11]: pointer to output oid
+ *              - mld_hash_alg_t hashAlg: hash algorithm enumeration
+ *              - size_t len: Hash length to be checked
+ *
+ * Returns 0 if hash algorithm is known and the hash length matches
+ * and -1 otherwise.
+ **************************************************/
+static int sha_oid(uint8_t oid[11], mld_hash_alg_t hashAlg, size_t len)
+{
+  const uint8_t sha2_224_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                    0x65, 0x03, 0x04, 0x02, 0x04};
+  const uint8_t sha2_256_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                    0x65, 0x03, 0x04, 0x02, 0x01};
+  const uint8_t sha2_384_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                    0x65, 0x03, 0x04, 0x02, 0x02};
+  const uint8_t sha2_512_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                    0x65, 0x03, 0x04, 0x02, 0x03};
+  const uint8_t sha2_512_224_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                        0x65, 0x03, 0x04, 0x02, 0x05};
+  const uint8_t sha2_512_256_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                        0x65, 0x03, 0x04, 0x02, 0x06};
+  const uint8_t sha3_224_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                    0x65, 0x03, 0x04, 0x02, 0x07};
+  const uint8_t sha3_256_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                    0x65, 0x03, 0x04, 0x02, 0x08};
+  const uint8_t sha3_384_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                    0x65, 0x03, 0x04, 0x02, 0x09};
+  const uint8_t sha3_512_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                    0x65, 0x03, 0x04, 0x02, 0x0A};
+  const uint8_t shake_128_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                     0x65, 0x03, 0x04, 0x02, 0x0B};
+  const uint8_t shake_256_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                     0x65, 0x03, 0x04, 0x02, 0x0C};
+
+  switch (hashAlg)
+  {
+    case MLD_SHA2_224:
+      if (len == 28)
+      {
+        mld_memcpy(oid, sha2_224_oid, 11);
+        return 0;
+      }
+      break;
+    case MLD_SHA2_256:
+      if (len == 32)
+      {
+        mld_memcpy(oid, sha2_256_oid, 11);
+        return 0;
+      }
+      break;
+    case MLD_SHA2_384:
+      if (len == 48)
+      {
+        mld_memcpy(oid, sha2_384_oid, 11);
+        return 0;
+      }
+      break;
+    case MLD_SHA2_512:
+      if (len == 64)
+      {
+        mld_memcpy(oid, sha2_512_oid, 11);
+        return 0;
+      }
+      break;
+    case MLD_SHA2_512_224:
+      if (len == 28)
+      {
+        mld_memcpy(oid, sha2_512_224_oid, 11);
+        return 0;
+      }
+      break;
+    case MLD_SHA2_512_256:
+      if (len == 32)
+      {
+        mld_memcpy(oid, sha2_512_256_oid, 11);
+        return 0;
+      }
+      break;
+    case MLD_SHA3_224:
+      if (len == 28)
+      {
+        mld_memcpy(oid, sha3_224_oid, 11);
+        return 0;
+      }
+      break;
+    case MLD_SHA3_256:
+      if (len == 32)
+      {
+        mld_memcpy(oid, sha3_256_oid, 11);
+        return 0;
+      }
+      break;
+    case MLD_SHA3_384:
+      if (len == 48)
+      {
+        mld_memcpy(oid, sha3_384_oid, 11);
+        return 0;
+      }
+      break;
+    case MLD_SHA3_512:
+      if (len == 64)
+      {
+        mld_memcpy(oid, sha3_512_oid, 11);
+        return 0;
+      }
+      break;
+    case MLD_SHAKE_128:
+      if (len == 32)
+      {
+        mld_memcpy(oid, shake_128_oid, 11);
+        return 0;
+      }
+      break;
+    case MLD_SHAKE_256:
+      if (len == 64)
+      {
+        mld_memcpy(oid, shake_256_oid, 11);
+        return 0;
+      }
+      break;
+  }
+  return -1;
+}
+
+MLD_MUST_CHECK_RETURN_VALUE
+MLD_EXTERNAL_API
+int crypto_sign_signature_pre_hash(uint8_t *sig, size_t *siglen,
+                                   const uint8_t *ph, size_t phlen,
+                                   const uint8_t *ctx, size_t ctxlen,
+                                   const uint8_t rnd[MLDSA_RNDBYTES],
+                                   const uint8_t *sk, mld_hash_alg_t hashAlg)
+{
+  /* formatted message: 0x01 || ctxlen (1 byte) || ctx || oid || ph */
+  uint8_t fmsg[2 + 255 + 11 + 64];
+
+  if (ctxlen > 255)
+  {
+    *siglen = 0;
+    return -1;
+  }
+  fmsg[0] = 1;
+  fmsg[1] = ctxlen;
+  if (ctx != NULL && ctxlen != 0)
+  {
+    mld_memcpy(fmsg + 2, ctx, ctxlen);
+  }
+  if (sha_oid(fmsg + 2 + ctxlen, hashAlg, phlen))
+  {
+    *siglen = 0;
+    return -1;
+  }
+  mld_memcpy(fmsg + 2 + ctxlen + 11, ph, phlen);
+
+  return crypto_sign_signature_internal(sig, siglen, fmsg,
+                                        2 + ctxlen + 11 + phlen, rnd, sk, 0);
+}
+
+MLD_MUST_CHECK_RETURN_VALUE
+MLD_EXTERNAL_API
+int crypto_sign_verify_pre_hash(const uint8_t *sig, size_t siglen,
+                                const uint8_t *ph, size_t phlen,
+                                const uint8_t *ctx, size_t ctxlen,
+                                const uint8_t *pk, mld_hash_alg_t hashAlg)
+{
+  /* formatted message: 0x01 || ctxlen (1 byte) || ctx || oid || ph */
+  uint8_t fmsg[2 + 255 + 11 + 64];
+
+  if (ctxlen > 255)
+  {
+    return -1;
+  }
+  fmsg[0] = 1;
+  fmsg[1] = ctxlen;
+  if (ctx != NULL && ctxlen != 0)
+  {
+    mld_memcpy(fmsg + 2, ctx, ctxlen);
+  }
+  if (sha_oid(fmsg + 2 + ctxlen, hashAlg, phlen))
+  {
+    return -1;
+  }
+  mld_memcpy(fmsg + 2 + ctxlen + 11, ph, phlen);
+
+  return crypto_sign_verify_internal(sig, siglen, fmsg, 2 + ctxlen + 11 + phlen,
+                                     pk, 0);
+}

mldsa/sign.h

@@ -13,6 +13,25 @@
 #include "polyvec.h"
 #include "sys.h"
 
+/*************************************************
+ * Hash algorithm enumeration for pre-hash functions
+ **************************************************/
+typedef enum
+{
+  MLD_SHA2_224,
+  MLD_SHA2_256,
+  MLD_SHA2_384,
+  MLD_SHA2_512,
+  MLD_SHA2_512_224,
+  MLD_SHA2_512_256,
+  MLD_SHA3_224,
+  MLD_SHA3_256,
+  MLD_SHA3_384,
+  MLD_SHA3_512,
+  MLD_SHAKE_128,
+  MLD_SHAKE_256
+} mld_hash_alg_t;
+
 #define crypto_sign_keypair_internal MLD_NAMESPACE(keypair_internal)
 /*************************************************
  * Name:        crypto_sign_keypair_internal
@@ -346,4 +365,94 @@ __contract__(
   ensures(return_value == 0 || return_value == -1)
 );
 
+
+#define crypto_sign_signature_pre_hash MLD_NAMESPACE(signature_pre_hash)
+/*************************************************
+ * Name:        crypto_sign_signature_pre_hash
+ *
+ * Description: FIPS 204: Algorithm 4 HashML-DSA.Sign.
+ *              Computes signature with pre-hashed message.
+ *
+ * Arguments:   - uint8_t *sig: pointer to output signature (of length
+ *                              CRYPTO_BYTES)
+ *              - size_t *siglen: pointer to output length of signature
+ *              - const uint8_t *ph: pointer to pre-hashed message
+ *              - size_t phlen: length of pre-hashed message
+ *              - const uint8_t *ctx: pointer to context string
+ *              - size_t ctxlen: length of context string
+ *              - const uint8_t *rnd: pointer to random seed
+ *              - const uint8_t *sk: pointer to bit-packed secret key
+ *              - mld_hash_alg_t hashAlg: hash algorithm enumeration
+ *
+ * The supported hash functions are: "SHA2-224", "SHA2-256", "SHA2-384",
+ *                                   "SHA2-512", "SHA2-512/224", "SHA2-512/256",
+ *                                   "SHA3-224", "SHA3-256", "SHA3-384",
+ *                                   "SHA3-512", "SHAKE-128", "SHAKE-256"
+ *
+ * Returns 0 (success) or -1 (context string too long OR nonce exhaustion)
+ **************************************************/
+MLD_MUST_CHECK_RETURN_VALUE
+MLD_EXTERNAL_API
+int crypto_sign_signature_pre_hash(uint8_t *sig, size_t *siglen,
+                                   const uint8_t *ph, size_t phlen,
+                                   const uint8_t *ctx, size_t ctxlen,
+                                   const uint8_t rnd[MLDSA_RNDBYTES],
+                                   const uint8_t *sk, mld_hash_alg_t hashAlg)
+__contract__(
+  requires(phlen <= 64)
+  requires(ctxlen <= MLD_MAX_BUFFER_SIZE)
+  requires(memory_no_alias(sig, CRYPTO_BYTES))
+  requires(memory_no_alias(siglen, sizeof(size_t)))
+  requires(memory_no_alias(ph, phlen))
+  requires((ctx == NULL && ctxlen == 0) || memory_no_alias(ctx, ctxlen))
+  requires(memory_no_alias(rnd, MLDSA_RNDBYTES))
+  requires(memory_no_alias(sk, CRYPTO_SECRETKEYBYTES))
+  requires(hashAlg >= MLD_SHA2_224 && hashAlg <= MLD_SHAKE_256)
+  assigns(memory_slice(sig, CRYPTO_BYTES))
+  assigns(object_whole(siglen))
+  ensures((return_value == 0 && *siglen == CRYPTO_BYTES) ||
+          (return_value == -1 && *siglen == 0))
+);
+
+#define crypto_sign_verify_pre_hash MLD_NAMESPACE(verify_pre_hash)
+/*************************************************
+ * Name:        crypto_sign_verify_pre_hash
+ *
+ * Description: FIPS 204: Algorithm 5 HashML-DSA.Verify.
+ *              Verifies signature with pre-hashed message.
+ *
+ * Arguments:   - const uint8_t *sig: pointer to input signature
+ *              - size_t siglen: length of signature
+ *              - const uint8_t *ph: pointer to pre-hashed message
+ *              - size_t phlen: length of pre-hashed message
+ *              - const uint8_t *ctx: pointer to context string
+ *              - size_t ctxlen: length of context string
+ *              - const uint8_t *pk: pointer to bit-packed public key
+ *              - mld_hash_alg_t hashAlg: hash algorithm enumeration
+ *
+ * The supported hash functions are: "SHA2-224", "SHA2-256", "SHA2-384",
+ *                                   "SHA2-512", "SHA2-512/224", "SHA2-512/256",
+ *                                   "SHA3-224", "SHA3-256", "SHA3-384",
+ *                                   "SHA3-512", "SHAKE-128", "SHAKE-256"
+ *
+ * Returns 0 if signature could be verified correctly and -1 otherwise
+ **************************************************/
+MLD_MUST_CHECK_RETURN_VALUE
+MLD_EXTERNAL_API
+int crypto_sign_verify_pre_hash(const uint8_t *sig, size_t siglen,
+                                const uint8_t *ph, size_t phlen,
+                                const uint8_t *ctx, size_t ctxlen,
+                                const uint8_t *pk, mld_hash_alg_t hashAlg)
+__contract__(
+  requires(phlen <= 64)
+  requires(ctxlen <= MLD_MAX_BUFFER_SIZE - 77)
+  requires(siglen <= MLD_MAX_BUFFER_SIZE)
+  requires(memory_no_alias(sig, siglen))
+  requires(memory_no_alias(ph, phlen))
+  requires((ctx == NULL && ctxlen == 0) || memory_no_alias(ctx, ctxlen))
+  requires(memory_no_alias(pk, CRYPTO_PUBLICKEYBYTES))
+  requires(hashAlg >= MLD_SHA2_224 && hashAlg <= MLD_SHAKE_256)
+  ensures(return_value == 0 || return_value == -1)
+);
+
 #endif /* !MLD_SIGN_H */

proofs/cbmc/crypto_sign_signature_pre_hash/Makefile

@@ -0,0 +1,58 @@
+# 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 = crypto_sign_signature_pre_hash_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 = crypto_sign_signature_pre_hash
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature_pre_hash
+USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature_internal
+
+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
+CBMCFLAGS += --slice-formula
+CBMCFLAGS += --no-array-field-sensitivity
+
+FUNCTION_NAME = crypto_sign_signature_pre_hash
+
+# 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/crypto_sign_signature_pre_hash/crypto_sign_signature_pre_hash_harness.c

@@ -0,0 +1,20 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "sign.h"
+
+void harness(void)
+{
+  uint8_t *sig;
+  size_t *siglen;
+  const uint8_t *ph;
+  size_t phlen;
+  const uint8_t *ctx;
+  size_t ctxlen;
+  const uint8_t *rnd;
+  const uint8_t *sk;
+  mld_hash_alg_t hashAlg;
+  int r;
+  r = crypto_sign_signature_pre_hash(sig, siglen, ph, phlen, ctx, ctxlen, rnd,
+                                     sk, hashAlg);
+}