From 21001e3b603fa8f6370ba54a74a4ad91e5d24f2f Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Tue, 15 Jul 2025 10:16:12 +0800 Subject: [PATCH 1/2] Consistently use mld_assert instead of cassert cassert turns into a CBMC proof assertion inside of CBMC proofs, but it turns into a no-op otherwise. mld_assert behaves the save inside of CBMC proofs, but also turns into a run-time assertion in debug builds. Signed-off-by: Matthias J. Kannwischer Signed-off-by: Hanno Becker --- mldsa/fips202/fips202.c | 2 -- mldsa/polyvec.c | 14 -------------- mldsa/reduce.c | 4 +++- mldsa/rounding.c | 11 ++++++----- mldsa/sign.c | 5 ++--- 5 files changed, 11 insertions(+), 25 deletions(-) diff --git a/mldsa/fips202/fips202.c b/mldsa/fips202/fips202.c index 145c2ef4..51b1078a 100644 --- a/mldsa/fips202/fips202.c +++ b/mldsa/fips202/fips202.c @@ -93,8 +93,6 @@ __contract__( { s[i] = 0; } - - cassert(forall(k, 0, MLD_KECCAK_LANES, s[k] == 0)); } /************************************************* diff --git a/mldsa/polyvec.c b/mldsa/polyvec.c index 228b1267..56e23dcf 100644 --- a/mldsa/polyvec.c +++ b/mldsa/polyvec.c @@ -269,21 +269,7 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u, t += (int64_t)u->vec[j].coeffs[i] * v->vec[j].coeffs[i]; } - /* Substitute j == MLSDA_L into the loop invariant to get... */ - cassert(j == MLDSA_L); - cassert(t >= -(int64_t)MLDSA_L * (MLDSA_Q - 1) * (MLD_NTT_BOUND - 1)); - cassert(t <= (int64_t)MLDSA_L * (MLDSA_Q - 1) * (MLD_NTT_BOUND - 1)); - - /* ...and therefore... */ - cassert(t >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX); - cassert(t < MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX); - - /* ...which meets the "strong" case of mld_montgomery_reduce() */ r = mld_montgomery_reduce(t); - - /* ...and therefore we can assert a stronger bound on r */ - cassert(r > -MLDSA_Q); - cassert(r < MLDSA_Q); w->coeffs[i] = r; } } diff --git a/mldsa/reduce.c b/mldsa/reduce.c index fd0208a1..3efe614a 100644 --- a/mldsa/reduce.c +++ b/mldsa/reduce.c @@ -4,6 +4,7 @@ */ #include +#include "debug.h" #include "reduce.h" /************************************************* @@ -65,7 +66,8 @@ int32_t mld_reduce32(int32_t a) t = (a + (1 << 22)) >> 23; t = a - t * MLDSA_Q; - cassert((t - a) % MLDSA_Q == 0); + + mld_assert((t - a) % MLDSA_Q == 0); return t; } diff --git a/mldsa/rounding.c b/mldsa/rounding.c index 7f268aef..dee9f37b 100644 --- a/mldsa/rounding.c +++ b/mldsa/rounding.c @@ -4,6 +4,7 @@ */ #include +#include "debug.h" #include "rounding.h" @@ -17,20 +18,20 @@ void mld_decompose(int32_t *a0, int32_t *a1, int32_t a) { *a1 = (a + 127) >> 7; /* We know a >= 0 and a < MLDSA_Q, so... */ - cassert(*a1 >= 0 && *a1 <= 65472); + mld_assert(*a1 >= 0 && *a1 <= 65472); #if MLDSA_MODE == 2 *a1 = (*a1 * 11275 + (1 << 23)) >> 24; - cassert(*a1 >= 0 && *a1 <= 44); + mld_assert(*a1 >= 0 && *a1 <= 44); *a1 ^= ((43 - *a1) >> 31) & *a1; - cassert(*a1 >= 0 && *a1 <= 43); + mld_assert(*a1 >= 0 && *a1 <= 43); #else /* MLDSA_MODE == 2 */ *a1 = (*a1 * 1025 + (1 << 21)) >> 22; - cassert(*a1 >= 0 && *a1 <= 16); + mld_assert(*a1 >= 0 && *a1 <= 16); *a1 &= 15; - cassert(*a1 >= 0 && *a1 <= 15); + mld_assert(*a1 >= 0 && *a1 <= 15); #endif /* MLDSA_MODE != 2 */ diff --git a/mldsa/sign.c b/mldsa/sign.c index 0e142c8f..9e3bb910 100644 --- a/mldsa/sign.c +++ b/mldsa/sign.c @@ -6,6 +6,7 @@ #include #include "cbmc.h" +#include "debug.h" #include "fips202/fips202.h" #include "packing.h" #include "poly.h" @@ -252,9 +253,7 @@ __contract__( /* If z is valid, then its coefficients are bounded by */ /* MLDSA_GAMMA1 - MLDSA_BETA. This will be needed below */ /* to prove the pre-condition of pack_sig() */ - cassert(forall(k1, 0, MLDSA_L, - array_abs_bound(z.vec[k1].coeffs, 0, MLDSA_N, - (MLDSA_GAMMA1 - MLDSA_BETA)))); + mld_assert_abs_bound_2d(z.vec, MLDSA_L, MLDSA_N, (MLDSA_GAMMA1 - MLDSA_BETA)); /* Check that subtracting cs2 does not change high bits of w and low bits * do not reveal secret information */ From 4b6feba8e503b871ffaaf3f9122d19fed2fbe625 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Wed, 23 Jul 2025 09:29:30 +0100 Subject: [PATCH 2/2] Remove unnecessary weak spec for mld_montgomery_reduce() mld_montgomery_reduce() so far had two CBMC specs with varying input/output bounds. However, it appears that the weak version is not necessary and can be removed. Signed-off-by: Hanno Becker --- mldsa/reduce.h | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/mldsa/reduce.h b/mldsa/reduce.h index a7acb78b..ee9a02d9 100644 --- a/mldsa/reduce.h +++ b/mldsa/reduce.h @@ -48,12 +48,8 @@ **************************************************/ int32_t mld_montgomery_reduce(int64_t a) __contract__( - requires(a >= -MONTGOMERY_REDUCE_DOMAIN_MAX && a <= MONTGOMERY_REDUCE_DOMAIN_MAX) - ensures(return_value >= INT32_MIN && return_value < REDUCE32_DOMAIN_MAX) - - /* Special case - for stronger input bounds, we can ensure stronger bounds on the output */ - ensures((a >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX && a < MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX) ==> - (return_value > -MLDSA_Q && return_value < MLDSA_Q)) + requires(a >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX && a < MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX) + ensures(return_value > -MLDSA_Q && return_value < MLDSA_Q) ); #define mld_reduce32 MLD_NAMESPACE(reduce32)