Add support for PreHash ML-DSA

Makefile.Microsoft_nmake

@@ -5,19 +5,23 @@
 CFLAGS = /nologo /O2 /Imldsa /Imlmdsa/fips202 /Imldsa/fips202/native /Imldsa/native
 
 OBJ_FILES = .\mldsa\*.obj \
-            .\mldsa\fips202\*.obj
+            .\mldsa\fips202\*.obj \
+            .\mldsa\sha2\*.obj
 
 BUILD_DIR = test\build
 MLDSA44_BUILD_DIR = $(BUILD_DIR)\mldsa44
 MLDSA65_BUILD_DIR = $(BUILD_DIR)\mldsa65
 MLDSA87_BUILD_DIR = $(BUILD_DIR)\mldsa87
 
 OBJ_FILES_44 = $(MLDSA44_BUILD_DIR)\mldsa\*.obj \
-                $(MLDSA44_BUILD_DIR)\mldsa\fips202\*.obj
+                $(MLDSA44_BUILD_DIR)\mldsa\fips202\*.obj \
+                $(MLDSA44_BUILD_DIR)\mldsa\sha2\*.obj
 OBJ_FILES_65 = $(MLDSA65_BUILD_DIR)\mldsa\*.obj \
-                $(MLDSA65_BUILD_DIR)\mldsa\fips202\*.obj
+                $(MLDSA65_BUILD_DIR)\mldsa\fips202\*.obj \
+                $(MLDSA65_BUILD_DIR)\mldsa\sha2\*.obj
 OBJ_FILES_87 = $(MLDSA87_BUILD_DIR)\mldsa\*.obj \
-                 $(MLDSA87_BUILD_DIR)\mldsa\fips202\*.obj
+                 $(MLDSA87_BUILD_DIR)\mldsa\fips202\*.obj \
+                 $(MLDSA87_BUILD_DIR)\mldsa\sha2\*.obj
 
 # NOTE: We currently only build code for non-opt code, as we haven't yet made the assembly compatible on Windows
 !IFNDEF OPT
@@ -37,6 +41,10 @@ OPT = 0
     @if NOT EXIST $(MLDSA44_BUILD_DIR)\mldsa\fips202 mkdir $(MLDSA44_BUILD_DIR)\mldsa\fips202
     $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=44 /c /Fo$(MLDSA44_BUILD_DIR)\mldsa\fips202\ $<
 
+{mldsa\sha2}.c{$(MLDSA44_BUILD_DIR)\mldsa\sha2}.obj::
+    @if NOT EXIST $(MLDSA44_BUILD_DIR)\mldsa\sha2 mkdir $(MLDSA44_BUILD_DIR)\mldsa\sha2
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=44 /c /Fo$(MLDSA44_BUILD_DIR)\mldsa\sha2\ $<
+
 {test}.c{$(MLDSA44_BUILD_DIR)\test}.obj::
     @if NOT EXIST $(MLDSA44_BUILD_DIR)\test mkdir $(MLDSA44_BUILD_DIR)\test
     $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=44 /c /Fo$(MLDSA44_BUILD_DIR)\test\ $<
@@ -50,6 +58,10 @@ OPT = 0
     @if NOT EXIST $(MLDSA65_BUILD_DIR)\mldsa\fips202 mkdir $(MLDSA65_BUILD_DIR)\mldsa\fips202
     $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=65 /c /Fo$(MLDSA65_BUILD_DIR)\mldsa\fips202\ $<
 
+{mldsa\sha2}.c{$(MLDSA65_BUILD_DIR)\mldsa\sha2}.obj::
+    @if NOT EXIST $(MLDSA65_BUILD_DIR)\mldsa\sha2 mkdir $(MLDSA65_BUILD_DIR)\mldsa\sha2
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=65 /c /Fo$(MLDSA65_BUILD_DIR)\mldsa\sha2\ $<
+
 {test}.c{$(MLDSA65_BUILD_DIR)\test}.obj::
     @if NOT EXIST $(MLDSA65_BUILD_DIR)\test mkdir $(MLDSA65_BUILD_DIR)\test
     $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=65 /c /Fo$(MLDSA65_BUILD_DIR)\test\ $<
