Skip to content

Commit fb50bdd

Browse files
mkannwischermkannwischer
committed
HashML-DSA: Add specialized shake256 pre-hashing function
Signed-off-by: Matthias J. Kannwischer <[email protected]>
1 parent 4e0b5ed commit fb50bdd

File tree

8 files changed

+464
-21
lines changed

8 files changed

+464
-21
lines changed

‎mldsa/sign.c‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1058,3 +1058,30 @@ int crypto_sign_verify_pre_hash_internal(const uint8_t *sig, size_t siglen,
10581058
return crypto_sign_verify_internal(sig, siglen, fmsg, 2 + ctxlen + 11 + phlen,
10591059
NULL, 0, pk, 0);
10601060
}
1061+
1062+
MLD_MUST_CHECK_RETURN_VALUE
1063+
MLD_EXTERNAL_API
1064+
int crypto_sign_signature_pre_hash_shake256(uint8_t *sig, size_t *siglen,
1065+
const uint8_t *m, size_t mlen,
1066+
const uint8_t *ctx, size_t ctxlen,
1067+
const uint8_t rnd[MLDSA_RNDBYTES],
1068+
const uint8_t *sk)
1069+
{
1070+
MLD_ALIGN uint8_t ph[64];
1071+
mld_shake256(ph, sizeof(ph), m, mlen);
1072+
return crypto_sign_signature_pre_hash_internal(
1073+
sig, siglen, ph, sizeof(ph), ctx, ctxlen, rnd, sk, MLD_SHAKE_256);
1074+
}
1075+
1076+
MLD_MUST_CHECK_RETURN_VALUE
1077+
MLD_EXTERNAL_API
1078+
int crypto_sign_verify_pre_hash_shake256(const uint8_t *sig, size_t siglen,
1079+
const uint8_t *m, size_t mlen,
1080+
const uint8_t *ctx, size_t ctxlen,
1081+
const uint8_t *pk)
1082+
{
1083+
MLD_ALIGN uint8_t ph[64];
1084+
mld_shake256(ph, sizeof(ph), m, mlen);
1085+
return crypto_sign_verify_pre_hash_internal(sig, siglen, ph, sizeof(ph), ctx,
1086+
ctxlen, pk, MLD_SHAKE_256);
1087+
}

‎mldsa/sign.h‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,10 @@
3737
MLD_NAMESPACE_KL(signature_pre_hash_internal)
3838
#define crypto_sign_verify_pre_hash_internal \
3939
MLD_NAMESPACE_KL(verify_pre_hash_internal)
40+
#define crypto_sign_signature_pre_hash_shake256 \
41+
MLD_NAMESPACE_KL(signature_pre_hash_shake256)
42+
#define crypto_sign_verify_pre_hash_shake256 \
43+
MLD_NAMESPACE_KL(verify_pre_hash_shake256)
4044

