Skip to content

Commit fa2a1b1

Browse files
mkannwischermkannwischer
committed
verify memory usage: Unpack hints h on the fly
This commit splits up the signature unpacking into two parts: unpack_sig_c_z and unpack_sig_h. This allows delaying unpacking of the hints h until later during the verification which in turn allows re-using the buffer used for the matrix. This cuts memory consumption by L KiB. - Hoisted out from #751 Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
1 parent 8933db9 commit fa2a1b1

File tree

11 files changed

+88
-88
lines changed

11 files changed

+88
-88
lines changed

‎mldsa/mldsa_native.S‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -257,7 +257,8 @@
257257
#undef mld_pack_sig_z
258258
#undef mld_pack_sk
259259
#undef mld_unpack_pk
260-
#undef mld_unpack_sig
260+
#undef mld_unpack_sig_c_z
261+
#undef mld_unpack_sig_h
261262
#undef mld_unpack_sk
262263
/* mldsa/src/params.h */
263264
#undef MLDSA_BETA

‎mldsa/mldsa_native.c‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -253,7 +253,8 @@
253253
#undef mld_pack_sig_z
254254
#undef mld_pack_sk
255255
#undef mld_unpack_pk
256-
#undef mld_unpack_sig
256+
#undef mld_unpack_sig_c_z
257+
#undef mld_unpack_sig_h
257258
#undef mld_unpack_sk
258259
/* mldsa/src/params.h */
259260
#undef MLDSA_BETA

‎mldsa/mldsa_native.h‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -928,15 +928,15 @@ int MLD_API_NAMESPACE(pk_from_sk)(
928928
#define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 32992
929929
#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 36192
930930
#define MLD_TOTAL_ALLOC_44_SIGN 32448
931-
#define MLD_TOTAL_ALLOC_44_VERIFY 22464
931+
#define MLD_TOTAL_ALLOC_44_VERIFY 18368
932932
#define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 46304
933933
#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 50048
934934
#define MLD_TOTAL_ALLOC_65_SIGN 44768
935-
#define MLD_TOTAL_ALLOC_65_VERIFY 30720
935+
#define MLD_TOTAL_ALLOC_65_VERIFY 25568
936936
#define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 62688
937937
#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 66336
938938
#define MLD_TOTAL_ALLOC_87_SIGN 59104
939-
#define MLD_TOTAL_ALLOC_87_VERIFY 41216
939+
#define MLD_TOTAL_ALLOC_87_VERIFY 34016
940940
#endif /* !(MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM) */
941941
/* check-magic: on */
942942

‎mldsa/src/packing.c‎

Lines changed: 6 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -9,13 +9,6 @@
99
#include "poly.h"
1010
#include "polyvec.h"
1111

12-
/* Parameter set namespacing
13-
* This is to facilitate building multiple instances
14-
* of mldsa-native (e.g. with varying parameter sets)
15-
* within a single compilation unit. */
16-
#define mld_unpack_hints MLD_ADD_PARAM_SET(mld_unpack_hints)
17-
/* End of parameter set namespacing */
18-
1912
MLD_INTERNAL_API
2013
void mld_pack_pk(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
2114
const uint8_t rho[MLDSA_SEEDBYTES], const mld_polyveck *t1)
@@ -177,33 +170,14 @@ void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi,
177170
mld_polyz_pack(sig, zi);
178171
}
179172

180-
/*************************************************
181-
* Name: mld_unpack_hints
182-
*
183-
* Description: Unpack raw hint bytes into a polyveck
184-
* struct
185-
*
186-
* Arguments: - mld_polyveck *h: pointer to output hint vector h
187-
* - const uint8_t packed_hints[MLDSA_POLYVECH_PACKEDBYTES]:
188-
* raw hint bytes
189-
*
190-
* Returns 1 in case of malformed hints; otherwise 0.
191-
**************************************************/
192-
static int mld_unpack_hints(
193-
mld_polyveck *h, const uint8_t packed_hints[MLDSA_POLYVECH_PACKEDBYTES])
194-
__contract__(
195-
requires(memory_no_alias(packed_hints, MLDSA_POLYVECH_PACKEDBYTES))
196-
requires(memory_no_alias(h, sizeof(mld_polyveck)))
197-
assigns(memory_slice(h, sizeof(mld_polyveck)))
198-
/* All returned coefficients are either 0 or 1 */
199-
ensures(forall(k1, 0, MLDSA_K,
200-
array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
201-
ensures(return_value >= 0 && return_value <= 1)
202-
)
173+
int mld_unpack_sig_h(mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES])
203174
{
204175
unsigned int i, j;
205176
unsigned int old_hint_count;
206177

178+
const uint8_t *packed_hints =
179+
sig + MLDSA_CTILDEBYTES + MLDSA_L * MLDSA_POLYZ_PACKEDBYTES;
180+
207181
/* Set all coefficients of all polynomials to 0. */
208182
/* Only those that are actually non-zero hints will */
209183
/* be overwritten below. */
@@ -269,18 +243,12 @@ __contract__(
269243
}
270244

271245
MLD_INTERNAL_API
272-
int mld_unpack_sig(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z,
273-
mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES])
246+
void mld_unpack_sig_c_z(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z,
247+
const uint8_t sig[MLDSA_CRYPTO_BYTES])
274248
{
275249
mld_memcpy(c, sig, MLDSA_CTILDEBYTES);
276250
sig += MLDSA_CTILDEBYTES;
277251

278252
mld_polyvecl_unpack_z(z, sig);
279253
sig += MLDSA_L * MLDSA_POLYZ_PACKEDBYTES;
280-
281-
return mld_unpack_hints(h, sig);
282254
}
283-
284-
/* To facilitate single-compilation-unit (SCU) builds, undefine all macros.
285-
* Don't modify by hand -- this is auto-generated by scripts/autogen. */
286-
#undef mld_unpack_hints

‎mldsa/src/packing.h‎

Lines changed: 33 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -190,36 +190,55 @@ __contract__(
190190
array_bound(s2->vec[k2].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1)))
191191
);
192192

