PreHash ML-DSA: SHAKE128/SHA3-256/SHA3-384/SHA3-224/SHA3-512

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

Author: mkannwischer

mldsa/fips202/fips202.c

@@ -145,6 +145,9 @@ static unsigned int keccak_squeeze(uint8_t *out, size_t outlen,
 __contract__(
   requires((r == SHAKE128_RATE && pos <= SHAKE128_RATE) ||
            (r == SHAKE256_RATE && pos <= SHAKE256_RATE) ||
+           (r == SHA3_224_RATE && pos <= SHA3_224_RATE) ||
+           (r == SHA3_256_RATE && pos <= SHA3_256_RATE) ||
+           (r == SHA3_384_RATE && pos <= SHA3_384_RATE) ||
            (r == SHA3_512_RATE && pos <= SHA3_512_RATE))
   requires(outlen <= 8 * r /* somewhat arbitrary bound */)
   requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
@@ -245,6 +248,17 @@ void mld_shake256_release(mld_shake256ctx *state)
   mld_zeroize(state, sizeof(mld_shake256ctx));
 }
 
+void mld_shake128(uint8_t *out, size_t outlen, const uint8_t *in, size_t inlen)
+{
+  mld_shake128ctx state;
+
+  mld_shake128_init(&state);
+  mld_shake128_absorb(&state, in, inlen);
+  mld_shake128_finalize(&state);
+  mld_shake128_squeeze(out, outlen, &state);
+  mld_shake128_release(&state);
+}
+
 void mld_shake256(uint8_t *out, size_t outlen, const uint8_t *in, size_t inlen)
 {
   mld_shake256ctx state;
@@ -255,3 +269,47 @@ void mld_shake256(uint8_t *out, size_t outlen, const uint8_t *in, size_t inlen)
   mld_shake256_squeeze(out, outlen, &state);
   mld_shake256_release(&state);
 }
+
+void mld_sha3_256(uint8_t *out, const uint8_t *in, size_t inlen)
+{
+  uint64_t s[MLD_KECCAK_LANES];
+
+  keccak_init(s);
+  keccak_absorb(s, 0, SHA3_256_RATE, in, inlen);
+  keccak_finalize(s, inlen % SHA3_256_RATE, SHA3_256_RATE, 0x06);
+  keccak_squeeze(out, SHA3_256_HASHBYTES, s, SHA3_256_RATE, SHA3_256_RATE);
+  mld_zeroize(s, sizeof(s));
+}
+
+void mld_sha3_384(uint8_t *out, const uint8_t *in, size_t inlen)
+{
+  uint64_t s[MLD_KECCAK_LANES];
+
+  keccak_init(s);
+  keccak_absorb(s, 0, SHA3_384_RATE, in, inlen);
+  keccak_finalize(s, inlen % SHA3_384_RATE, SHA3_384_RATE, 0x06);
+  keccak_squeeze(out, SHA3_384_HASHBYTES, s, SHA3_384_RATE, SHA3_384_RATE);
+  mld_zeroize(s, sizeof(s));
+}
+
+void mld_sha3_224(uint8_t *out, const uint8_t *in, size_t inlen)
+{
+  uint64_t s[MLD_KECCAK_LANES];
+
+  keccak_init(s);
+  keccak_absorb(s, 0, SHA3_224_RATE, in, inlen);
+  keccak_finalize(s, inlen % SHA3_224_RATE, SHA3_224_RATE, 0x06);
+  keccak_squeeze(out, SHA3_224_HASHBYTES, s, SHA3_224_RATE, SHA3_224_RATE);
+  mld_zeroize(s, sizeof(s));
+}
+
+void mld_sha3_512(uint8_t *out, const uint8_t *in, size_t inlen)
+{
+  uint64_t s[MLD_KECCAK_LANES];
+
+  keccak_init(s);
+  keccak_absorb(s, 0, SHA3_512_RATE, in, inlen);
+  keccak_finalize(s, inlen % SHA3_512_RATE, SHA3_512_RATE, 0x06);
+  keccak_squeeze(out, SHA3_512_HASHBYTES, s, SHA3_512_RATE, SHA3_512_RATE);
+  mld_zeroize(s, sizeof(s));
+}

mldsa/fips202/fips202.h

@@ -11,10 +11,14 @@
 
 #define SHAKE128_RATE 168
 #define SHAKE256_RATE 136
+#define SHA3_224_RATE 144
 #define SHA3_256_RATE 136
+#define SHA3_384_RATE 104
 #define SHA3_512_RATE 72
 #define MLD_KECCAK_LANES 25
+#define SHA3_224_HASHBYTES 28
 #define SHA3_256_HASHBYTES 32
+#define SHA3_384_HASHBYTES 48
 #define SHA3_512_HASHBYTES 64
 
 #define FIPS202_NAMESPACE(s) mldsa_fips202_ref_##s
@@ -121,6 +125,26 @@ __contract__(
   assigns(memory_slice(state, sizeof(mld_shake128ctx)))
 );
 
+#define mld_shake128 FIPS202_NAMESPACE(shake128)
+/*************************************************
+ * Name:        mld_shake128
+ *
+ * Description: SHAKE128 XOF with non-incremental API
+ *
+ * Arguments:   - uint8_t *out: pointer to output
+ *              - size_t outlen: requested output length in bytes
+ *              - const uint8_t *in: pointer to input
+ *              - size_t inlen: length of input in bytes
+ **************************************************/
+void mld_shake128(uint8_t *out, size_t outlen, const uint8_t *in, size_t inlen)
+__contract__(
+  requires(inlen <= MLD_MAX_BUFFER_SIZE)
+  requires(outlen <= 8 * SHAKE128_RATE /* somewhat arbitrary bound */)
+  requires(memory_no_alias(in, inlen))
+  requires(memory_no_alias(out, outlen))
+  assigns(memory_slice(out, outlen))
+);
+
 #define mld_shake256_init FIPS202_NAMESPACE(shake256_init)
 /*************************************************
  * Name:        mld_shake256_init
@@ -231,4 +255,76 @@ __contract__(
   assigns(memory_slice(out, outlen))
 );
 
+#define mld_sha3_256 FIPS202_NAMESPACE(sha3_256)
+/*************************************************
+ * Name:        mld_sha3_256
+ *
+ * Description: SHA3-256 hash function
+ *
+ * Arguments:   - uint8_t *out: pointer to output (32 bytes)
+ *              - const uint8_t *in: pointer to input
+ *              - size_t inlen: length of input in bytes
+ **************************************************/
+void mld_sha3_256(uint8_t *out, const uint8_t *in, size_t inlen)
+__contract__(
+  requires(inlen <= MLD_MAX_BUFFER_SIZE)
+  requires(memory_no_alias(in, inlen))
+  requires(memory_no_alias(out, SHA3_256_HASHBYTES))
+  assigns(memory_slice(out, SHA3_256_HASHBYTES))
+);
+
+#define mld_sha3_384 FIPS202_NAMESPACE(sha3_384)
+/*************************************************
+ * Name:        mld_sha3_384
+ *
+ * Description: SHA3-384 hash function
+ *
+ * Arguments:   - uint8_t *out: pointer to output (48 bytes)
+ *              - const uint8_t *in: pointer to input
+ *              - size_t inlen: length of input in bytes
+ **************************************************/
+void mld_sha3_384(uint8_t *out, const uint8_t *in, size_t inlen)
+__contract__(
+  requires(inlen <= MLD_MAX_BUFFER_SIZE)
+  requires(memory_no_alias(in, inlen))
+  requires(memory_no_alias(out, SHA3_384_HASHBYTES))
+  assigns(memory_slice(out, SHA3_384_HASHBYTES))
+);
+
+#define mld_sha3_224 FIPS202_NAMESPACE(sha3_224)
+/*************************************************
+ * Name:        mld_sha3_224
+ *
+ * Description: SHA3-224 hash function
+ *
+ * Arguments:   - uint8_t *out: pointer to output (28 bytes)
+ *              - const uint8_t *in: pointer to input
+ *              - size_t inlen: length of input in bytes
+ **************************************************/
+void mld_sha3_224(uint8_t *out, const uint8_t *in, size_t inlen)
+__contract__(
+  requires(inlen <= MLD_MAX_BUFFER_SIZE)
+  requires(memory_no_alias(in, inlen))
+  requires(memory_no_alias(out, SHA3_224_HASHBYTES))
+  assigns(memory_slice(out, SHA3_224_HASHBYTES))
+);
+
+#define mld_sha3_512 FIPS202_NAMESPACE(sha3_512)
+/*************************************************
+ * Name:        mld_sha3_512
+ *
+ * Description: SHA3-512 hash function
+ *
+ * Arguments:   - uint8_t *out: pointer to output (64 bytes)
+ *              - const uint8_t *in: pointer to input
+ *              - size_t inlen: length of input in bytes
+ **************************************************/
+void mld_sha3_512(uint8_t *out, const uint8_t *in, size_t inlen)
+__contract__(
+  requires(inlen <= MLD_MAX_BUFFER_SIZE)
+  requires(memory_no_alias(in, inlen))
+  requires(memory_no_alias(out, SHA3_512_HASHBYTES))
+  assigns(memory_slice(out, SHA3_512_HASHBYTES))
+);
+
 #endif /* !MLD_FIPS202_FIPS202_H */

mldsa/sign.c

@@ -877,15 +877,24 @@ int crypto_sign_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen,
  *              - mld_hash_alg_t hashAlg: hash algorithm enumeration
  *
  * Returns 0 if hash algorithm is supported and -1 otherwise.
- * Currently only SHAKE-256 is supported.
+ * Currently SHAKE-128 and SHAKE-256 are supported.
  **************************************************/
 static int prehash_message(uint8_t *out, size_t *oid_ph_len, const uint8_t *m,
                            size_t mlen, mld_hash_alg_t hashAlg)
 {
-  /* OIDs for supported hash functions - currently only SHAKE-256 is implemented
-   */
+  /* OIDs for supported hash functions */
+  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};
+  const uint8_t sha3_256_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                    0x65, 0x03, 0x04, 0x02, 0x08};
+  const uint8_t sha3_224_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
+                                    0x65, 0x03, 0x04, 0x02, 0x07};
+  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};
 
   /* OIDs for hash functions to be added:
   const uint8_t sha2_224_oid[11] = {0x06, 0x09, 0x60, 0x86, 0x48, 0x01,
@@ -900,38 +909,53 @@ static int prehash_message(uint8_t *out, size_t *oid_ph_len, const uint8_t *m,
                                         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};
   */
 
   switch (hashAlg)
   {
+    case MLD_SHAKE_128:
+      mld_memcpy(out, shake_128_oid, 11);
+      mld_shake128(out + 11, 32, m, mlen);
+      *oid_ph_len = 11 + 32;
+      return 0;
+
     case MLD_SHAKE_256:
       mld_memcpy(out, shake_256_oid, 11);
       mld_shake256(out + 11, 64, m, mlen);
       *oid_ph_len = 11 + 64;
       return 0;
 
+    case MLD_SHA3_256:
+      mld_memcpy(out, sha3_256_oid, 11);
+      mld_sha3_256(out + 11, m, mlen);
+      *oid_ph_len = 11 + 32;
+      return 0;
+
+    case MLD_SHA3_224:
+      mld_memcpy(out, sha3_224_oid, 11);
+      mld_sha3_224(out + 11, m, mlen);
+      *oid_ph_len = 11 + 28;
+      return 0;
+
+    case MLD_SHA3_384:
+      mld_memcpy(out, sha3_384_oid, 11);
+      mld_sha3_384(out + 11, m, mlen);
+      *oid_ph_len = 11 + 48;
+      return 0;
+
+    case MLD_SHA3_512:
+      mld_memcpy(out, sha3_512_oid, 11);
+      mld_sha3_512(out + 11, m, mlen);
+      *oid_ph_len = 11 + 64;
+      return 0;
+
     /* Other hash algorithms not yet supported */
     case MLD_SHA2_224:
     case MLD_SHA2_256:
     case MLD_SHA2_384:
     case MLD_SHA2_512:
     case MLD_SHA2_512_224:
     case MLD_SHA2_512_256:
-    case MLD_SHA3_224:
-    case MLD_SHA3_256:
-    case MLD_SHA3_384:
-    case MLD_SHA3_512:
-    case MLD_SHAKE_128:
     default:
       return -1;
   }

proofs/cbmc/sha3_224/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 = sha3_224_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 = sha3_224
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/fips202/fips202.c
+
+CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)sha3_224
+USE_FUNCTION_CONTRACTS=keccak_init keccak_absorb keccak_finalize keccak_squeeze
+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 = sha3_224
+
+# 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/sha3_224/sha3_224_harness.c

@@ -0,0 +1,22 @@
+/*
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+
+/*
+ * Proof for mld_sha3_224()
+ */
+
+#include <assert.h>
+#include <stdint.h>
+
+#include "fips202.h"
+
+void harness(void)
+{
+  uint8_t in[65536];
+  uint8_t out[28];
+  size_t inlen;
+
+  mld_sha3_224(out, in, inlen);
+}