Skip to content

Commit 1186576

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 95e6ed3 commit 1186576

File tree

6 files changed

+112
-6
lines changed

6 files changed

+112
-6
lines changed

‎mldsa/src/polyvec.c‎

Lines changed: 22 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -510,7 +510,6 @@ void mld_polyveck_add(mld_polyveck *u, const mld_polyveck *v)
510510
invariant(i <= MLDSA_K)
511511
invariant(forall(k0, i, MLDSA_K,
512512
forall(k1, 0, MLDSA_N, u->vec[k0].coeffs[k1] == loop_entry(*u).vec[k0].coeffs[k1])))
513-
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])))
514513
invariant(forall(k6, 0, i, array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
515514
)
516515
{
@@ -519,6 +518,28 @@ void mld_polyveck_add(mld_polyveck *u, const mld_polyveck *v)
519518
mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX);
520519
}
521520

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

‎mldsa/src/polyvec.h‎

Lines changed: 23 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -290,9 +290,29 @@ __contract__(
290290
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)))
291291
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)))
292292
assigns(object_whole(u))
293-
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])))
294-
ensures(forall(k6, 0, MLDSA_L,
295-
array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
293+
ensures(forall(k6, 0, MLDSA_K, array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
294+
);
295+
296+
#define mld_polyveck_add_error MLD_NAMESPACE_KL(polyveck_add_error)
297+
/*************************************************
298+
* Name: mld_polyveck_add_error
299+
*
300+
* Description: As mld_polyveck_add(), but special
301+
* case (and stronger contracts) when
302+
* input vector v is an error term
303+
* where all coefficients are bounded
304+
* in absolute value by MLDSA_ETA.
305+
**************************************************/
306+
MLD_INTERNAL_API
307+
void mld_polyveck_add_error(mld_polyveck *u, const mld_polyveck *v)
308+
__contract__(
309+
requires(memory_no_alias(u, sizeof(mld_polyveck)))
310+
requires(memory_no_alias(v, sizeof(mld_polyveck)))
311+
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)))
312+
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)))
313+
requires(forall(k4, 0, MLDSA_K, array_abs_bound(v->vec[k4].coeffs, 0, MLDSA_N, MLDSA_ETA + 1)))
314+
assigns(object_whole(u))
315+
ensures(forall(k6, 0, MLDSA_K, array_abs_bound(u->vec[k6].coeffs, 0, MLDSA_N, MLDSA_Q)))
296316
);
297317

298318
#define mld_polyveck_sub MLD_NAMESPACE_KL(polyveck_sub)

‎mldsa/src/sign.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -210,7 +210,7 @@ int crypto_sign_keypair_internal(uint8_t pk[CRYPTO_PUBLICKEYBYTES],
210210
mld_polyveck_invntt_tomont(&t1);
211211

212212
/* Add error vector s2 */
213-
mld_polyveck_add(&t1, &s2);
213+
mld_polyveck_add_error(&t1, &s2);
214214

215215
/* Extract t1 and write public key */
216216
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)