@@ -63,6 +75,10 @@ OPT = 0
     @if NOT EXIST $(MLDSA87_BUILD_DIR)\mldsa\fips202 mkdir $(MLDSA87_BUILD_DIR)\mldsa\fips202
     $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=87 /c /Fo$(MLDSA87_BUILD_DIR)\mldsa\fips202\ $<
 
+{mldsa\sha2}.c{$(MLDSA87_BUILD_DIR)\mldsa\sha2}.obj::
+    @if NOT EXIST $(MLDSA87_BUILD_DIR)\mldsa\sha2 mkdir $(MLDSA87_BUILD_DIR)\mldsa\sha2
+    $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=87 /c /Fo$(MLDSA87_BUILD_DIR)\mldsa\sha2\ $<
+
 {test}.c{$(MLDSA87_BUILD_DIR)\test}.obj::
     @if NOT EXIST $(MLDSA87_BUILD_DIR)\test mkdir $(MLDSA87_BUILD_DIR)\test
     $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=87 /c /Fo$(MLDSA87_BUILD_DIR)\test\ $<

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/sha2/sha2.h

@@ -0,0 +1,98 @@
+/*
+ * Copyright (c) The mldsa-native project authors
+ * Copyright (c) The slhdsa-c project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+
+#ifndef MLD_SHA2_SHA2_H
+#define MLD_SHA2_SHA2_H
+
+
+/* FIPS 180-4 (SHA-2) */
+
+#include <stddef.h>
+#include <stdint.h>
+#include "../cbmc.h"
+
+#define SHA2_224_HASHBYTES 28
+#define SHA2_256_HASHBYTES 32
+#define SHA2_384_HASHBYTES 48
+#define SHA2_512_HASHBYTES 64
+#define SHA2_512_224_HASHBYTES 28
+#define SHA2_512_256_HASHBYTES 32
+
+#define FIPS180_NAMESPACE(s) mldsa_fips180_ref_##s
+
+#define mld_sha2_224 FIPS180_NAMESPACE(sha2_224)
+/*************************************************
+ * Name:        mld_sha2_224
+ *
+ * Description: SHA2-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_sha2_224(uint8_t *out, const uint8_t *in, size_t inlen);
+
+#define mld_sha2_256 FIPS180_NAMESPACE(sha2_256)
+/*************************************************
+ * Name:        mld_sha2_256
+ *
+ * Description: SHA2-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_sha2_256(uint8_t *out, const uint8_t *in, size_t inlen);
+
+#define mld_sha2_384 FIPS180_NAMESPACE(sha2_384)
+/*************************************************
+ * Name:        mld_sha2_384
+ *
+ * Description: SHA2-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_sha2_384(uint8_t *out, const uint8_t *in, size_t inlen);
+
+#define mld_sha2_512 FIPS180_NAMESPACE(sha2_512)
+/*************************************************
+ * Name:        mld_sha2_512
+ *
+ * Description: SHA2-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_sha2_512(uint8_t *out, const uint8_t *in, size_t inlen);
+
+#define mld_sha2_512_224 FIPS180_NAMESPACE(sha2_512_224)
+/*************************************************
+ * Name:        mld_sha2_512_224
+ *
+ * Description: SHA2-512/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_sha2_512_224(uint8_t *out, const uint8_t *in, size_t inlen);
+
+#define mld_sha2_512_256 FIPS180_NAMESPACE(sha2_512_256)
+/*************************************************
+ * Name:        mld_sha2_512_256
+ *
+ * Description: SHA2-512/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_sha2_512_256(uint8_t *out, const uint8_t *in, size_t inlen);
+
+#endif /* !MLD_SHA2_SHA2_H */