193-
#define mld_unpack_sig MLD_NAMESPACE_KL(unpack_sig)
193+
#define mld_unpack_sig_h MLD_NAMESPACE_KL(unpack_sig_h)
194194
/*************************************************
195-
* Name: mld_unpack_sig
195+
* Name: mld_unpack_sig_h
196196
*
197-
* Description: Unpack signature sig = (c, z, h).
197+
* Description: Unpack h of signature sig = (c, z, h).
198+
* The (c, z) components unis packed separately using
199+
* mld_unpack_sig_c_z.
200+
*
201+
* Arguments: - mld_polyveck *h: pointer to output hint vector h
202+
* - const uint8_t packed_hints[MLDSA_POLYVECH_PACKEDBYTES]:
203+
* raw hint bytes
204+
*
205+
* Returns 1 in case of malformed hints; otherwise 0.
206+
**************************************************/
207+
MLD_INTERNAL_API
208+
MLD_MUST_CHECK_RETURN_VALUE
209+
int mld_unpack_sig_h(mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES])
210+
__contract__(
211+
requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
212+
requires(memory_no_alias(h, sizeof(mld_polyveck)))
213+
assigns(memory_slice(h, sizeof(mld_polyveck)))
214+
ensures(forall(k1, 0, MLDSA_K,
215+
array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
216+
ensures(return_value >= 0 && return_value <= 1)
217+
);
218+
219+
#define mld_unpack_sig_c_z MLD_NAMESPACE_KL(unpack_sig_c_z)
220+
/*************************************************
221+
* Name: mld_unpack_sig_c_z
222+
*
223+
* Description: Unpack (c, z) of signature sig = (c, z, h).
224+
* The h component unis packed separately using mld_pack_sig_z.
198225
*
199226
* Arguments: - uint8_t *c: pointer to output challenge hash
200-
* - mld_polyvecl *z: pointer to output vector z
201227
* - mld_polyveck *h: pointer to output hint vector h
202-
* - const uint8_t sig[]: byte array containing
228+
* - const uint8_t sig[MLDSA_CRYPTO_BYTES]: byte array containing
203229
* bit-packed signature
204230
*
205-
* Returns 1 in case of malformed signature; otherwise 0.
206231
**************************************************/
207232
MLD_INTERNAL_API
208-
MLD_MUST_CHECK_RETURN_VALUE
209-
int mld_unpack_sig(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z,
210-
mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES])
233+
void mld_unpack_sig_c_z(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z,
234+
const uint8_t sig[MLDSA_CRYPTO_BYTES])
211235
__contract__(
212236
requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
213237
requires(memory_no_alias(c, MLDSA_CTILDEBYTES))
214238
requires(memory_no_alias(z, sizeof(mld_polyvecl)))
215-
requires(memory_no_alias(h, sizeof(mld_polyveck)))
216239
assigns(memory_slice(c, MLDSA_CTILDEBYTES))
217240
assigns(memory_slice(z, sizeof(mld_polyvecl)))
218-
assigns(memory_slice(h, sizeof(mld_polyveck)))
219241
ensures(forall(k0, 0, MLDSA_L,
220242
array_bound(z->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)))
221-
ensures(forall(k1, 0, MLDSA_K,
222-
array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
223-
ensures(return_value >= 0 && return_value <= 1)
224243
);
225244
#endif /* !MLD_PACKING_H */

‎mldsa/src/sign.c‎

Lines changed: 26 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -993,27 +993,38 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
993993
mld_polyveck *t1;
994994
mld_polyveck *w1;
995995

996+
/* TODO: Remove the following workaround for
997+
* https://github.com/diffblue/cbmc/issues/8813 */
998+
typedef MLD_UNION_OR_STRUCT
999+
{
1000+
mld_polymat mat;
1001+
mld_polyveck h;
1002+
}
1003+
math_u;
1004+
mld_polymat *mat;
1005+
mld_polyveck *h;
1006+
9961007
MLD_ALLOC(buf, uint8_t, (MLDSA_K * MLDSA_POLYW1_PACKEDBYTES), context);
9971008
MLD_ALLOC(rho, uint8_t, MLDSA_SEEDBYTES, context);
9981009
MLD_ALLOC(mu, uint8_t, MLDSA_CRHBYTES, context);
9991010
MLD_ALLOC(c, uint8_t, MLDSA_CTILDEBYTES, context);
10001011
MLD_ALLOC(c2, uint8_t, MLDSA_CTILDEBYTES, context);
10011012
MLD_ALLOC(cp, mld_poly, 1, context);
1002-
MLD_ALLOC(mat, mld_polymat, 1, context);
1013+
MLD_ALLOC(math, math_u, 1, context);
10031014
MLD_ALLOC(z, mld_polyvecl, 1, context);
10041015
MLD_ALLOC(t1w1, t1w1_u, 1, context);
10051016
MLD_ALLOC(tmp, mld_polyveck, 1, context);
1006-
MLD_ALLOC(h, mld_polyveck, 1, context);
10071017

10081018
if (buf == NULL || rho == NULL || mu == NULL || c == NULL || c2 == NULL ||
1009-
cp == NULL || mat == NULL || z == NULL || t1w1 == NULL || tmp == NULL ||
1010-
h == NULL)
1019+
cp == NULL || math == NULL || z == NULL || t1w1 == NULL || tmp == NULL)
10111020
{
10121021
ret = MLD_ERR_OUT_OF_MEMORY;
10131022
goto cleanup;
10141023
}
10151024
t1 = &t1w1->t1;
10161025
w1 = &t1w1->w1;
1026+
mat = &math->mat;
1027+
h = &math->h;
10171028

10181029
if (siglen != MLDSA_CRYPTO_BYTES)
10191030
{
@@ -1023,14 +1034,10 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
10231034

10241035
mld_unpack_pk(rho, t1, pk);
10251036

1026-
/* mld_unpack_sig and mld_polyvecl_chknorm signal failure through a
1037+
mld_unpack_sig_c_z(c, z, sig);
1038+
/* mld_polyvecl_chknorm signals failure through a
10271039
* single non-zero error code that's not yet aligned with MLD_ERR_XXX.
10281040
* Map it to MLD_ERR_FAIL explicitly. */
1029-
if (mld_unpack_sig(c, z, h, sig))
1030-
{
1031-
ret = MLD_ERR_FAIL;
1032-
goto cleanup;
1033-
}
10341041
if (mld_polyvecl_chknorm(z, MLDSA_GAMMA1 - MLDSA_BETA))
10351042
{
10361043
ret = MLD_ERR_FAIL;
@@ -1070,6 +1077,14 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
10701077

10711078
/* Reconstruct w1 */
10721079
mld_polyveck_caddq(w1);
1080+
/* mld_unpack_sig_h signals failure through a
1081+
* single non-zero error code that's not yet aligned with MLD_ERR_XXX.
1082+
* Map it to MLD_ERR_FAIL explicitly. */
1083+
if (mld_unpack_sig_h(h, sig))
1084+
{
1085+
ret = MLD_ERR_FAIL;
1086+
goto cleanup;
1087+
}
10731088
mld_polyveck_use_hint(tmp, w1, h);
10741089
mld_polyveck_pack_w1(buf, tmp);
10751090
/* Call random oracle and verify challenge */
@@ -1085,11 +1100,10 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
10851100

10861101
cleanup:
10871102
/* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
1088-
MLD_FREE(h, mld_polyveck, 1, context);
10891103
MLD_FREE(tmp, mld_polyveck, 1, context);
10901104
MLD_FREE(t1w1, t1w1_u, 1, context);
10911105
MLD_FREE(z, mld_polyvecl, 1, context);
1092-
MLD_FREE(mat, mld_polymat, 1, context);
1106+
MLD_FREE(math, math_u, 1, context);
10931107
MLD_FREE(cp, mld_poly, 1, context);
10941108
MLD_FREE(c2, uint8_t, MLDSA_CTILDEBYTES, context);
10951109
MLD_FREE(c, uint8_t, MLDSA_CTILDEBYTES, context);

‎proofs/cbmc/sign_verify_internal/Makefile‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,8 @@ PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c
2121

2222
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_internal
2323
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)unpack_pk
24-
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)unpack_sig
24+
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)unpack_sig_c_z
25+
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)unpack_sig_h
2526
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvecl_chknorm
2627
USE_FUNCTION_CONTRACTS+=mld_H
2728
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)poly_challenge
@@ -46,8 +47,9 @@ USE_DYNAMIC_FRAMES=1
4647

4748
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
4849
EXTERNAL_SAT_SOLVER=
49-
CBMCFLAGS=--smt2
50+
CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3
5051
CBMCFLAGS += --slice-formula
52+
CBMCFLAGS += --no-array-field-sensitivity
5153

5254
FUNCTION_NAME = sign_verify_internal
5355

@@ -58,7 +60,7 @@ FUNCTION_NAME = sign_verify_internal
5860
# EXPENSIVE = true
5961

6062
# This function is large enough to need...
61-
CBMC_OBJECT_BITS = 10
63+
CBMC_OBJECT_BITS = 12
6264

6365
# If you require access to a file-local ("static") function or object to conduct
6466
# your proof, set the following (and do not include the original source file

proofs/cbmc/unpack_sig/Makefile renamed to proofs/cbmc/unpack_sig_c_z/Makefile

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,11 @@
44
include ../Makefile_params.common
55

66
HARNESS_ENTRY = harness
7-
HARNESS_FILE = unpack_sig_harness
7+
HARNESS_FILE = unpack_sig_c_z_harness
88

99
# This should be a unique identifier for this proof, and will appear on the
1010
# Litani dashboard. It can be human-readable and contain spaces if you wish.
11-
PROOF_UID = unpack_sig
11+
PROOF_UID = unpack_sig_c_z
1212

1313
DEFINES +=
1414
INCLUDES +=
@@ -18,8 +18,8 @@ REMOVE_FUNCTION_BODY +=
1818
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
1919
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c
2020

21-
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)unpack_sig
22-
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_unpack_z mld_unpack_hints
21+
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)unpack_sig_c_z
22+
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_unpack_z
2323
APPLY_LOOP_CONTRACTS=on
2424
USE_DYNAMIC_FRAMES=1
2525

@@ -28,7 +28,7 @@ EXTERNAL_SAT_SOLVER=
2828
CBMCFLAGS=--smt2
2929
CBMCFLAGS+=--slice-formula
3030

31-
FUNCTION_NAME = unpack_sig
31+
FUNCTION_NAME = unpack_sig_c_z
3232

3333
# If this proof is found to consume huge amounts of RAM, you can set the
3434
# EXPENSIVE variable. With new enough versions of the proof tools, this will

proofs/cbmc/unpack_sig/unpack_sig_harness.c renamed to proofs/cbmc/unpack_sig_c_z/unpack_sig_c_z_harness.c

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,6 @@ void harness(void)
88
{
99
uint8_t *c;
1010
uint8_t *sig;
11-
mld_polyveck *h;
1211
mld_polyvecl *z;
13-
int r;
14-
r = mld_unpack_sig(c, z, h, sig);
12+
mld_unpack_sig_c_z(c, z, sig);
1513
}

proofs/cbmc/unpack_hints/Makefile renamed to proofs/cbmc/unpack_sig_h/Makefile

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,11 @@
44
include ../Makefile_params.common
55

66
HARNESS_ENTRY = harness
7-
HARNESS_FILE = unpack_hints_harness
7+
HARNESS_FILE = unpack_sig_h_harness
88

99
# This should be a unique identifier for this proof, and will appear on the
1010
# Litani dashboard. It can be human-readable and contain spaces if you wish.
11-
PROOF_UID = unpack_hints
11+
PROOF_UID = unpack_sig_h
1212

1313
DEFINES +=
1414
INCLUDES +=
@@ -18,7 +18,7 @@ REMOVE_FUNCTION_BODY +=
1818
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
1919
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c
2020

21-
CHECK_FUNCTION_CONTRACTS=mld_unpack_hints
21+
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)unpack_sig_h
2222
USE_FUNCTION_CONTRACTS=
2323
APPLY_LOOP_CONTRACTS=on
2424
USE_DYNAMIC_FRAMES=1
@@ -28,7 +28,7 @@ EXTERNAL_SAT_SOLVER=
2828
CBMCFLAGS=--smt2
2929
CBMCFLAGS+=--slice-formula
3030

31-
FUNCTION_NAME = mld_unpack_hints
31+
FUNCTION_NAME = unpack_sig_h
3232

3333
# If this proof is found to consume huge amounts of RAM, you can set the
3434
# EXPENSIVE variable. With new enough versions of the proof tools, this will

0 commit comments

Comments
 (0)