diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index c52d345d9..f8b361089 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -268,7 +268,7 @@ static MLD_INLINE int mld_poly_decompose_32_native(int32_t *a1, int32_t *a0, __contract__( requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(a0 == a || memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) @@ -302,7 +302,7 @@ static MLD_INLINE int mld_poly_decompose_88_native(int32_t *a1, int32_t *a0, __contract__( requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(a0 == a || memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c index 1e1a5bf38..dc5ae8ff3 100644 --- a/mldsa/src/poly_kl.c +++ b/mldsa/src/poly_kl.c @@ -44,7 +44,7 @@ MLD_STATIC_TESTABLE void mld_poly_decompose_c(mld_poly *a1, mld_poly *a0, __contract__( requires(memory_no_alias(a1, sizeof(mld_poly))) requires(memory_no_alias(a0, sizeof(mld_poly))) - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(a0 == a || memory_no_alias(a, sizeof(mld_poly))) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) assigns(memory_slice(a1, sizeof(mld_poly))) assigns(memory_slice(a0, sizeof(mld_poly))) @@ -60,6 +60,8 @@ __contract__( invariant(i <= MLDSA_N) invariant(array_bound(a1->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) invariant(array_abs_bound(a0->coeffs, 0, i, MLDSA_GAMMA2+1)) + invariant(forall(k1, i, MLDSA_N, + a->coeffs[k1] == loop_entry(*a).coeffs[k1])) ) { mld_decompose(&a0->coeffs[i], &a1->coeffs[i], a->coeffs[i]); diff --git a/mldsa/src/poly_kl.h b/mldsa/src/poly_kl.h index 23c525efe..caf56bfe6 100644 --- a/mldsa/src/poly_kl.h +++ b/mldsa/src/poly_kl.h @@ -31,7 +31,7 @@ void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a) __contract__( requires(memory_no_alias(a1, sizeof(mld_poly))) requires(memory_no_alias(a0, sizeof(mld_poly))) - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(a0 == a || memory_no_alias(a, sizeof(mld_poly))) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) assigns(memory_slice(a1, sizeof(mld_poly))) assigns(memory_slice(a0, sizeof(mld_poly))) diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c index 13f052337..4d0c38b30 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -681,6 +681,8 @@ void mld_polyveck_decompose(mld_polyveck *v1, mld_polyveck *v0, array_bound(v1->vec[k1].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))) invariant(forall(k2, 0, i, array_abs_bound(v0->vec[k2].coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1))) + invariant(forall(k0, i, MLDSA_K, forall(k1, 0, MLDSA_N, + v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1]))) ) { mld_poly_decompose(&v1->vec[i], &v0->vec[i], &v->vec[i]); diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h index bb1ed8fba..a522432ec 100644 --- a/mldsa/src/polyvec.h +++ b/mldsa/src/polyvec.h @@ -484,7 +484,7 @@ void mld_polyveck_decompose(mld_polyveck *v1, mld_polyveck *v0, __contract__( requires(memory_no_alias(v1, sizeof(mld_polyveck))) requires(memory_no_alias(v0, sizeof(mld_polyveck))) - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(v0 == v || memory_no_alias(v, sizeof(mld_polyveck))) requires(forall(k0, 0, MLDSA_K, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) assigns(memory_slice(v1, sizeof(mld_polyveck))) diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c index 87d5f58ac..033a3f91a 100644 --- a/mldsa/src/sign.c +++ b/mldsa/src/sign.c @@ -447,7 +447,15 @@ __contract__( MLD_ALIGN uint8_t challenge_bytes[MLDSA_CTILDEBYTES]; unsigned int n; mld_polyvecl y, z; - mld_polyveck w, w1, w0, h; + mld_polyveck w1, h; + union + { + mld_polyveck w; + mld_polyveck w0; + } ww0; + mld_polyveck *w = &ww0.w; + mld_polyveck *w0 = &ww0.w0; + mld_poly cp; uint32_t z_invalid, w0_invalid, h_invalid; int res; @@ -458,13 +466,13 @@ __contract__( /* Matrix-vector multiplication */ z = y; mld_polyvecl_ntt(&z); - mld_polyvec_matrix_pointwise_montgomery(&w, mat, &z); - mld_polyveck_reduce(&w); - mld_polyveck_invntt_tomont(&w); + mld_polyvec_matrix_pointwise_montgomery(w, mat, &z); + mld_polyveck_reduce(w); + mld_polyveck_invntt_tomont(w); /* Decompose w and call the random oracle */ - mld_polyveck_caddq(&w); - mld_polyveck_decompose(&w1, &w0, &w); + mld_polyveck_caddq(w); + mld_polyveck_decompose(&w1, w0, w); mld_polyveck_pack_w1(sig, &w1); mld_H(challenge_bytes, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, sig, @@ -505,10 +513,10 @@ __contract__( * do not reveal secret information */ mld_polyveck_pointwise_poly_montgomery(&h, &cp, s2); mld_polyveck_invntt_tomont(&h); - mld_polyveck_sub(&w0, &h); - mld_polyveck_reduce(&w0); + mld_polyveck_sub(w0, &h); + mld_polyveck_reduce(w0); - w0_invalid = mld_polyveck_chknorm(&w0, MLDSA_GAMMA2 - MLDSA_BETA); + w0_invalid = mld_polyveck_chknorm(w0, MLDSA_GAMMA2 - MLDSA_BETA); /* Constant time: w0_invalid may be leaked - see comment for z_invalid. */ MLD_CT_TESTING_DECLASSIFY(&w0_invalid, sizeof(uint32_t)); if (w0_invalid) @@ -531,7 +539,7 @@ __contract__( goto cleanup; } - mld_polyveck_add(&w0, &h); + mld_polyveck_add(w0, &h); /* Constant time: At this point all norm checks have passed and we, hence, * know that the signature does not leak any secret information. @@ -541,9 +549,9 @@ __contract__( * h=c*t0 is public as both c and t0 are public. * For a more detailed discussion, refer to https://eprint.iacr.org/2022/1406. */ - MLD_CT_TESTING_DECLASSIFY(&w0, sizeof(w0)); + MLD_CT_TESTING_DECLASSIFY(w0, sizeof(mld_polyveck)); MLD_CT_TESTING_DECLASSIFY(&w1, sizeof(w1)); - n = mld_polyveck_make_hint(&h, &w0, &w1); + n = mld_polyveck_make_hint(&h, w0, &w1); if (n > MLDSA_OMEGA) { res = -1; /* reject */ @@ -564,9 +572,8 @@ __contract__( mld_zeroize(challenge_bytes, MLDSA_CTILDEBYTES); mld_zeroize(&y, sizeof(y)); mld_zeroize(&z, sizeof(z)); - mld_zeroize(&w, sizeof(w)); mld_zeroize(&w1, sizeof(w1)); - mld_zeroize(&w0, sizeof(w0)); + mld_zeroize(&ww0, sizeof(ww0)); mld_zeroize(&h, sizeof(h)); mld_zeroize(&cp, sizeof(cp));