From 7adc7e8ffb80502bbaf5b8345d96845da0abf13c Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Sat, 2 Nov 2024 05:20:40 +0000 Subject: [PATCH] CBMC: Add spec + proof for polyvec_basemul_acc_montgomery_cached The proof is less trivial than the ones before since one has to use the output bounds of the lower level functions to show that the accumulation loop does not overflow. Signed-off-by: Hanno Becker --- .../Makefile | 54 +++++++++++++++++++ .../cbmc-proof.txt | 3 ++ ...ec_basemul_acc_montgomery_cached_harness.c | 30 +++++++++++ mlkem/polyvec.c | 33 +++++++++--- mlkem/polyvec.h | 30 ++++++++++- 5 files changed, 141 insertions(+), 9 deletions(-) create mode 100644 cbmc/proofs/polyvec_basemul_acc_montgomery_cached/Makefile create mode 100644 cbmc/proofs/polyvec_basemul_acc_montgomery_cached/cbmc-proof.txt create mode 100644 cbmc/proofs/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c diff --git a/cbmc/proofs/polyvec_basemul_acc_montgomery_cached/Makefile b/cbmc/proofs/polyvec_basemul_acc_montgomery_cached/Makefile new file mode 100644 index 000000000..a0e9205a1 --- /dev/null +++ b/cbmc/proofs/polyvec_basemul_acc_montgomery_cached/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = polyvec_basemul_acc_montgomery_cached_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = polyvec_basemul_acc_montgomery_cached + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += $(MLKEM_NAMESPACE)polyvec_basemul_acc_montgomery_cached.0:4 # Largest value of MLKEM_K + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_basemul_acc_montgomery_cached +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_basemul_montgomery_cached $(MLKEM_NAMESPACE)poly_add +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = polyvec_basemul_acc_montgomery_cached + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/cbmc/proofs/polyvec_basemul_acc_montgomery_cached/cbmc-proof.txt b/cbmc/proofs/polyvec_basemul_acc_montgomery_cached/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/polyvec_basemul_acc_montgomery_cached/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/cbmc/proofs/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c b/cbmc/proofs/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c new file mode 100644 index 000000000..fe09ea509 --- /dev/null +++ b/cbmc/proofs/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c @@ -0,0 +1,30 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +/* + * Insert copyright notice + */ + +/** + * @file polyvec_basemul_acc_montgomery_cached_harness.c + * @brief Implements the proof harness for basemul_cached function. + */ +#include "polyvec.h" + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) { + poly r; + polyvec a, b; + polyvec_mulcache b_cached; + + polyvec_basemul_acc_montgomery_cached(&r, &a, &b, &b_cached); +} diff --git a/mlkem/polyvec.c b/mlkem/polyvec.c index dd2eaa0b6..bc0d77093 100644 --- a/mlkem/polyvec.c +++ b/mlkem/polyvec.c @@ -226,18 +226,35 @@ void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a, POLYVEC_BOUND(b, NTT_BOUND); POLYVEC_BOUND(b_cache, MLKEM_Q); - unsigned int i; + int i; poly t; poly_basemul_montgomery_cached(r, &a->vec[0], &b->vec[0], &b_cache->vec[0]); - for (i = 1; i < MLKEM_K; i++) { - poly_basemul_montgomery_cached(&t, &a->vec[i], &b->vec[i], - &b_cache->vec[i]); - poly_add(r, r, &t); - // abs bounds: < (i+1) * 3/2 * q - } - // abs bounds: < MLKEM_K * 3/2 * q <= 4 * 3/2 * q = 19974 + for (i = 1; i < MLKEM_K; i++) + // clang-format off + ASSIGNS(i, t, OBJECT_WHOLE(r)) + INVARIANT(i >= 1 && i <= MLKEM_K) + INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, \ + i * (-3 * HALF_Q + 1), i * (3 * HALF_Q - 1))) + DECREASES(MLKEM_K - i) + // clang-format on + { + poly_basemul_montgomery_cached(&t, &a->vec[i], &b->vec[i], + &b_cache->vec[i]); + poly_add(r, r, &t); + // abs bounds: < (i+1) * 3/2 * q + } + + // Those bounds are true for the C implementation, but not needed + // in the higher level bounds reasoning. It is thus best to omit + // them from the spec to not unnecessarily constraint native implementations. + ASSERT( + ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, + MLKEM_K * (-3 * HALF_Q + 1), MLKEM_K * (3 * HALF_Q - 1)), + "polyvec_basemul_acc_montgomery_cached output bounds"); + // TODO: Integrate CBMC assertin into POLY_BOUND if CBMC is set + POLY_BOUND(r, MLKEM_K * 3 * HALF_Q); } #else /* !MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED */ void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a, diff --git a/mlkem/polyvec.h b/mlkem/polyvec.h index cde038e9d..21112e358 100644 --- a/mlkem/polyvec.h +++ b/mlkem/polyvec.h @@ -40,9 +40,37 @@ void polyvec_basemul_acc_montgomery(poly *r, const polyvec *a, // REF-CHANGE: This function does not exist in the reference implementation #define polyvec_basemul_acc_montgomery_cached \ MLKEM_NAMESPACE(polyvec_basemul_acc_montgomery_cached) +/************************************************* + * Name: polyvec_basemul_acc_montgomery_cached + * + * Description: Scalar product of two vectors of polynomials in NTT domain, + * using mulcache for second operand. + * + * Bounds: + * - a is assumed to be coefficient-wise < q in absolute value. + * - No bounds guarantees for the coefficients in the result. + * + * Arguments: - poly *r: pointer to output polynomial + * - const polyvec *a: pointer to first input polynomial vector + * - const polyvec *b: pointer to second input polynomial vector + * - const polyvec_mulcache *b_cache: pointer to mulcache + * for second input polynomial vector. Can be computed + * via polyvec_mulcache_compute(). + **************************************************/ void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a, const polyvec *b, - const polyvec_mulcache *b_cache); + const polyvec_mulcache *b_cache) + // clang-format off +REQUIRES(r != NULL && a != NULL && b != NULL && b_cache != NULL) +REQUIRES(IS_FRESH(r, sizeof(poly))) +REQUIRES(IS_FRESH(a, sizeof(polyvec)) && IS_FRESH(b, sizeof(polyvec))) +REQUIRES(IS_FRESH(b_cache, sizeof(polyvec_mulcache))) +// Input is coefficient-wise < q in absolute value +REQUIRES(FORALL(int, k1, 0, MLKEM_K - 1, \ + ARRAY_IN_BOUNDS(int, k2, 0, MLKEM_N - 1, \ + a->vec[k1].coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))) +ASSIGNS(OBJECT_WHOLE(r)); +// clang-format on // REF-CHANGE: This function does not exist in the reference implementation #define polyvec_mulcache_compute MLKEM_NAMESPACE(polyvec_mulcache_compute)