4145
/*************************************************
4246
* Hash algorithm enumeration for pre-hash functions
@@ -501,4 +505,81 @@ __contract__(
501505
ensures(return_value == 0 || return_value == -1)
502506
);
503507

508+
/*************************************************
509+
* Name: crypto_sign_signature_pre_hash_shake256
510+
*
511+
* Description: FIPS 204: Algorithm 4 HashML-DSA.Sign with SHAKE256.
512+
* Computes signature with pre-hashed message using SHAKE256.
513+
* This function computes the SHAKE256 hash of the message
514+
*internally.
515+
*
516+
* Arguments: - uint8_t *sig: pointer to output signature (of length
517+
* CRYPTO_BYTES)
518+
* - size_t *siglen: pointer to output length of signature
519+
* - const uint8_t *m: pointer to message to be hashed and signed
520+
* - size_t mlen: length of message
521+
* - const uint8_t *ctx: pointer to context string
522+
* - size_t ctxlen: length of context string
523+
* - const uint8_t *rnd: pointer to random seed
524+
* - const uint8_t *sk: pointer to bit-packed secret key
525+
*
526+
* Returns 0 (success) or -1 (context string too long OR nonce exhaustion)
527+
**************************************************/
528+
MLD_MUST_CHECK_RETURN_VALUE
529+
MLD_EXTERNAL_API
530+
int crypto_sign_signature_pre_hash_shake256(uint8_t *sig, size_t *siglen,
531+
const uint8_t *m, size_t mlen,
532+
const uint8_t *ctx, size_t ctxlen,
533+
const uint8_t rnd[MLDSA_RNDBYTES],
534+
const uint8_t *sk)
535+
__contract__(
536+
requires(mlen <= MLD_MAX_BUFFER_SIZE)
537+
requires(ctxlen <= MLD_MAX_BUFFER_SIZE)
538+
requires(memory_no_alias(sig, CRYPTO_BYTES))
539+
requires(memory_no_alias(siglen, sizeof(size_t)))
540+
requires(memory_no_alias(m, mlen))
541+
requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen))
542+
requires(memory_no_alias(rnd, MLDSA_RNDBYTES))
543+
requires(memory_no_alias(sk, CRYPTO_SECRETKEYBYTES))
544+
assigns(memory_slice(sig, CRYPTO_BYTES))
545+
assigns(object_whole(siglen))
546+
ensures((return_value == 0 && *siglen == CRYPTO_BYTES) ||
547+
(return_value == -1 && *siglen == 0))
548+
);
549+
550+
/*************************************************
551+
* Name: crypto_sign_verify_pre_hash_shake256
552+
*
553+
* Description: FIPS 204: Algorithm 5 HashML-DSA.Verify with SHAKE256.
554+
* Verifies signature with pre-hashed message using SHAKE256.
555+
* This function computes the SHAKE256 hash of the message
556+
*internally.
557+
*
558+
* Arguments: - const uint8_t *sig: pointer to input signature
559+
* - size_t siglen: length of signature
560+
* - const uint8_t *m: pointer to message to be hashed and verified
561+
* - size_t mlen: length of message
562+
* - const uint8_t *ctx: pointer to context string
563+
* - size_t ctxlen: length of context string
564+
* - const uint8_t *pk: pointer to bit-packed public key
565+
*
566+
* Returns 0 if signature could be verified correctly and -1 otherwise
567+
**************************************************/
568+
MLD_MUST_CHECK_RETURN_VALUE
569+
MLD_EXTERNAL_API
570+
int crypto_sign_verify_pre_hash_shake256(const uint8_t *sig, size_t siglen,
571+
const uint8_t *m, size_t mlen,
572+
const uint8_t *ctx, size_t ctxlen,
573+
const uint8_t *pk)
574+
__contract__(
575+
requires(mlen <= MLD_MAX_BUFFER_SIZE)
576+
requires(ctxlen <= MLD_MAX_BUFFER_SIZE - 77)
577+
requires(siglen <= MLD_MAX_BUFFER_SIZE)
578+
requires(memory_no_alias(sig, siglen))
579+
requires(memory_no_alias(m, mlen))
580+
requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen))
581+
requires(memory_no_alias(pk, CRYPTO_PUBLICKEYBYTES))
582+
ensures(return_value == 0 || return_value == -1)
583+
);
584+
504585
#endif /* !MLD_SIGN_H */

