Skip to content

Commit 2463e18

Browse files
rod-chapmanrod-chapman
committed
Further proof stabilization.
1. Weaken the contract of mld_polyveck_add(). This is sufficient to prove the caller in mld_attempt_signature_generation() 2. Introduce a new mld_polyveck_add_error() with stronger contracts where the second argument is an error term where all coefficients are bounded in absolute value to MLDSA_ETA. The post-condition of this function is just right to prove the calling code in crypto_sign_keypair_internal() which relies on these stronger bounds. 3. Add proof artefacts as appropriate. Signed-off-by: Rod Chapman <[email protected]>
1 parent e264496 commit 2463e18

File tree

6 files changed

+112
-6
lines changed

6 files changed

+112
-6
lines changed

‎mldsa/polyvec.c‎

Lines changed: 22 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -509,7 +509,6 @@ void mld_polyveck_add(mld_polyveck *u, const mld_polyveck *v)
509509
invariant(i <= MLDSA_K)
510510
invariant(forall(k0, i, MLDSA_K,
511511
forall(k1, 0, MLDSA_N, u->vec[k0].coeffs[k1] == loop_entry(*u).vec[k0].coeffs[k1])))
512-
invariant(forall(k4, 0, i, forall(k5, 0, MLDSA_N, u->vec[k4].coeffs[k5] == loop_entry(*u).vec[k4].coeffs[k5] + v->vec[k4].coeffs[k5])))
513512
invariant(forall(k6, 0, i, array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
514513
)
515514
{
@@ -518,6 +517,28 @@ void mld_polyveck_add(mld_polyveck *u, const mld_polyveck *v)
518517
mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX);
519518
}
520519

520+
/* Reference: We use destructive version (output=first input) to avoid
521+
* reasoning about aliasing in the CBMC specification */
522+
MLD_INTERNAL_API
523+
void mld_polyveck_add_error(mld_polyveck *u, const mld_polyveck *v)
524+
{
525+
unsigned int i;
526+
527+
for (i = 0; i < MLDSA_K; ++i)
528+
__loop__(
529+
assigns(i, memory_slice(u, sizeof(mld_polyveck)))
530+
invariant(i <= MLDSA_K)
531+
invariant(forall(k0, i, MLDSA_K,
532+
forall(k1, 0, MLDSA_N, u->vec[k0].coeffs[k1] == loop_entry(*u).vec[k0].coeffs[k1])))
533+
invariant(forall(k6, 0, i, array_abs_bound(u->vec[k6].coeffs, 0, MLDSA_N, MLDSA_Q)))
534+
)
535+
{
536+
mld_poly_add(&u->vec[i], &v->vec[i]);
537+
}
538+
mld_assert_abs_bound_2d(u->vec, MLDSA_L, MLDSA_N, MLDSA_Q);
539+
}
540+
541+
521542
MLD_INTERNAL_API
522543
void mld_polyveck_sub(mld_polyveck *u, const mld_polyveck *v)
523544
{

‎mldsa/polyvec.h‎

Lines changed: 23 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -284,9 +284,29 @@ __contract__(
284284
requires(forall(k0, 0, MLDSA_K, forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] < REDUCE32_DOMAIN_MAX)))
285285
requires(forall(k2, 0, MLDSA_K, forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] >= INT32_MIN)))
286286
assigns(object_whole(u))
287-
ensures(forall(k4, 0, MLDSA_K, forall(k5, 0, MLDSA_N, u->vec[k4].coeffs[k5] == old(*u).vec[k4].coeffs[k5] + v->vec[k4].coeffs[k5])))
288-
ensures(forall(k6, 0, MLDSA_L,
289-
array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
287+
ensures(forall(k6, 0, MLDSA_K, array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
288+
);
289+
290+
#define mld_polyveck_add_error MLD_NAMESPACE_KL(polyveck_add_error)
291+
/*************************************************
292+
* Name: mld_polyveck_add_error
293+
*
294+
* Description: As mld_polyveck_add(), but special
295+
* case (and stronger contracts) when
296+
* input vector v is an error term
297+
* where all coefficients are bounded
298+
* in absolute value by MLDSA_ETA.
299+
**************************************************/
300+
MLD_INTERNAL_API
301+
void mld_polyveck_add_error(mld_polyveck *u, const mld_polyveck *v)
302+
__contract__(
303+
requires(memory_no_alias(u, sizeof(mld_polyveck)))
304+
requires(memory_no_alias(v, sizeof(mld_polyveck)))
305+
requires(forall(k0, 0, MLDSA_K, forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] < MLDSA_Q)))
306+
requires(forall(k2, 0, MLDSA_K, forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] > -MLDSA_Q)))
307+
requires(forall(k4, 0, MLDSA_K, array_abs_bound(v->vec[k4].coeffs, 0, MLDSA_N, MLDSA_ETA + 1)))
308+
assigns(object_whole(u))
309+
ensures(forall(k6, 0, MLDSA_K, array_abs_bound(u->vec[k6].coeffs, 0, MLDSA_N, MLDSA_Q)))
290310
);
291311

