From 3b98b01a56bb1f0e346e8536ef0d39ff4fd9a029 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Thu, 23 Oct 2025 13:06:18 +0800 Subject: [PATCH 1/3] CBMC: Re-model preconditions allowing NULL pointers Previously if a pointer was allowed to be NULL, we would write requires((p == NULL && len == 0) || memory_no_alias(p, len)). This commit refactores that to requires(len == 0 || memory_no_alias(p, len)) which feels more natural as there is no need to force p to NULL if len is 0. Signed-off-by: Matthias J. Kannwischer --- mldsa/sign.c | 12 ++++++------ mldsa/sign.h | 12 ++++++------ 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/mldsa/sign.c b/mldsa/sign.c index f129046d4..ca25e1eb3 100644 --- a/mldsa/sign.c +++ b/mldsa/sign.c @@ -245,11 +245,11 @@ int crypto_sign_keypair(uint8_t *pk, uint8_t *sk) * 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 + * May be NULL if in2len=0, 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 + * May be NULL if in3len=0, in which case * this block is ignored * - size_t in3len: length of input in3 bytes **************************************************/ @@ -262,8 +262,8 @@ __contract__( requires(in3len <= MLD_MAX_BUFFER_SIZE) 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(in2len == 0 || memory_no_alias(in2, in2len)) + requires(in3len == 0 || memory_no_alias(in3, in3len)) requires(memory_no_alias(out, outlen)) assigns(memory_slice(out, outlen)) ) @@ -271,11 +271,11 @@ __contract__( mld_shake256ctx state; mld_shake256_init(&state); mld_shake256_absorb(&state, in1, in1len); - if (in2 != NULL) + if (in2len != 0) { mld_shake256_absorb(&state, in2, in2len); } - if (in3 != NULL) + if (in3len != 0) { mld_shake256_absorb(&state, in3, in3len); } diff --git a/mldsa/sign.h b/mldsa/sign.h index abdb8ad6a..71fef15de 100644 --- a/mldsa/sign.h +++ b/mldsa/sign.h @@ -134,7 +134,7 @@ __contract__( requires(memory_no_alias(m, mlen)) requires(memory_no_alias(rnd, MLDSA_RNDBYTES)) requires(memory_no_alias(sk, CRYPTO_SECRETKEYBYTES)) - requires((externalmu == 0 && pre != NULL && prelen >= 2 && memory_no_alias(pre, prelen)) || + requires((externalmu == 0 && (prelen == 0 || memory_no_alias(pre, prelen))) || (externalmu == 1 && mlen == MLDSA_CRHBYTES)) assigns(memory_slice(sig, CRYPTO_BYTES)) assigns(object_whole(siglen)) @@ -153,7 +153,7 @@ __contract__( * - uint8_t *m: pointer to message to be signed * - size_t mlen: length of message * - uint8_t *ctx: pointer to context string. May be NULL - * iff ctxlen == 0 + * if ctxlen == 0 * - size_t ctxlen: length of context string. Should be <= 255. * - uint8_t *sk: pointer to bit-packed secret key * @@ -173,7 +173,7 @@ __contract__( requires(memory_no_alias(siglen, sizeof(size_t))) requires(memory_no_alias(m, mlen)) requires(ctxlen <= MLD_MAX_BUFFER_SIZE) - requires((ctx == NULL && ctxlen == 0) || memory_no_alias(ctx, ctxlen)) + requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) requires(memory_no_alias(sk, CRYPTO_SECRETKEYBYTES)) assigns(memory_slice(sig, CRYPTO_BYTES)) assigns(object_whole(siglen)) @@ -281,7 +281,7 @@ __contract__( requires(memory_no_alias(sig, siglen)) requires(memory_no_alias(m, mlen)) requires(externalmu == 0 || (externalmu == 1 && mlen == MLDSA_CRHBYTES)) - requires(externalmu == 1 || memory_no_alias(pre, prelen)) + requires(externalmu == 1 || prelen == 0 || memory_no_alias(pre, prelen)) requires(memory_no_alias(pk, CRYPTO_PUBLICKEYBYTES)) ensures(return_value == 0 || return_value == -1) ); @@ -296,7 +296,7 @@ __contract__( * - const uint8_t *m: pointer to message * - size_t mlen: length of message * - const uint8_t *ctx: pointer to context string - * May be NULL iff ctxlen == 0 + * May be NULL if ctxlen == 0 * - size_t ctxlen: length of context string * - const uint8_t *pk: pointer to bit-packed public key * @@ -316,7 +316,7 @@ __contract__( requires(ctxlen <= MLD_MAX_BUFFER_SIZE) requires(memory_no_alias(sig, siglen)) requires(memory_no_alias(m, mlen)) - requires((ctx == NULL && ctxlen == 0) || memory_no_alias(ctx, ctxlen)) + requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) requires(memory_no_alias(pk, CRYPTO_PUBLICKEYBYTES)) ensures(return_value == 0 || return_value == -1) ); From ff1e0ff44e5c18d6786e13c89a8a8fa6914a0ca1 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Sun, 28 Sep 2025 21:35:12 +0800 Subject: [PATCH 2/3] Add support for PreHash ML-DSA This commit adds two functions crypto_sign_signature_pre_hash_internal and crypto_sign_verify_pre_hash_internal 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 https://github.com/pq-code-package/mldsa-native/issues/39 Signed-off-by: Matthias J. Kannwischer --- mldsa/sign.c | 204 +++++++++++++ mldsa/sign.h | 118 ++++++++ .../Makefile | 58 ++++ ...sign_signature_pre_hash_internal_harness.c | 20 ++ .../Makefile | 66 +++++ ...to_sign_verify_pre_hash_internal_harness.c | 19 ++ test/acvp_client.py | 74 ++++- test/acvp_mldsa.c | 279 +++++++++++++++++- 8 files changed, 824 insertions(+), 14 deletions(-) create mode 100644 proofs/cbmc/crypto_sign_signature_pre_hash_internal/Makefile create mode 100644 proofs/cbmc/crypto_sign_signature_pre_hash_internal/crypto_sign_signature_pre_hash_internal_harness.c create mode 100644 proofs/cbmc/crypto_sign_verify_pre_hash_internal/Makefile create mode 100644 proofs/cbmc/crypto_sign_verify_pre_hash_internal/crypto_sign_verify_pre_hash_internal_harness.c diff --git a/mldsa/sign.c b/mldsa/sign.c index ca25e1eb3..e14f861fc 100644 --- a/mldsa/sign.c +++ b/mldsa/sign.c @@ -862,3 +862,207 @@ 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_internal(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 */ + MLD_ALIGN uint8_t fmsg[2 + 255 + 11 + 64]; + int result; + + 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); + + result = crypto_sign_signature_internal( + sig, siglen, fmsg, 2 + ctxlen + 11 + phlen, NULL, 0, rnd, sk, 0); + /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ + mld_zeroize(fmsg, sizeof(fmsg)); + return result; +} + +MLD_MUST_CHECK_RETURN_VALUE +MLD_EXTERNAL_API +int crypto_sign_verify_pre_hash_internal(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 */ + MLD_ALIGN uint8_t fmsg[2 + 255 + 11 + 64]; + int result; + + 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); + + result = crypto_sign_verify_internal(sig, siglen, fmsg, + 2 + ctxlen + 11 + phlen, NULL, 0, pk, 0); + /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ + mld_zeroize(fmsg, sizeof(fmsg)); + return result; +} diff --git a/mldsa/sign.h b/mldsa/sign.h index 71fef15de..d323f9e87 100644 --- a/mldsa/sign.h +++ b/mldsa/sign.h @@ -33,6 +33,29 @@ #define crypto_sign_verify MLD_NAMESPACE_KL(verify) #define crypto_sign_verify_extmu MLD_NAMESPACE_KL(verify_extmu) #define crypto_sign_open MLD_NAMESPACE_KL(open) +#define crypto_sign_signature_pre_hash_internal \ + MLD_NAMESPACE_KL(signature_pre_hash_internal) +#define crypto_sign_verify_pre_hash_internal \ + MLD_NAMESPACE_KL(verify_pre_hash_internal) + +/************************************************* + * 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; /************************************************* * Name: crypto_sign_keypair_internal @@ -383,4 +406,99 @@ __contract__( ensures(return_value == 0 || return_value == -1) ); +/************************************************* + * Name: crypto_sign_signature_pre_hash_internal + * + * 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" + * + * Warning: This is an unstable API that may change in the future. If you need + * a stable API use crypto_sign_signature_pre_hash_shake256. + * + * 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_internal(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(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)) +); + +/************************************************* + * Name: crypto_sign_verify_pre_hash_internal + * + * 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" + * + * Warning: This is an unstable API that may change in the future. If you need + * a stable API use crypto_sign_verify_pre_hash_shake256. + * + * 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_internal(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(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 */ diff --git a/proofs/cbmc/crypto_sign_signature_pre_hash_internal/Makefile b/proofs/cbmc/crypto_sign_signature_pre_hash_internal/Makefile new file mode 100644 index 000000000..323533963 --- /dev/null +++ b/proofs/cbmc/crypto_sign_signature_pre_hash_internal/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_internal_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_internal + +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_internal +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_internal + +# 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 diff --git a/proofs/cbmc/crypto_sign_signature_pre_hash_internal/crypto_sign_signature_pre_hash_internal_harness.c b/proofs/cbmc/crypto_sign_signature_pre_hash_internal/crypto_sign_signature_pre_hash_internal_harness.c new file mode 100644 index 000000000..a2e95b529 --- /dev/null +++ b/proofs/cbmc/crypto_sign_signature_pre_hash_internal/crypto_sign_signature_pre_hash_internal_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_internal(sig, siglen, ph, phlen, ctx, + ctxlen, rnd, sk, hashAlg); +} diff --git a/proofs/cbmc/crypto_sign_verify_pre_hash_internal/Makefile b/proofs/cbmc/crypto_sign_verify_pre_hash_internal/Makefile new file mode 100644 index 000000000..88b2513f8 --- /dev/null +++ b/proofs/cbmc/crypto_sign_verify_pre_hash_internal/Makefile @@ -0,0 +1,66 @@ +# 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_verify_pre_hash_internal_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_verify_pre_hash_internal + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_pre_hash_internal +USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_internal \ + $(MLD_NAMESPACE)unpack_pk \ + $(MLD_NAMESPACE)unpack_sig \ + $(MLD_NAMESPACE)polyvec_matrix_expand \ + $(MLD_NAMESPACE)polyvecl_invntt_tomont \ + $(MLD_NAMESPACE)polyveck_invntt_tomont \ + $(MLD_NAMESPACE)polyveck_sub \ + $(MLD_NAMESPACE)polyveck_use_hint +USE_FUNCTION_CONTRACTS+=mld_zeroize + +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_verify_pre_hash_internal + +# 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 diff --git a/proofs/cbmc/crypto_sign_verify_pre_hash_internal/crypto_sign_verify_pre_hash_internal_harness.c b/proofs/cbmc/crypto_sign_verify_pre_hash_internal/crypto_sign_verify_pre_hash_internal_harness.c new file mode 100644 index 000000000..d7e757051 --- /dev/null +++ b/proofs/cbmc/crypto_sign_verify_pre_hash_internal/crypto_sign_verify_pre_hash_internal_harness.c @@ -0,0 +1,19 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "sign.h" + +void harness(void) +{ + 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; + int r; + r = crypto_sign_verify_pre_hash_internal(sig, siglen, ph, phlen, ctx, ctxlen, + pk, hashAlg); +} diff --git a/test/acvp_client.py b/test/acvp_client.py index 224039261..6afd14bfe 100644 --- a/test/acvp_client.py +++ b/test/acvp_client.py @@ -10,6 +10,7 @@ # Invokes `acvp_mldsa{lvl}` under the hood. import argparse +import hashlib import os import json import sys @@ -129,25 +130,62 @@ def run_keyGen_test(tg, tc): info("OK") +def compute_hash(msg, alg): + msg_bytes = bytes.fromhex(msg) + + if alg == "SHA2-224": + return hashlib.sha224(msg_bytes).hexdigest() + elif alg == "SHA2-256": + return hashlib.sha256(msg_bytes).hexdigest() + elif alg == "SHA2-384": + return hashlib.sha384(msg_bytes).hexdigest() + elif alg == "SHA2-512": + return hashlib.sha512(msg_bytes).hexdigest() + elif alg == "SHA2-512/224": + return hashlib.new("sha512_224", msg_bytes).hexdigest() + elif alg == "SHA2-512/256": + return hashlib.new("sha512_256", msg_bytes).hexdigest() + elif alg == "SHA3-224": + return hashlib.sha3_224(msg_bytes).hexdigest() + elif alg == "SHA3-256": + return hashlib.sha3_256(msg_bytes).hexdigest() + elif alg == "SHA3-384": + return hashlib.sha3_384(msg_bytes).hexdigest() + elif alg == "SHA3-512": + return hashlib.sha3_512(msg_bytes).hexdigest() + elif alg == "SHAKE-128": + return hashlib.shake_128(msg_bytes).hexdigest(32) + elif alg == "SHAKE-256": + return hashlib.shake_256(msg_bytes).hexdigest(64) + else: + raise ValueError(f"Unsupported hash algorithm: {alg}") + + def run_sigGen_test(tg, tc): info(f"Running sigGen test case {tc['tcId']} ... ", end="") acvp_bin = get_acvp_binary(tg) assert tg["testType"] == "AFT" - # TODO: implement pre-hashing mode - if tg["preHash"] == "preHash": - info("SKIP preHash") - return - # TODO: probably we want to handle handle the deterministic case differently if tg["deterministic"] is True: tc["rnd"] = "0" * 64 - assert tc["hashAlg"] == "none" - - if tg["signatureInterface"] == "external": + if tg["preHash"] == "preHash": + ph = compute_hash(tc["message"], tc["hashAlg"]) + assert len(tc["context"]) <= 2 * 255 + acvp_call = exec_prefix + [ + acvp_bin, + "sigGenPreHash", + f"ph={ph}", + f"context={tc['context']}", + f"rng={tc['rnd']}", + f"sk={tc['sk']}", + f"hashAlg={tc['hashAlg']}", + ] + elif tg["signatureInterface"] == "external": + assert tc["hashAlg"] == "none" assert len(tc["context"]) <= 2 * 255 assert len(tc["message"]) <= 2 * 65536 @@ -160,6 +198,7 @@ def run_sigGen_test(tg, tc): f"context={tc['context']}", ] else: # signatureInterface=internal + assert tc["hashAlg"] == "none" externalMu = 0 if tg["externalMu"] is True: externalMu = 1 @@ -198,13 +237,21 @@ def run_sigVer_test(tg, tc): info(f"Running sigVer test case {tc['tcId']} ... ", end="") acvp_bin = get_acvp_binary(tg) - # TODO: implement pre-hashing mode if tg["preHash"] == "preHash": - info("SKIP preHash") - return + ph = compute_hash(tc["message"], tc["hashAlg"]) + assert len(tc["context"]) <= 2 * 255 - assert tc["hashAlg"] == "none" - if tg["signatureInterface"] == "external": + acvp_call = exec_prefix + [ + acvp_bin, + "sigVerPreHash", + f"ph={ph}", + f"context={tc['context']}", + f"signature={tc['signature']}", + f"pk={tc['pk']}", + f"hashAlg={tc['hashAlg']}", + ] + elif tg["signatureInterface"] == "external": + assert tc["hashAlg"] == "none" assert len(tc["context"]) <= 2 * 255 assert len(tc["message"]) <= 2 * 65536 @@ -217,6 +264,7 @@ def run_sigVer_test(tg, tc): f"pk={tc['pk']}", ] else: # signatureInterface=internal + assert tc["hashAlg"] == "none" externalMu = 0 if tg["externalMu"] is True: externalMu = 1 diff --git a/test/acvp_mldsa.c b/test/acvp_mldsa.c index 049ef3143..71dc6771f 100644 --- a/test/acvp_mldsa.c +++ b/test/acvp_mldsa.c @@ -21,6 +21,13 @@ #define SIGVER_INTERNAL_USAGE \ "acvp_mldsa{lvl} sigVerInternal message=HEX signature=HEX pk=HEX " \ "externalMu=0/1" +#define SIGGEN_PREHASH_USAGE \ + "acvp_mldsa{lvl} sigGenPreHash ph=HEX context=HEX rng=HEX sk=HEX " \ + "hashAlg=STRING" +#define SIGVER_PREHASH_USAGE \ + "acvp_mldsa{lvl} sigVerPreHash ph=HEX context=HEX signature=HEX pk=HEX " \ + "hashAlg=STRING" + /* maximum message length used in the ACVP tests */ #define MAX_MSG_LENGTH 65536 @@ -45,7 +52,9 @@ typedef enum sigGen, sigGenInternal, sigVer, - sigVerInternal + sigVerInternal, + sigGenPreHash, + sigVerPreHash } acvp_mode; /* Decode hex character [0-9A-Fa-f] into 0-15 */ @@ -163,6 +172,45 @@ static int decode_keyed_int(const char *prefix_string, int *out, return 1; } +static int parse_str(const char *prefix, char *out, size_t out_max_len, + const char *str) +{ + size_t str_len = strlen(str); + size_t prefix_len = strlen(prefix); + size_t value_len; + + /* + * Check that str starts with `prefix=` + * Use memcmp, not strcmp + */ + if (str_len < prefix_len + 1 || memcmp(prefix, str, prefix_len) != 0 || + str[prefix_len] != '=') + { + goto str_usage; + } + + str += prefix_len + 1; + value_len = strlen(str); + + if (value_len >= out_max_len) + { + fprintf(stderr, + "Argument %s invalid: String value too long (max %u characters)\n", + str - prefix_len - 1, (unsigned)(out_max_len - 1)); + return 1; + } + + strncpy(out, str, out_max_len - 1); + out[out_max_len - 1] = '\0'; + return 0; + +str_usage: + fprintf(stderr, + "Argument %s invalid: Expected argument of the form '%s=STRING'\n", + str, prefix); + return 1; +} + static void print_hex(const char *name, const unsigned char *raw, size_t len) { if (name != NULL) @@ -245,6 +293,91 @@ static int acvp_mldsa_sigVerInternal_AFT( } } +static mld_hash_alg_t str_to_hash_alg(const char *hashAlg) +{ + if (strcmp(hashAlg, "SHA2-224") == 0) + { + return MLD_SHA2_224; + } + if (strcmp(hashAlg, "SHA2-256") == 0) + { + return MLD_SHA2_256; + } + if (strcmp(hashAlg, "SHA2-384") == 0) + { + return MLD_SHA2_384; + } + if (strcmp(hashAlg, "SHA2-512") == 0) + { + return MLD_SHA2_512; + } + if (strcmp(hashAlg, "SHA2-512/224") == 0) + { + return MLD_SHA2_512_224; + } + if (strcmp(hashAlg, "SHA2-512/256") == 0) + { + return MLD_SHA2_512_256; + } + if (strcmp(hashAlg, "SHA3-224") == 0) + { + return MLD_SHA3_224; + } + if (strcmp(hashAlg, "SHA3-256") == 0) + { + return MLD_SHA3_256; + } + if (strcmp(hashAlg, "SHA3-384") == 0) + { + return MLD_SHA3_384; + } + if (strcmp(hashAlg, "SHA3-512") == 0) + { + return MLD_SHA3_512; + } + if (strcmp(hashAlg, "SHAKE-128") == 0) + { + return MLD_SHAKE_128; + } + if (strcmp(hashAlg, "SHAKE-256") == 0) + { + return MLD_SHAKE_256; + } + /* Invalid hash algorithm */ + fprintf(stderr, "Error: Unsupported hash algorithm: %s\n", hashAlg); + exit(1); +} + +static int acvp_mldsa_sigGenPreHash_AFT( + const unsigned char *ph, size_t phlen, const unsigned char *context, + size_t ctxlen, const unsigned char rng[MLDSA_RNDBYTES], + const unsigned char sk[CRYPTO_SECRETKEYBYTES], const char *hashAlg) +{ + unsigned char signature[CRYPTO_BYTES]; + size_t siglen; + + if (crypto_sign_signature_pre_hash_internal(signature, &siglen, ph, phlen, + context, ctxlen, rng, sk, + str_to_hash_alg(hashAlg)) != 0) + { + return 1; + } + + print_hex("signature", signature, siglen); + return 0; +} + +static int acvp_mldsa_sigVerPreHash_AFT( + const unsigned char *ph, size_t phlen, const unsigned char *context, + size_t ctxlen, const unsigned char signature[CRYPTO_BYTES], + const unsigned char pk[CRYPTO_PUBLICKEYBYTES], const char *hashAlg) +{ + return crypto_sign_verify_pre_hash_internal(signature, CRYPTO_BYTES, ph, + phlen, context, ctxlen, pk, + str_to_hash_alg(hashAlg)); +} + + int main(int argc, char *argv[]) { acvp_mode mode; @@ -280,6 +413,14 @@ int main(int argc, char *argv[]) { mode = sigVerInternal; } + else if (strcmp(*argv, "sigGenPreHash") == 0) + { + mode = sigGenPreHash; + } + else if (strcmp(*argv, "sigVerPreHash") == 0) + { + mode = sigVerPreHash; + } else { goto usage; @@ -514,6 +655,134 @@ int main(int argc, char *argv[]) return acvp_mldsa_sigVerInternal_AFT(message, mlen, signature, pk, externalMu); } + + case sigGenPreHash: + { + unsigned char ph[64]; + unsigned char context[MAX_CTX_LENGTH]; + unsigned char rng[MLDSA_RNDBYTES]; + unsigned char sk[CRYPTO_SECRETKEYBYTES]; + char hashAlg[100]; + size_t phlen; + size_t ctxlen; + + /* Parse ph */ + if (argc == 0) + { + goto siggen_prehash_usage; + } + phlen = (strlen(*argv) - strlen("ph=")) / 2; + if (phlen > 64 || decode_hex("ph", ph, phlen, *argv) != 0) + { + goto siggen_prehash_usage; + } + argc--, argv++; + + /* Parse context */ + if (argc == 0) + { + goto siggen_prehash_usage; + } + ctxlen = (strlen(*argv) - strlen("context=")) / 2; + if (ctxlen > MAX_CTX_LENGTH || + decode_hex("context", context, ctxlen, *argv) != 0) + { + goto siggen_prehash_usage; + } + argc--, argv++; + + /* Parse rng */ + if (argc == 0 || decode_hex("rng", rng, sizeof(rng), *argv) != 0) + { + goto siggen_prehash_usage; + } + argc--, argv++; + + /* Parse sk */ + if (argc == 0 || decode_hex("sk", sk, sizeof(sk), *argv) != 0) + { + goto siggen_prehash_usage; + } + argc--, argv++; + + /* Parse hashAlg */ + if (argc == 0 || + parse_str("hashAlg", hashAlg, sizeof(hashAlg), *argv) != 0) + { + goto siggen_prehash_usage; + } + argc--, argv++; + + /* Call function under test */ + return acvp_mldsa_sigGenPreHash_AFT(ph, phlen, context, ctxlen, rng, sk, + hashAlg); + } + + case sigVerPreHash: + { + unsigned char ph[64]; + unsigned char context[MAX_CTX_LENGTH]; + unsigned char signature[CRYPTO_BYTES]; + unsigned char pk[CRYPTO_PUBLICKEYBYTES]; + char hashAlg[100]; + size_t phlen; + size_t ctxlen; + + /* Parse message */ + if (argc == 0) + { + goto sigver_prehash_usage; + } + phlen = (strlen(*argv) - strlen("ph=")) / 2; + if (phlen > 64 || decode_hex("ph", ph, phlen, *argv) != 0) + { + goto sigver_prehash_usage; + } + argc--, argv++; + + /* Parse context */ + if (argc == 0) + { + goto sigver_prehash_usage; + } + ctxlen = (strlen(*argv) - strlen("context=")) / 2; + if (ctxlen > MAX_CTX_LENGTH || + decode_hex("context", context, ctxlen, *argv) != 0) + { + goto sigver_prehash_usage; + } + argc--, argv++; + + /* Parse signature */ + if (argc == 0 || + decode_hex("signature", signature, sizeof(signature), *argv) != 0) + { + goto sigver_prehash_usage; + } + argc--, argv++; + + + /* Parse pk */ + if (argc == 0 || decode_hex("pk", pk, sizeof(pk), *argv) != 0) + { + goto sigver_prehash_usage; + } + argc--, argv++; + + /* Parse hashAlg */ + if (argc == 0 || + parse_str("hashAlg", hashAlg, sizeof(hashAlg), *argv) != 0) + { + goto sigver_prehash_usage; + } + argc--, argv++; + + + + /* Call function under test */ + return acvp_mldsa_sigVerPreHash_AFT(ph, phlen, context, ctxlen, signature, + pk, hashAlg); + } } return (0); @@ -541,4 +810,12 @@ int main(int argc, char *argv[]) sigver_internal_usage: fprintf(stderr, SIGVER_INTERNAL_USAGE "\n"); return (1); + +siggen_prehash_usage: + fprintf(stderr, SIGGEN_PREHASH_USAGE "\n"); + return (1); + +sigver_prehash_usage: + fprintf(stderr, SIGVER_PREHASH_USAGE "\n"); + return (1); } From 1a74760aed3cc95d581925ab6267e30db48baf4f Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Thu, 23 Oct 2025 10:50:22 +0800 Subject: [PATCH 3/3] HashML-DSA: Add specialized shake256 pre-hashing function The previous commit added the _pre_hash_internal functions that expect the pre-hashed message, i.e., requiring the callee to compute the pre-hash themselves. The alternative is to perform the pre-hashing inside mldsa-native which eases the use for the consumer. However, that would require maintaining 12 hash functions and allowing consumers to replace those with their own hash functions. This commit implements a compromise: We do add an API that includes the pre-hashing step, but only for the most popular pre-hashing hash function: SHAKE256. If later a consumer also requires other hash functions, we can add it. Signed-off-by: Matthias J. Kannwischer --- mldsa/sign.c | 35 ++++ mldsa/sign.h | 81 +++++++++ .../Makefile | 58 +++++++ ...sign_signature_pre_hash_shake256_harness.c | 19 ++ .../Makefile | 58 +++++++ ...to_sign_verify_pre_hash_shake256_harness.c | 18 ++ test/acvp_client.py | 62 ++++--- test/acvp_mldsa.c | 162 +++++++++++++++++- 8 files changed, 472 insertions(+), 21 deletions(-) create mode 100644 proofs/cbmc/crypto_sign_signature_pre_hash_shake256/Makefile create mode 100644 proofs/cbmc/crypto_sign_signature_pre_hash_shake256/crypto_sign_signature_pre_hash_shake256_harness.c create mode 100644 proofs/cbmc/crypto_sign_verify_pre_hash_shake256/Makefile create mode 100644 proofs/cbmc/crypto_sign_verify_pre_hash_shake256/crypto_sign_verify_pre_hash_shake256_harness.c diff --git a/mldsa/sign.c b/mldsa/sign.c index e14f861fc..18caeeb5e 100644 --- a/mldsa/sign.c +++ b/mldsa/sign.c @@ -1066,3 +1066,38 @@ int crypto_sign_verify_pre_hash_internal(const uint8_t *sig, size_t siglen, mld_zeroize(fmsg, sizeof(fmsg)); return result; } + +MLD_MUST_CHECK_RETURN_VALUE +MLD_EXTERNAL_API +int crypto_sign_signature_pre_hash_shake256(uint8_t *sig, size_t *siglen, + const uint8_t *m, size_t mlen, + const uint8_t *ctx, size_t ctxlen, + const uint8_t rnd[MLDSA_RNDBYTES], + const uint8_t *sk) +{ + MLD_ALIGN uint8_t ph[64]; + int result; + mld_shake256(ph, sizeof(ph), m, mlen); + result = crypto_sign_signature_pre_hash_internal( + sig, siglen, ph, sizeof(ph), ctx, ctxlen, rnd, sk, MLD_SHAKE_256); + /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ + mld_zeroize(ph, sizeof(ph)); + return result; +} + +MLD_MUST_CHECK_RETURN_VALUE +MLD_EXTERNAL_API +int crypto_sign_verify_pre_hash_shake256(const uint8_t *sig, size_t siglen, + const uint8_t *m, size_t mlen, + const uint8_t *ctx, size_t ctxlen, + const uint8_t *pk) +{ + MLD_ALIGN uint8_t ph[64]; + int result; + mld_shake256(ph, sizeof(ph), m, mlen); + result = crypto_sign_verify_pre_hash_internal(sig, siglen, ph, sizeof(ph), + ctx, ctxlen, pk, MLD_SHAKE_256); + /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ + mld_zeroize(ph, sizeof(ph)); + return result; +} diff --git a/mldsa/sign.h b/mldsa/sign.h index d323f9e87..4e3421c3d 100644 --- a/mldsa/sign.h +++ b/mldsa/sign.h @@ -37,6 +37,10 @@ MLD_NAMESPACE_KL(signature_pre_hash_internal) #define crypto_sign_verify_pre_hash_internal \ MLD_NAMESPACE_KL(verify_pre_hash_internal) +#define crypto_sign_signature_pre_hash_shake256 \ + MLD_NAMESPACE_KL(signature_pre_hash_shake256) +#define crypto_sign_verify_pre_hash_shake256 \ + MLD_NAMESPACE_KL(verify_pre_hash_shake256) /************************************************* * Hash algorithm enumeration for pre-hash functions @@ -501,4 +505,81 @@ __contract__( ensures(return_value == 0 || return_value == -1) ); +/************************************************* + * Name: crypto_sign_signature_pre_hash_shake256 + * + * Description: FIPS 204: Algorithm 4 HashML-DSA.Sign with SHAKE256. + * Computes signature with pre-hashed message using SHAKE256. + * This function computes the SHAKE256 hash of the message + *internally. + * + * Arguments: - uint8_t *sig: pointer to output signature (of length + * CRYPTO_BYTES) + * - size_t *siglen: pointer to output length of signature + * - const uint8_t *m: pointer to message to be hashed and signed + * - size_t mlen: length of 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 + * + * 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_shake256(uint8_t *sig, size_t *siglen, + const uint8_t *m, size_t mlen, + const uint8_t *ctx, size_t ctxlen, + const uint8_t rnd[MLDSA_RNDBYTES], + const uint8_t *sk) +__contract__( + requires(mlen <= MLD_MAX_BUFFER_SIZE) + 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(m, mlen)) + requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) + requires(memory_no_alias(rnd, MLDSA_RNDBYTES)) + requires(memory_no_alias(sk, CRYPTO_SECRETKEYBYTES)) + assigns(memory_slice(sig, CRYPTO_BYTES)) + assigns(object_whole(siglen)) + ensures((return_value == 0 && *siglen == CRYPTO_BYTES) || + (return_value == -1 && *siglen == 0)) +); + +/************************************************* + * Name: crypto_sign_verify_pre_hash_shake256 + * + * Description: FIPS 204: Algorithm 5 HashML-DSA.Verify with SHAKE256. + * Verifies signature with pre-hashed message using SHAKE256. + * This function computes the SHAKE256 hash of the message + *internally. + * + * Arguments: - const uint8_t *sig: pointer to input signature + * - size_t siglen: length of signature + * - const uint8_t *m: pointer to message to be hashed and verified + * - size_t mlen: length of 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 + * + * 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_shake256(const uint8_t *sig, size_t siglen, + const uint8_t *m, size_t mlen, + const uint8_t *ctx, size_t ctxlen, + const uint8_t *pk) +__contract__( + requires(mlen <= MLD_MAX_BUFFER_SIZE) + requires(ctxlen <= MLD_MAX_BUFFER_SIZE - 77) + requires(siglen <= MLD_MAX_BUFFER_SIZE) + requires(memory_no_alias(sig, siglen)) + requires(memory_no_alias(m, mlen)) + requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) + requires(memory_no_alias(pk, CRYPTO_PUBLICKEYBYTES)) + ensures(return_value == 0 || return_value == -1) +); + #endif /* !MLD_SIGN_H */ diff --git a/proofs/cbmc/crypto_sign_signature_pre_hash_shake256/Makefile b/proofs/cbmc/crypto_sign_signature_pre_hash_shake256/Makefile new file mode 100644 index 000000000..49b317f55 --- /dev/null +++ b/proofs/cbmc/crypto_sign_signature_pre_hash_shake256/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_shake256_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_shake256 + +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_shake256 +USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature_pre_hash_internal $(FIPS202_NAMESPACE)shake256 + +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_shake256 + +# 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 diff --git a/proofs/cbmc/crypto_sign_signature_pre_hash_shake256/crypto_sign_signature_pre_hash_shake256_harness.c b/proofs/cbmc/crypto_sign_signature_pre_hash_shake256/crypto_sign_signature_pre_hash_shake256_harness.c new file mode 100644 index 000000000..da885f746 --- /dev/null +++ b/proofs/cbmc/crypto_sign_signature_pre_hash_shake256/crypto_sign_signature_pre_hash_shake256_harness.c @@ -0,0 +1,19 @@ +// 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 *m; + size_t mlen; + const uint8_t *ctx; + size_t ctxlen; + const uint8_t *rnd; + const uint8_t *sk; + int r; + r = crypto_sign_signature_pre_hash_shake256(sig, siglen, m, mlen, ctx, ctxlen, + rnd, sk); +} diff --git a/proofs/cbmc/crypto_sign_verify_pre_hash_shake256/Makefile b/proofs/cbmc/crypto_sign_verify_pre_hash_shake256/Makefile new file mode 100644 index 000000000..6f1f53766 --- /dev/null +++ b/proofs/cbmc/crypto_sign_verify_pre_hash_shake256/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_verify_pre_hash_shake256_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_verify_pre_hash_shake256 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_pre_hash_shake256 +USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_pre_hash_internal $(FIPS202_NAMESPACE)shake256 + +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_verify_pre_hash_shake256 + +# 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 diff --git a/proofs/cbmc/crypto_sign_verify_pre_hash_shake256/crypto_sign_verify_pre_hash_shake256_harness.c b/proofs/cbmc/crypto_sign_verify_pre_hash_shake256/crypto_sign_verify_pre_hash_shake256_harness.c new file mode 100644 index 000000000..3c46981cc --- /dev/null +++ b/proofs/cbmc/crypto_sign_verify_pre_hash_shake256/crypto_sign_verify_pre_hash_shake256_harness.c @@ -0,0 +1,18 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "sign.h" + +void harness(void) +{ + const uint8_t *sig; + size_t siglen; + const uint8_t *m; + size_t mlen; + const uint8_t *ctx; + size_t ctxlen; + const uint8_t *pk; + int r; + r = crypto_sign_verify_pre_hash_shake256(sig, siglen, m, mlen, ctx, ctxlen, + pk); +} diff --git a/test/acvp_client.py b/test/acvp_client.py index 6afd14bfe..419b28d05 100644 --- a/test/acvp_client.py +++ b/test/acvp_client.py @@ -172,18 +172,29 @@ def run_sigGen_test(tg, tc): tc["rnd"] = "0" * 64 if tg["preHash"] == "preHash": - ph = compute_hash(tc["message"], tc["hashAlg"]) assert len(tc["context"]) <= 2 * 255 - acvp_call = exec_prefix + [ - acvp_bin, - "sigGenPreHash", - f"ph={ph}", - f"context={tc['context']}", - f"rng={tc['rnd']}", - f"sk={tc['sk']}", - f"hashAlg={tc['hashAlg']}", - ] + # Use specialized SHAKE256 function that computes hash internally + if tc["hashAlg"] == "SHAKE-256": + acvp_call = exec_prefix + [ + acvp_bin, + "sigGenPreHashShake256", + f"message={tc['message']}", + f"context={tc['context']}", + f"rnd={tc['rnd']}", + f"sk={tc['sk']}", + ] + else: + ph = compute_hash(tc["message"], tc["hashAlg"]) + acvp_call = exec_prefix + [ + acvp_bin, + "sigGenPreHash", + f"ph={ph}", + f"context={tc['context']}", + f"rng={tc['rnd']}", + f"sk={tc['sk']}", + f"hashAlg={tc['hashAlg']}", + ] elif tg["signatureInterface"] == "external": assert tc["hashAlg"] == "none" assert len(tc["context"]) <= 2 * 255 @@ -238,18 +249,29 @@ def run_sigVer_test(tg, tc): acvp_bin = get_acvp_binary(tg) if tg["preHash"] == "preHash": - ph = compute_hash(tc["message"], tc["hashAlg"]) assert len(tc["context"]) <= 2 * 255 - acvp_call = exec_prefix + [ - acvp_bin, - "sigVerPreHash", - f"ph={ph}", - f"context={tc['context']}", - f"signature={tc['signature']}", - f"pk={tc['pk']}", - f"hashAlg={tc['hashAlg']}", - ] + # Use specialized SHAKE256 function that computes hash internally + if tc["hashAlg"] == "SHAKE-256": + acvp_call = exec_prefix + [ + acvp_bin, + "sigVerPreHashShake256", + f"message={tc['message']}", + f"context={tc['context']}", + f"signature={tc['signature']}", + f"pk={tc['pk']}", + ] + else: + ph = compute_hash(tc["message"], tc["hashAlg"]) + acvp_call = exec_prefix + [ + acvp_bin, + "sigVerPreHash", + f"ph={ph}", + f"context={tc['context']}", + f"signature={tc['signature']}", + f"pk={tc['pk']}", + f"hashAlg={tc['hashAlg']}", + ] elif tg["signatureInterface"] == "external": assert tc["hashAlg"] == "none" assert len(tc["context"]) <= 2 * 255 diff --git a/test/acvp_mldsa.c b/test/acvp_mldsa.c index 71dc6771f..2d34d5875 100644 --- a/test/acvp_mldsa.c +++ b/test/acvp_mldsa.c @@ -27,6 +27,12 @@ #define SIGVER_PREHASH_USAGE \ "acvp_mldsa{lvl} sigVerPreHash ph=HEX context=HEX signature=HEX pk=HEX " \ "hashAlg=STRING" +#define SIGGEN_PREHASH_SHAKE256_USAGE \ + "acvp_mldsa{lvl} sigGenPreHashShake256 message=HEX context=HEX rnd=HEX " \ + "sk=HEX" +#define SIGVER_PREHASH_SHAKE256_USAGE \ + "acvp_mldsa{lvl} sigVerPreHashShake256 message=HEX context=HEX " \ + "signature=HEX pk=HEX" /* maximum message length used in the ACVP tests */ @@ -54,7 +60,9 @@ typedef enum sigVer, sigVerInternal, sigGenPreHash, - sigVerPreHash + sigVerPreHash, + sigGenPreHashShake256, + sigVerPreHashShake256 } acvp_mode; /* Decode hex character [0-9A-Fa-f] into 0-15 */ @@ -377,6 +385,33 @@ static int acvp_mldsa_sigVerPreHash_AFT( str_to_hash_alg(hashAlg)); } +static int acvp_mldsa_sigGenPreHashShake256_AFT( + const unsigned char *message, size_t mlen, const unsigned char *context, + size_t ctxlen, const unsigned char rnd[MLDSA_RNDBYTES], + const unsigned char sk[CRYPTO_SECRETKEYBYTES]) +{ + unsigned char signature[CRYPTO_BYTES]; + size_t siglen; + + if (crypto_sign_signature_pre_hash_shake256(signature, &siglen, message, mlen, + context, ctxlen, rnd, sk) != 0) + { + return 1; + } + + print_hex("signature", signature, siglen); + return 0; +} + +static int acvp_mldsa_sigVerPreHashShake256_AFT( + const unsigned char *message, size_t mlen, const unsigned char *context, + size_t ctxlen, const unsigned char signature[CRYPTO_BYTES], + const unsigned char pk[CRYPTO_PUBLICKEYBYTES]) +{ + return crypto_sign_verify_pre_hash_shake256(signature, CRYPTO_BYTES, message, + mlen, context, ctxlen, pk); +} + int main(int argc, char *argv[]) { @@ -421,6 +456,14 @@ int main(int argc, char *argv[]) { mode = sigVerPreHash; } + else if (strcmp(*argv, "sigGenPreHashShake256") == 0) + { + mode = sigGenPreHashShake256; + } + else if (strcmp(*argv, "sigVerPreHashShake256") == 0) + { + mode = sigVerPreHashShake256; + } else { goto usage; @@ -783,6 +826,115 @@ int main(int argc, char *argv[]) return acvp_mldsa_sigVerPreHash_AFT(ph, phlen, context, ctxlen, signature, pk, hashAlg); } + + case sigGenPreHashShake256: + { + unsigned char message[MAX_MSG_LENGTH]; + unsigned char context[MAX_CTX_LENGTH]; + unsigned char rnd[MLDSA_RNDBYTES]; + unsigned char sk[CRYPTO_SECRETKEYBYTES]; + size_t mlen; + size_t ctxlen; + + /* Parse message */ + if (argc == 0) + { + goto siggen_prehash_shake256_usage; + } + mlen = (strlen(*argv) - strlen("message=")) / 2; + if (mlen > MAX_MSG_LENGTH || + decode_hex("message", message, mlen, *argv) != 0) + { + goto siggen_prehash_shake256_usage; + } + argc--, argv++; + + /* Parse context */ + if (argc == 0) + { + goto siggen_prehash_shake256_usage; + } + ctxlen = (strlen(*argv) - strlen("context=")) / 2; + if (ctxlen > MAX_CTX_LENGTH || + decode_hex("context", context, ctxlen, *argv) != 0) + { + goto siggen_prehash_shake256_usage; + } + argc--, argv++; + + /* Parse rnd */ + if (argc == 0 || decode_hex("rnd", rnd, sizeof(rnd), *argv) != 0) + { + goto siggen_prehash_shake256_usage; + } + argc--, argv++; + + /* Parse sk */ + if (argc == 0 || decode_hex("sk", sk, sizeof(sk), *argv) != 0) + { + goto siggen_prehash_shake256_usage; + } + argc--, argv++; + + /* Call function under test */ + return acvp_mldsa_sigGenPreHashShake256_AFT(message, mlen, context, + ctxlen, rnd, sk); + } + + case sigVerPreHashShake256: + { + unsigned char message[MAX_MSG_LENGTH]; + unsigned char context[MAX_CTX_LENGTH]; + unsigned char signature[CRYPTO_BYTES]; + unsigned char pk[CRYPTO_PUBLICKEYBYTES]; + size_t mlen; + size_t ctxlen; + + /* Parse message */ + if (argc == 0) + { + goto sigver_prehash_shake256_usage; + } + mlen = (strlen(*argv) - strlen("message=")) / 2; + if (mlen > MAX_MSG_LENGTH || + decode_hex("message", message, mlen, *argv) != 0) + { + goto sigver_prehash_shake256_usage; + } + argc--, argv++; + + /* Parse context */ + if (argc == 0) + { + goto sigver_prehash_shake256_usage; + } + ctxlen = (strlen(*argv) - strlen("context=")) / 2; + if (ctxlen > MAX_CTX_LENGTH || + decode_hex("context", context, ctxlen, *argv) != 0) + { + goto sigver_prehash_shake256_usage; + } + argc--, argv++; + + /* Parse signature */ + if (argc == 0 || + decode_hex("signature", signature, sizeof(signature), *argv) != 0) + { + goto sigver_prehash_shake256_usage; + } + argc--, argv++; + + /* Parse pk */ + if (argc == 0 || decode_hex("pk", pk, sizeof(pk), *argv) != 0) + { + goto sigver_prehash_shake256_usage; + } + argc--, argv++; + + /* Call function under test */ + return acvp_mldsa_sigVerPreHashShake256_AFT(message, mlen, context, + ctxlen, signature, pk); + } } return (0); @@ -818,4 +970,12 @@ int main(int argc, char *argv[]) sigver_prehash_usage: fprintf(stderr, SIGVER_PREHASH_USAGE "\n"); return (1); + +siggen_prehash_shake256_usage: + fprintf(stderr, SIGGEN_PREHASH_SHAKE256_USAGE "\n"); + return (1); + +sigver_prehash_shake256_usage: + fprintf(stderr, SIGVER_PREHASH_SHAKE256_USAGE "\n"); + return (1); }