‎proofs/cbmc/crypto_sign_signature_pre_hash_shake256/Makefile‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
# Copyright (c) The mldsa-native project authors
2+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
include ../Makefile_params.common
5+
6+
HARNESS_ENTRY = harness
7+
HARNESS_FILE = crypto_sign_signature_pre_hash_shake256_harness
8+
9+
# This should be a unique identifier for this proof, and will appear on the
10+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
11+
PROOF_UID = crypto_sign_signature_pre_hash_shake256
12+
13+
DEFINES +=
14+
INCLUDES +=
15+
16+
REMOVE_FUNCTION_BODY +=
17+
UNWINDSET +=
18+
19+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
20+
PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c
21+
22+
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature_pre_hash_shake256
23+
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature_pre_hash_internal $(FIPS202_NAMESPACE)shake256
24+
25+
APPLY_LOOP_CONTRACTS=on
26+
USE_DYNAMIC_FRAMES=1
27+
28+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
29+
EXTERNAL_SAT_SOLVER=
30+
CBMCFLAGS=--smt2
31+
CBMCFLAGS += --slice-formula
32+
CBMCFLAGS += --no-array-field-sensitivity
33+
34+
FUNCTION_NAME = crypto_sign_signature_pre_hash_shake256
35+
36+
# If this proof is found to consume huge amounts of RAM, you can set the
37+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
38+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
39+
# documentation in Makefile.common under the "Job Pools" heading for details.
40+
# EXPENSIVE = true
41+
42+
# This function is large enough to need...
43+
CBMC_OBJECT_BITS = 8
44+
45+
# If you require access to a file-local ("static") function or object to conduct
46+
# your proof, set the following (and do not include the original source file
47+
# ("mldsa/poly.c") in PROJECT_SOURCES).
48+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
49+
# include ../Makefile.common
50+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c
51+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
52+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
53+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
54+
# be set before including Makefile.common, but any use of variables on the
55+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
56+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
57+
58+
include ../Makefile.common

‎proofs/cbmc/crypto_sign_signature_pre_hash_shake256/crypto_sign_signature_pre_hash_shake256_harness.c‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include "sign.h"
5+
6+
void harness(void)
7+
{
8+
uint8_t *sig;
9+
size_t *siglen;
10+
const uint8_t *m;
11+
size_t mlen;
12+
const uint8_t *ctx;
13+
size_t ctxlen;
14+
const uint8_t *rnd;
15+
const uint8_t *sk;
16+
int r;
17+
r = crypto_sign_signature_pre_hash_shake256(sig, siglen, m, mlen, ctx, ctxlen,
18+
rnd, sk);
19+
}

‎proofs/cbmc/crypto_sign_verify_pre_hash_shake256/Makefile‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
# Copyright (c) The mldsa-native project authors
2+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
include ../Makefile_params.common
5+
6+
HARNESS_ENTRY = harness
7+
HARNESS_FILE = crypto_sign_verify_pre_hash_shake256_harness
8+
9+
# This should be a unique identifier for this proof, and will appear on the
10+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
11+
PROOF_UID = crypto_sign_verify_pre_hash_shake256
12+
13+
DEFINES +=
14+
INCLUDES +=
15+
16+
REMOVE_FUNCTION_BODY +=
17+
UNWINDSET +=
18+
19+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
20+
PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c
21+
22+
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_pre_hash_shake256
23+
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_pre_hash_internal $(FIPS202_NAMESPACE)shake256
24+
25+
APPLY_LOOP_CONTRACTS=on
26+
USE_DYNAMIC_FRAMES=1
27+
28+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
29+
EXTERNAL_SAT_SOLVER=
30+
CBMCFLAGS=--smt2
31+
CBMCFLAGS += --slice-formula
32+
CBMCFLAGS += --no-array-field-sensitivity
33+
34+
FUNCTION_NAME = crypto_sign_verify_pre_hash_shake256
35+
36+
# If this proof is found to consume huge amounts of RAM, you can set the
37+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
38+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
39+
# documentation in Makefile.common under the "Job Pools" heading for details.
40+
# EXPENSIVE = true
41+
42+
# This function is large enough to need...
43+
CBMC_OBJECT_BITS = 8
44+
45+
# If you require access to a file-local ("static") function or object to conduct
46+
# your proof, set the following (and do not include the original source file
47+
# ("mldsa/poly.c") in PROJECT_SOURCES).
48+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
49+
# include ../Makefile.common
50+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c
51+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
52+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
53+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
54+
# be set before including Makefile.common, but any use of variables on the
55+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
56+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
57+
58+
include ../Makefile.common