292312
#define mld_polyveck_sub MLD_NAMESPACE_KL(polyveck_sub)

‎mldsa/sign.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -197,7 +197,7 @@ int crypto_sign_keypair_internal(uint8_t *pk, uint8_t *sk,
197197
mld_polyveck_invntt_tomont(&t1);
198198

199199
/* Add error vector s2 */
200-
mld_polyveck_add(&t1, &s2);
200+
mld_polyveck_add_error(&t1, &s2);
201201

202202
/* Extract t1 and write public key */
203203
mld_polyveck_caddq(&t1);

‎proofs/cbmc/crypto_sign_keypair_internal/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvecl_ntt
2727
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_pointwise_montgomery
2828
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_reduce
2929
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_invntt_tomont
30-
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_add
30+
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_add_error
3131
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_caddq
3232
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_power2round
3333
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)pack_pk

‎proofs/cbmc/polyveck_add_error/Makefile‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
# Copyright (c) The mldsa-native project authors
2+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
include ../Makefile_params.common
5+
6+
HARNESS_ENTRY = harness
7+
HARNESS_FILE = polyveck_add_error_harness
8+
9+
# This should be a unique identifier for this proof, and will appear on the
10+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
11+
PROOF_UID = polyveck_add_error
12+
13+
DEFINES +=
14+
INCLUDES +=
15+
16+
REMOVE_FUNCTION_BODY +=
17+
UNWINDSET +=
18+
19+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
20+
PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c
21+
22+
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_add_error
23+
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_add
24+
APPLY_LOOP_CONTRACTS=on
25+
USE_DYNAMIC_FRAMES=1
26+
27+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
28+
EXTERNAL_SAT_SOLVER=
29+
CBMCFLAGS=--smt2 --arrays-uf-always --slice-formula
30+
31+
FUNCTION_NAME = polyveck_add_error
32+
33+
# If this proof is found to consume huge amounts of RAM, you can set the
34+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
35+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
36+
# documentation in Makefile.common under the "Job Pools" heading for details.
37+
# EXPENSIVE = true
38+
39+
# This function is large enough to need...
40+
CBMC_OBJECT_BITS = 8
41+
42+
# If you require access to a file-local ("static") function or object to conduct
43+
# your proof, set the following (and do not include the original source file
44+
# ("mldsa/poly.c") in PROJECT_SOURCES).
45+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
46+
# include ../Makefile.common
47+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c
48+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
49+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
50+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
51+
# be set before including Makefile.common, but any use of variables on the
52+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
53+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
54+
55+
include ../Makefile.common

‎proofs/cbmc/polyveck_add_error/polyveck_add_error_harness.c‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include "polyvec.h"
5+
6+
void harness(void)
7+
{
8+
mld_polyveck *r, *b;
9+
mld_polyveck_add_error(r, b);
10+
}

0 commit comments

Comments
 (0)