From 0dd40db967acdb2546bdd3d3fae73c268cb843f8 Mon Sep 17 00:00:00 2001 From: Brendan Moran Date: Wed, 10 Sep 2025 14:35:04 +0100 Subject: [PATCH 1/5] Avoid calling keccak_absorb with partial lanes Signed-off-by: Brendan Moran --- mldsa/sign.c | 58 +++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 48 insertions(+), 10 deletions(-) diff --git a/mldsa/sign.c b/mldsa/sign.c index f129046d4..dc920cd56 100644 --- a/mldsa/sign.c +++ b/mldsa/sign.c @@ -231,6 +231,44 @@ int crypto_sign_keypair(uint8_t *pk, uint8_t *sk) return result; } +static void shake256_absorb_with_residual( + keccak_state *state, const uint8_t *in, size_t inlen, + uint8_t *residual, size_t *pos) +__contract__( + requires(0 <= *pos && pos <= 8) + requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(in == NULL || memory_no_alias(in, inlen)) + requires(memory_no_alias(residual, 8)) + assigns(memory_slice(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) + assigns(memory_slice(residual, 8)) + assigns(*pos) +) +{ + size_t nb; + if(in){ + if (*pos) { + nb = inlen < 8 - *pos ? inlen : 8 - *pos; + memcpy(residual + *pos, in, nb); + inlen -= nb; + in += nb; + *pos += nb; + if (*pos == 8) { + shake256_absorb(state, residual, 8U); + } + } + nb = inlen & ~7UL; + if (nb) { + shake256_absorb(state, in, nb); + in += nb; + inlen -= nb; + } + if (inlen) { + memcpy(residual, in, inlen); + *pos = inlen; + } + } +} + /************************************************* * Name: mld_H * @@ -268,16 +306,15 @@ __contract__( assigns(memory_slice(out, outlen)) ) { - mld_shake256ctx state; - mld_shake256_init(&state); - mld_shake256_absorb(&state, in1, in1len); - if (in2 != NULL) - { - mld_shake256_absorb(&state, in2, in2len); - } - if (in3 != NULL) - { - mld_shake256_absorb(&state, in3, in3len); + keccak_state state; + uint8_t buf[8]; + size_t pos=0; + shake256_init(&state); + shake256_absorb_with_residual(&state, in1, in1len, buf, &pos); + shake256_absorb_with_residual(&state, in2, in2len, buf, &pos); + shake256_absorb_with_residual(&state, in3, in3len, buf, &pos); + if(pos) { + shake256_absorb(&state, buf, pos); } mld_shake256_finalize(&state); mld_shake256_squeeze(out, outlen, &state); @@ -285,6 +322,7 @@ __contract__( /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ mld_zeroize(&state, sizeof(state)); + mld_zeroize(&buf, sizeof(buf)); } /* Reference: The reference implementation does not explicitly */ From d868cc1a390c9fc3ae831f70e822ad7c67d37262 Mon Sep 17 00:00:00 2001 From: Brendan Moran Date: Wed, 10 Sep 2025 14:54:00 +0100 Subject: [PATCH 2/5] Fix pos reset, fix linting errors Signed-off-by: Brendan Moran --- mldsa/sign.c | 27 +++++++++++++++++---------- 1 file changed, 17 insertions(+), 10 deletions(-) diff --git a/mldsa/sign.c b/mldsa/sign.c index dc920cd56..c6b74b4ac 100644 --- a/mldsa/sign.c +++ b/mldsa/sign.c @@ -231,9 +231,9 @@ int crypto_sign_keypair(uint8_t *pk, uint8_t *sk) return result; } -static void shake256_absorb_with_residual( - keccak_state *state, const uint8_t *in, size_t inlen, - uint8_t *residual, size_t *pos) +static void shake256_absorb_with_residual(keccak_state *state, + const uint8_t *in, size_t inlen, + uint8_t *residual, size_t *pos) __contract__( requires(0 <= *pos && pos <= 8) requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) @@ -245,24 +245,30 @@ __contract__( ) { size_t nb; - if(in){ - if (*pos) { + if (in) + { + if (*pos) + { nb = inlen < 8 - *pos ? inlen : 8 - *pos; memcpy(residual + *pos, in, nb); inlen -= nb; in += nb; *pos += nb; - if (*pos == 8) { + if (*pos == 8) + { shake256_absorb(state, residual, 8U); + *pos = 0; } } nb = inlen & ~7UL; - if (nb) { + if (nb) + { shake256_absorb(state, in, nb); in += nb; inlen -= nb; } - if (inlen) { + if (inlen) + { memcpy(residual, in, inlen); *pos = inlen; } @@ -308,12 +314,13 @@ __contract__( { keccak_state state; uint8_t buf[8]; - size_t pos=0; + size_t pos = 0; shake256_init(&state); shake256_absorb_with_residual(&state, in1, in1len, buf, &pos); shake256_absorb_with_residual(&state, in2, in2len, buf, &pos); shake256_absorb_with_residual(&state, in3, in3len, buf, &pos); - if(pos) { + if (pos) + { shake256_absorb(&state, buf, pos); } mld_shake256_finalize(&state); From a8d2d6a8b0efde1e37923bb4d8373a1645d12b6c Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Sat, 4 Oct 2025 08:33:02 +0800 Subject: [PATCH 3/5] Fix after FIPS202 function renaming Signed-off-by: Matthias J. Kannwischer --- mldsa/sign.c | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/mldsa/sign.c b/mldsa/sign.c index c6b74b4ac..83f748906 100644 --- a/mldsa/sign.c +++ b/mldsa/sign.c @@ -231,15 +231,15 @@ int crypto_sign_keypair(uint8_t *pk, uint8_t *sk) return result; } -static void shake256_absorb_with_residual(keccak_state *state, - const uint8_t *in, size_t inlen, - uint8_t *residual, size_t *pos) +static void mld_shake256_absorb_with_residual(mld_shake256ctx *state, + const uint8_t *in, size_t inlen, + uint8_t *residual, size_t *pos) __contract__( requires(0 <= *pos && pos <= 8) - requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(memory_no_alias(state, sizeof(mld_shake256ctx))) requires(in == NULL || memory_no_alias(in, inlen)) requires(memory_no_alias(residual, 8)) - assigns(memory_slice(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) + assigns(memory_slice(state, sizeof(mld_shake256ctx))) assigns(memory_slice(residual, 8)) assigns(*pos) ) @@ -256,14 +256,14 @@ __contract__( *pos += nb; if (*pos == 8) { - shake256_absorb(state, residual, 8U); + mld_shake256_absorb(state, residual, 8U); *pos = 0; } } nb = inlen & ~7UL; if (nb) { - shake256_absorb(state, in, nb); + mld_shake256_absorb(state, in, nb); in += nb; inlen -= nb; } @@ -312,23 +312,22 @@ __contract__( assigns(memory_slice(out, outlen)) ) { - keccak_state state; + mld_shake256ctx state; uint8_t buf[8]; size_t pos = 0; - shake256_init(&state); - shake256_absorb_with_residual(&state, in1, in1len, buf, &pos); - shake256_absorb_with_residual(&state, in2, in2len, buf, &pos); - shake256_absorb_with_residual(&state, in3, in3len, buf, &pos); + mld_shake256_init(&state); + mld_shake256_absorb_with_residual(&state, in1, in1len, buf, &pos); + mld_shake256_absorb_with_residual(&state, in2, in2len, buf, &pos); + mld_shake256_absorb_with_residual(&state, in3, in3len, buf, &pos); if (pos) { - shake256_absorb(&state, buf, pos); + mld_shake256_absorb(&state, buf, pos); } mld_shake256_finalize(&state); mld_shake256_squeeze(out, outlen, &state); mld_shake256_release(&state); /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ - mld_zeroize(&state, sizeof(state)); mld_zeroize(&buf, sizeof(buf)); } From f82f72964bc99dc37d224a17cc54cffd544be18c Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Sat, 4 Oct 2025 08:36:02 +0800 Subject: [PATCH 4/5] Remove contract of mld_shake256_absorb_with_residual This gets inlined into the proof of mld_H - no need for a separate contract if the proofs go through. Signed-off-by: Matthias J. Kannwischer --- mldsa/sign.c | 9 --------- 1 file changed, 9 deletions(-) diff --git a/mldsa/sign.c b/mldsa/sign.c index 83f748906..135be8af5 100644 --- a/mldsa/sign.c +++ b/mldsa/sign.c @@ -234,15 +234,6 @@ int crypto_sign_keypair(uint8_t *pk, uint8_t *sk) static void mld_shake256_absorb_with_residual(mld_shake256ctx *state, const uint8_t *in, size_t inlen, uint8_t *residual, size_t *pos) -__contract__( - requires(0 <= *pos && pos <= 8) - requires(memory_no_alias(state, sizeof(mld_shake256ctx))) - requires(in == NULL || memory_no_alias(in, inlen)) - requires(memory_no_alias(residual, 8)) - assigns(memory_slice(state, sizeof(mld_shake256ctx))) - assigns(memory_slice(residual, 8)) - assigns(*pos) -) { size_t nb; if (in) From 81844535e1cb08995816ab2d3a9534429e34e220 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Sat, 4 Oct 2025 03:15:21 +0100 Subject: [PATCH 5/5] Increase CBMC_OBJECT_BITS for this proof to complete. Signed-off-by: Rod Chapman --- proofs/cbmc/H/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/cbmc/H/Makefile b/proofs/cbmc/H/Makefile index 70640ffc8..fa87c4422 100644 --- a/proofs/cbmc/H/Makefile +++ b/proofs/cbmc/H/Makefile @@ -37,7 +37,7 @@ FUNCTION_NAME = mld_h # EXPENSIVE = true # This function is large enough to need... -CBMC_OBJECT_BITS = 8 +CBMC_OBJECT_BITS = 9 # 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