From 738454a5b4141275de989b6a0a6924c60e35d69a Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Tue, 5 Nov 2024 05:33:40 +0000 Subject: [PATCH] CBMC: Add specs+proofs for pack_pk, unpack_pk, polyvec_reduce Resolves #334 Resolves #331 Resolves #333 Signed-off-by: Hanno Becker --- cbmc/proofs/pack_pk/Makefile | 54 +++++++++++++++++++ cbmc/proofs/pack_pk/cbmc-proof.txt | 3 ++ cbmc/proofs/pack_pk/pack_pk_harness.c | 19 +++++++ cbmc/proofs/polyvec_reduce/Makefile | 54 +++++++++++++++++++ cbmc/proofs/polyvec_reduce/cbmc-proof.txt | 3 ++ .../polyvec_reduce/polyvec_reduce_harness.c | 27 ++++++++++ cbmc/proofs/unpack_pk/Makefile | 54 +++++++++++++++++++ cbmc/proofs/unpack_pk/cbmc-proof.txt | 3 ++ cbmc/proofs/unpack_pk/unpack_pk_harness.c | 19 +++++++ mlkem/cbmc.h | 5 ++ mlkem/indcpa.c | 34 +++++++++--- mlkem/poly.h | 2 +- mlkem/polyvec.h | 21 +++++++- 13 files changed, 290 insertions(+), 8 deletions(-) create mode 100644 cbmc/proofs/pack_pk/Makefile create mode 100644 cbmc/proofs/pack_pk/cbmc-proof.txt create mode 100644 cbmc/proofs/pack_pk/pack_pk_harness.c create mode 100644 cbmc/proofs/polyvec_reduce/Makefile create mode 100644 cbmc/proofs/polyvec_reduce/cbmc-proof.txt create mode 100644 cbmc/proofs/polyvec_reduce/polyvec_reduce_harness.c create mode 100644 cbmc/proofs/unpack_pk/Makefile create mode 100644 cbmc/proofs/unpack_pk/cbmc-proof.txt create mode 100644 cbmc/proofs/unpack_pk/unpack_pk_harness.c diff --git a/cbmc/proofs/pack_pk/Makefile b/cbmc/proofs/pack_pk/Makefile new file mode 100644 index 000000000..93457538e --- /dev/null +++ b/cbmc/proofs/pack_pk/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = pack_pk_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 = pack_pk + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c + +CHECK_FUNCTION_CONTRACTS=pack_pk +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_tobytes +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 = pack_pk + +# 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/pack_pk/cbmc-proof.txt b/cbmc/proofs/pack_pk/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/pack_pk/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/pack_pk/pack_pk_harness.c b/cbmc/proofs/pack_pk/pack_pk_harness.c new file mode 100644 index 000000000..81ee05d7e --- /dev/null +++ b/cbmc/proofs/pack_pk/pack_pk_harness.c @@ -0,0 +1,19 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +#include +#include "polyvec.h" + +void pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], polyvec *pk, + const uint8_t seed[MLKEM_SYMBYTES]); + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) { + polyvec *pk; + uint8_t *r, *seed; + + pack_pk(r, pk, seed); +} diff --git a/cbmc/proofs/polyvec_reduce/Makefile b/cbmc/proofs/polyvec_reduce/Makefile new file mode 100644 index 000000000..07b3aeb08 --- /dev/null +++ b/cbmc/proofs/polyvec_reduce/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = polyvec_reduce_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_reduce + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += $(MLKEM_NAMESPACE)polyvec_reduce.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_reduce +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_reduce +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 = $(MLKEM_NAMESPACE)polyvec_reduce + +# 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_reduce/cbmc-proof.txt b/cbmc/proofs/polyvec_reduce/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/polyvec_reduce/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_reduce/polyvec_reduce_harness.c b/cbmc/proofs/polyvec_reduce/polyvec_reduce_harness.c new file mode 100644 index 000000000..d830519b5 --- /dev/null +++ b/cbmc/proofs/polyvec_reduce/polyvec_reduce_harness.c @@ -0,0 +1,27 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +/* + * Insert copyright notice + */ + +/** + * @file polyvec_reduce_harness.c + * @brief Implements the proof harness for polyvec_reduce function. + */ + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ +#include + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) { + polyvec *a; + polyvec_reduce(a); +} diff --git a/cbmc/proofs/unpack_pk/Makefile b/cbmc/proofs/unpack_pk/Makefile new file mode 100644 index 000000000..f17981c9d --- /dev/null +++ b/cbmc/proofs/unpack_pk/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = unpack_pk_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 = unpack_pk + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c + +CHECK_FUNCTION_CONTRACTS=unpack_pk +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_frombytes $(MLKEM_NAMESPACE)polyvec_reduce +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 = unpack_pk + +# 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/unpack_pk/cbmc-proof.txt b/cbmc/proofs/unpack_pk/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/unpack_pk/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/unpack_pk/unpack_pk_harness.c b/cbmc/proofs/unpack_pk/unpack_pk_harness.c new file mode 100644 index 000000000..fe779665d --- /dev/null +++ b/cbmc/proofs/unpack_pk/unpack_pk_harness.c @@ -0,0 +1,19 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +#include +#include "polyvec.h" + +void unpack_pk(polyvec *pk, uint8_t seed[MLKEM_SYMBYTES], + const uint8_t packedpk[MLKEM_INDCPA_PUBLICKEYBYTES]); + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) { + polyvec *pk; + uint8_t *packedpk, *seed; + + unpack_pk(pk, seed, packedpk); +} diff --git a/mlkem/cbmc.h b/mlkem/cbmc.h index ddca57050..cd8ee7308 100644 --- a/mlkem/cbmc.h +++ b/mlkem/cbmc.h @@ -6,6 +6,8 @@ #ifndef CBMC +#define STATIC_TESTABLE static + // CBMC top-level contracts are replaced by "" for compilation #define ASSIGNS(...) #define REQUIRES(...) @@ -17,6 +19,9 @@ #else // CBMC _is_ defined, therefore we're doing proof +// expose certain procedures to CBMC proofs that are static otherwise +#define STATIC_TESTABLE + // https://diffblue.github.io/cbmc/contracts-assigns.html #define ASSIGNS(...) __CPROVER_assigns(__VA_ARGS__) diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c index 0d9190c33..5bedd3724 100644 --- a/mlkem/indcpa.c +++ b/mlkem/indcpa.c @@ -17,6 +17,8 @@ #include "arith_native.h" #include "debug/debug.h" +#include "cbmc.h" + /************************************************* * Name: pack_pk * @@ -25,11 +27,20 @@ * and the public seed used to generate the matrix A. * * Arguments: uint8_t *r: pointer to the output serialized public key - * polyvec *pk: pointer to the input public-key polyvec + * polyvec *pk: pointer to the input public-key polyvec. + * Must have coefficients within [0,..,q-1]. * const uint8_t *seed: pointer to the input public seed **************************************************/ -static void pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], polyvec *pk, - const uint8_t seed[MLKEM_SYMBYTES]) { +STATIC_TESTABLE +void pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], polyvec *pk, + const uint8_t seed[MLKEM_SYMBYTES]) // clang-format off +REQUIRES(IS_FRESH(r, MLKEM_INDCPA_PUBLICKEYBYTES)) +REQUIRES(IS_FRESH(pk, sizeof(polyvec))) +REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES)) +REQUIRES(FORALL(int, k0, 0, MLKEM_K - 1, + ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, MLKEM_Q - 1))) +ASSIGNS(OBJECT_WHOLE(r)) // clang-format on +{ POLYVEC_BOUND(pk, MLKEM_Q); polyvec_tobytes(r, pk); memcpy(r + MLKEM_POLYVECBYTES, seed, MLKEM_SYMBYTES); @@ -42,12 +53,23 @@ static void pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], polyvec *pk, * approximate inverse of pack_pk * * Arguments: - polyvec *pk: pointer to output public-key polynomial vector + * Coefficients will be normalized to [0,..,q-1]. * - uint8_t *seed: pointer to output seed to generate matrix A * - const uint8_t *packedpk: pointer to input serialized public - *key + * key. **************************************************/ -static void unpack_pk(polyvec *pk, uint8_t seed[MLKEM_SYMBYTES], - const uint8_t packedpk[MLKEM_INDCPA_PUBLICKEYBYTES]) { +STATIC_TESTABLE +void unpack_pk( + polyvec *pk, uint8_t seed[MLKEM_SYMBYTES], + const uint8_t packedpk[MLKEM_INDCPA_PUBLICKEYBYTES]) // clang-format off +REQUIRES(IS_FRESH(packedpk, MLKEM_INDCPA_PUBLICKEYBYTES)) +REQUIRES(IS_FRESH(pk, sizeof(polyvec))) +REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES)) +ENSURES(FORALL(int, k0, 0, MLKEM_K - 1, + ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, MLKEM_Q - 1))) +ASSIGNS(OBJECT_WHOLE(pk)) +ASSIGNS(OBJECT_WHOLE(seed)) // clang-format on +{ polyvec_frombytes(pk, packedpk); memcpy(seed, packedpk + MLKEM_POLYVECBYTES, MLKEM_SYMBYTES); diff --git a/mlkem/poly.h b/mlkem/poly.h index edd7f77e0..ed1d1d202 100644 --- a/mlkem/poly.h +++ b/mlkem/poly.h @@ -427,7 +427,7 @@ ASSIGNS(OBJECT_WHOLE(x)); void poly_reduce(poly *r) // clang-format off REQUIRES(IS_FRESH(r, sizeof(poly))) -ASSIGNS(OBJECT_WHOLE(r)) +ASSIGNS(OBJECT_UPTO(r, sizeof(poly))) ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, 0, MLKEM_Q - 1)); // clang-format on diff --git a/mlkem/polyvec.h b/mlkem/polyvec.h index 64eab49f6..8e1f16dfa 100644 --- a/mlkem/polyvec.h +++ b/mlkem/polyvec.h @@ -141,7 +141,26 @@ ASSIGNS(OBJECT_WHOLE(x)); // clang-format on #define polyvec_reduce MLKEM_NAMESPACE(polyvec_reduce) -void polyvec_reduce(polyvec *r); +/************************************************* + * Name: polyvec_reduce + * + * Description: Applies Barrett reduction to each coefficient + * of each element of a vector of polynomials; + * for details of the Barrett reduction see comments in reduce.c + * + * Arguments: - polyvec *r: pointer to input/output polynomial + **************************************************/ +// REF-CHANGE: The semantics of polyvec_reduce() is different in +// the reference implementation, which requires +// signed canonical output data. Unsigned canonical +// outputs are better suited to the only remaining +// use of poly_reduce() in the context of (de)serialization. +void polyvec_reduce(polyvec *r) // clang-format off +REQUIRES(IS_FRESH(r, sizeof(polyvec))) +ASSIGNS(OBJECT_WHOLE(r)) +ENSURES(FORALL(int, k0, 0, MLKEM_K - 1, + ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, r->vec[k0].coeffs, 0, MLKEM_Q - 1))); +// clang-format on #define polyvec_add MLKEM_NAMESPACE(polyvec_add) void polyvec_add(polyvec *r, const polyvec *b);