‎proofs/cbmc/crypto_sign_verify_pre_hash_shake256/crypto_sign_verify_pre_hash_shake256_harness.c‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include "sign.h"
5+
6+
void harness(void)
7+
{
8+
const uint8_t *sig;
9+
size_t siglen;
10+
const uint8_t *m;
11+
size_t mlen;
12+
const uint8_t *ctx;
13+
size_t ctxlen;
14+
const uint8_t *pk;
15+
int r;
16+
r = crypto_sign_verify_pre_hash_shake256(sig, siglen, m, mlen, ctx, ctxlen,
17+
pk);
18+
}

‎test/acvp_client.py‎

Lines changed: 42 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -172,18 +172,29 @@ def run_sigGen_test(tg, tc):
172172
tc["rnd"] = "0" * 64
173173

174174
if tg["preHash"] == "preHash":
175-
ph = compute_hash(tc["message"], tc["hashAlg"])
176175
assert len(tc["context"]) <= 2 * 255
177176

178-
acvp_call = exec_prefix + [
179-
acvp_bin,
180-
"sigGenPreHash",
181-
f"ph={ph}",
182-
f"context={tc['context']}",
183-
f"rng={tc['rnd']}",
184-
f"sk={tc['sk']}",
185-
f"hashAlg={tc['hashAlg']}",
186-
]
177+
# Use specialized SHAKE256 function that computes hash internally
178+
if tc["hashAlg"] == "SHAKE-256":
179+
acvp_call = exec_prefix + [
180+
acvp_bin,
181+
"sigGenPreHashShake256",
182+
f"message={tc['message']}",
183+
f"context={tc['context']}",
184+
f"rnd={tc['rnd']}",
185+
f"sk={tc['sk']}",
186+
]
187+
else:
188+
ph = compute_hash(tc["message"], tc["hashAlg"])
189+
acvp_call = exec_prefix + [
190+
acvp_bin,
191+
"sigGenPreHash",
192+
f"ph={ph}",
193+
f"context={tc['context']}",
194+
f"rng={tc['rnd']}",
195+
f"sk={tc['sk']}",
196+
f"hashAlg={tc['hashAlg']}",
197+
]
187198
elif tg["signatureInterface"] == "external":
188199
assert tc["hashAlg"] == "none"
189200
assert len(tc["context"]) <= 2 * 255
@@ -238,18 +249,29 @@ def run_sigVer_test(tg, tc):
238249
acvp_bin = get_acvp_binary(tg)
239250

240251
if tg["preHash"] == "preHash":
241-
ph = compute_hash(tc["message"], tc["hashAlg"])
242252
assert len(tc["context"]) <= 2 * 255
243253

244-
acvp_call = exec_prefix + [
245-
acvp_bin,
246-
"sigVerPreHash",
247-
f"ph={ph}",
248-
f"context={tc['context']}",
249-
f"signature={tc['signature']}",
250-
f"pk={tc['pk']}",
251-
f"hashAlg={tc['hashAlg']}",
252-
]
254+
# Use specialized SHAKE256 function that computes hash internally
255+
if tc["hashAlg"] == "SHAKE-256":
256+
acvp_call = exec_prefix + [
257+
acvp_bin,
258+
"sigVerPreHashShake256",
259+
f"message={tc['message']}",
260+
f"context={tc['context']}",
261+
f"signature={tc['signature']}",
262+
f"pk={tc['pk']}",
263+
]
264+
else:
265+
ph = compute_hash(tc["message"], tc["hashAlg"])
266+
acvp_call = exec_prefix + [
267+
acvp_bin,
268+
"sigVerPreHash",
269+
f"ph={ph}",
270+
f"context={tc['context']}",
271+
f"signature={tc['signature']}",
272+
f"pk={tc['pk']}",
273+
f"hashAlg={tc['hashAlg']}",
274+
]
253275
elif tg["signatureInterface"] == "external":
254276
assert tc["hashAlg"] == "none"
255277
assert len(tc["context"]) <= 2 * 255

0 commit comments

Comments
 (0)