Skip to content

Verify memory usage: Re-use t1/w1 buffer #866

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mkannwischer merged 1 commit into from
Jan 12, 2026
+24 −15
Merged

Verify memory usage: Re-use t1/w1 buffer #866

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions mldsa/mldsa_native.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -839,13 +839,13 @@ int MLD_API_NAMESPACE(pk_from_sk)(
#else /* MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM */
#define MLD_TOTAL_ALLOC_44_KEYPAIR 36192
#define MLD_TOTAL_ALLOC_44_SIGN 32448
#define MLD_TOTAL_ALLOC_44_VERIFY 26560
#define MLD_TOTAL_ALLOC_44_VERIFY 22464
#define MLD_TOTAL_ALLOC_65_KEYPAIR 50048
#define MLD_TOTAL_ALLOC_65_SIGN 44768
#define MLD_TOTAL_ALLOC_65_VERIFY 36864
#define MLD_TOTAL_ALLOC_65_VERIFY 30720
#define MLD_TOTAL_ALLOC_87_KEYPAIR 66336
#define MLD_TOTAL_ALLOC_87_SIGN 59104
#define MLD_TOTAL_ALLOC_87_VERIFY 49408
#define MLD_TOTAL_ALLOC_87_VERIFY 41216
#endif /* !(MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM) */
/* check-magic: on */

Expand Down
33 changes: 21 additions & 12 deletions mldsa/src/sign.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -966,6 +966,18 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
int externalmu)
{
int ret, cmp;

/* TODO: Remove the following workaround for
* https://github.com/diffblue/cbmc/issues/8813 */
typedef MLK_UNION_OR_STRUCT
{
mld_polyveck t1;
mld_polyveck w1;
}
t1w1_u;
mld_polyveck *t1;
mld_polyveck *w1;

MLD_ALLOC(buf, uint8_t, (MLDSA_K * MLDSA_POLYW1_PACKEDBYTES));
MLD_ALLOC(rho, uint8_t, MLDSA_SEEDBYTES);
MLD_ALLOC(mu, uint8_t, MLDSA_CRHBYTES);
Expand All @@ -974,18 +986,19 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
MLD_ALLOC(cp, mld_poly, 1);
MLD_ALLOC(mat, mld_polymat, 1);
MLD_ALLOC(z, mld_polyvecl, 1);
MLD_ALLOC(t1, mld_polyveck, 1);
MLD_ALLOC(w1, mld_polyveck, 1);
MLD_ALLOC(t1w1, t1w1_u, 1);
MLD_ALLOC(tmp, mld_polyveck, 1);
MLD_ALLOC(h, mld_polyveck, 1);

if (buf == NULL || rho == NULL || mu == NULL || c == NULL || c2 == NULL ||
cp == NULL || mat == NULL || z == NULL || t1 == NULL || w1 == NULL ||
tmp == NULL || h == NULL)
cp == NULL || mat == NULL || z == NULL || t1w1 == NULL || tmp == NULL ||
h == NULL)
{
ret = MLD_ERR_OUT_OF_MEMORY;
goto cleanup;
}
t1 = &t1w1->t1;
w1 = &t1w1->w1;

if (siglen != MLDSA_CRYPTO_BYTES)
{
Expand Down Expand Up @@ -1028,17 +1041,14 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,

/* Matrix-vector multiplication; compute Az - c2^dt1 */
mld_poly_challenge(cp, c);
mld_polyvec_matrix_expand(mat, rho);

mld_polyvecl_ntt(z);
mld_polyvec_matrix_pointwise_montgomery(w1, mat, z);

mld_poly_ntt(cp);
mld_polyveck_shiftl(t1);
mld_polyveck_ntt(t1);

mld_polyveck_pointwise_poly_montgomery(tmp, cp, t1);

mld_polyvec_matrix_expand(mat, rho);
mld_polyvecl_ntt(z);
mld_polyvec_matrix_pointwise_montgomery(w1, mat, z);
mld_polyveck_sub(w1, tmp);
mld_polyveck_reduce(w1);
mld_polyveck_invntt_tomont(w1);
Expand All @@ -1062,8 +1072,7 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
/* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
MLD_FREE(h, mld_polyveck, 1);
MLD_FREE(tmp, mld_polyveck, 1);
MLD_FREE(w1, mld_polyveck, 1);
MLD_FREE(t1, mld_polyveck, 1);
MLD_FREE(t1w1, t1w1_u, 1);
MLD_FREE(z, mld_polyvecl, 1);
MLD_FREE(mat, mld_polymat, 1);
MLD_FREE(cp, mld_poly, 1);
Expand Down