From 0a49ea2e1540d392b4db4a18fb713762c536e8b9 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 12 Nov 2024 13:07:46 +0000 Subject: [PATCH] Add contracts and proof artefacts for indcpa_dec() Also adds proof of for unpack_ciphertext() and moves descriptive comment for indcpa_dec() from body to header file. Signed-off-by: Rod Chapman --- cbmc/proofs/indcpa_dec/Makefile | 61 +++++++++++++++++++ cbmc/proofs/indcpa_dec/cbmc-proof.txt | 3 + cbmc/proofs/indcpa_dec/indcpa_dec_harness.c | 28 +++++++++ cbmc/proofs/unpack_ciphertext/Makefile | 54 ++++++++++++++++ cbmc/proofs/unpack_ciphertext/cbmc-proof.txt | 3 + .../unpack_ciphertext_harness.c | 20 ++++++ mlkem/indcpa.c | 29 ++++----- mlkem/indcpa.h | 24 +++++++- 8 files changed, 203 insertions(+), 19 deletions(-) create mode 100644 cbmc/proofs/indcpa_dec/Makefile create mode 100644 cbmc/proofs/indcpa_dec/cbmc-proof.txt create mode 100644 cbmc/proofs/indcpa_dec/indcpa_dec_harness.c create mode 100644 cbmc/proofs/unpack_ciphertext/Makefile create mode 100644 cbmc/proofs/unpack_ciphertext/cbmc-proof.txt create mode 100644 cbmc/proofs/unpack_ciphertext/unpack_ciphertext_harness.c diff --git a/cbmc/proofs/indcpa_dec/Makefile b/cbmc/proofs/indcpa_dec/Makefile new file mode 100644 index 000000000..859c60c8f --- /dev/null +++ b/cbmc/proofs/indcpa_dec/Makefile @@ -0,0 +1,61 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = indcpa_dec_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 = indcpa_dec + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)indcpa_dec + +USED_FUNCTIONS = polyvec_ntt +USED_FUNCTIONS += polyvec_basemul_acc_montgomery +USED_FUNCTIONS += poly_invntt_tomont +USED_FUNCTIONS += poly_sub +USED_FUNCTIONS += poly_reduce +USED_FUNCTIONS += poly_tomsg +USE_FUNCTION_CONTRACTS=unpack_ciphertext unpack_sk $(addprefix $(MLKEM_NAMESPACE),$(USED_FUNCTIONS)) +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)indcpa_dec + +# 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 = 10 + +# 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/indcpa_dec/cbmc-proof.txt b/cbmc/proofs/indcpa_dec/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/indcpa_dec/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/indcpa_dec/indcpa_dec_harness.c b/cbmc/proofs/indcpa_dec/indcpa_dec_harness.c new file mode 100644 index 000000000..bc980db35 --- /dev/null +++ b/cbmc/proofs/indcpa_dec/indcpa_dec_harness.c @@ -0,0 +1,28 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +/* + * Insert copyright notice + */ + +/** + * @file indcpa_dec_harness.c + * @brief Implements the proof harness for indcpa_dec function. + */ + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ +#include +#include + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) { + uint8_t *m, *c, *sk; + indcpa_dec(m, c, sk); +} diff --git a/cbmc/proofs/unpack_ciphertext/Makefile b/cbmc/proofs/unpack_ciphertext/Makefile new file mode 100644 index 000000000..bd86e9e4b --- /dev/null +++ b/cbmc/proofs/unpack_ciphertext/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = unpack_ciphertext_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_ciphertext + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c + +CHECK_FUNCTION_CONTRACTS=unpack_ciphertext +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_decompress $(MLKEM_NAMESPACE)poly_decompress +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_ciphertext + +# 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_ciphertext/cbmc-proof.txt b/cbmc/proofs/unpack_ciphertext/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/unpack_ciphertext/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_ciphertext/unpack_ciphertext_harness.c b/cbmc/proofs/unpack_ciphertext/unpack_ciphertext_harness.c new file mode 100644 index 000000000..36e9e8f9f --- /dev/null +++ b/cbmc/proofs/unpack_ciphertext/unpack_ciphertext_harness.c @@ -0,0 +1,20 @@ +// 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_ciphertext(polyvec *b, poly *v, + const uint8_t c[MLKEM_INDCPA_BYTES]); + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) { + polyvec *b; + poly *v; + uint8_t *c; + + unpack_ciphertext(b, v, c); +} diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c index 4418f5c24..475923f09 100644 --- a/mlkem/indcpa.c +++ b/mlkem/indcpa.c @@ -153,8 +153,19 @@ static void pack_ciphertext(uint8_t r[MLKEM_INDCPA_BYTES], polyvec *b, * - poly *v: pointer to the output polynomial v * - const uint8_t *c: pointer to the input serialized ciphertext **************************************************/ -static void unpack_ciphertext(polyvec *b, poly *v, - const uint8_t c[MLKEM_INDCPA_BYTES]) { +STATIC_TESTABLE +void unpack_ciphertext(polyvec *b, poly *v, + const uint8_t c[MLKEM_INDCPA_BYTES]) // clang-format off +REQUIRES(IS_FRESH(b, sizeof(polyvec))) +REQUIRES(IS_FRESH(v, sizeof(poly))) +REQUIRES(IS_FRESH(c, MLKEM_INDCPA_BYTES)) +ASSIGNS(OBJECT_WHOLE(b)) +ASSIGNS(OBJECT_WHOLE(v)) +ENSURES(FORALL(int, k0, 0, MLKEM_K - 1, + ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), b->vec[k0].coeffs, 0, (MLKEM_Q - 1)))) +ENSURES(ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), v->coeffs, 0, (MLKEM_Q - 1))) +// clang-format on +{ polyvec_decompress(b, c); poly_decompress(v, c + MLKEM_POLYVECCOMPRESSEDBYTES); } @@ -525,20 +536,6 @@ void indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], pack_ciphertext(c, &b, &v); } -/************************************************* - * Name: indcpa_dec - * - * Description: Decryption function of the CPA-secure - * public-key encryption scheme underlying Kyber. - * - * Arguments: - uint8_t *m: pointer to output decrypted message - * (of length MLKEM_INDCPA_MSGBYTES) - * - const uint8_t *c: pointer to input ciphertext - * (of length MLKEM_INDCPA_BYTES) - * - const uint8_t *sk: pointer to input secret key - * (of length MLKEM_INDCPA_SECRETKEYBYTES) - **************************************************/ - // Check that the arithmetic in indcpa_dec() does not overflow STATIC_ASSERT(INVNTT_BOUND + MLKEM_Q < INT16_MAX, indcpa_dec_bound_0) diff --git a/mlkem/indcpa.h b/mlkem/indcpa.h index b7e277154..a62b9b4a3 100644 --- a/mlkem/indcpa.h +++ b/mlkem/indcpa.h @@ -33,6 +33,19 @@ void indcpa_keypair_derand( // clang-format on #define indcpa_enc MLKEM_NAMESPACE(indcpa_enc) +/************************************************* + * Name: indcpa_dec + * + * Description: Decryption function of the CPA-secure + * public-key encryption scheme underlying Kyber. + * + * Arguments: - uint8_t *m: pointer to output decrypted message + * (of length MLKEM_INDCPA_MSGBYTES) + * - const uint8_t *c: pointer to input ciphertext + * (of length MLKEM_INDCPA_BYTES) + * - const uint8_t *sk: pointer to input secret key + * (of length MLKEM_INDCPA_SECRETKEYBYTES) + **************************************************/ void indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], const uint8_t m[MLKEM_INDCPA_MSGBYTES], const uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], @@ -45,8 +58,13 @@ void indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], // clang-format on #define indcpa_dec MLKEM_NAMESPACE(indcpa_dec) -void indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES], - const uint8_t c[MLKEM_INDCPA_BYTES], - const uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES]); +void indcpa_dec( + uint8_t m[MLKEM_INDCPA_MSGBYTES], const uint8_t c[MLKEM_INDCPA_BYTES], + const uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES]) // clang-format off + REQUIRES(IS_FRESH(c, MLKEM_INDCPA_BYTES)) + REQUIRES(IS_FRESH(m, MLKEM_INDCPA_MSGBYTES)) + REQUIRES(IS_FRESH(sk, MLKEM_INDCPA_SECRETKEYBYTES)) + ASSIGNS(OBJECT_WHOLE(m)); +// clang-format on #endif