CBMC: Proof of type safety and memory safety for toplevel MLKEM KeyGen (modulo NTT+SHA3)

.github/actions/cbmc/action.yml

@@ -48,5 +48,5 @@ runs:
         run: |
           cd cbmc/proofs;
           echo "::group::cbmc_${{ inputs.mlkem_k }}"
-          MLKEM_K=${{ inputs.mlkem_k }} ./run-cbmc-proofs.py --summarize -j8;
+          MLKEM_K=${{ inputs.mlkem_k }} ./run-cbmc-proofs.py --summarize --no-coverage -j8;
           echo "::endgroup::"

cbmc/proofs/crypto_kem_keypair_derand/Makefile

@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = crypto_kem_keypair_derand_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 = crypto_kem_keypair_derand
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keypair_derand
+USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)sha3_256 $(MLKEM_NAMESPACE)indcpa_keypair_derand
+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)keypair_derand
+
+# 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

cbmc/proofs/crypto_kem_keypair_derand/cbmc-proof.txt

@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.

cbmc/proofs/crypto_kem_keypair_derand/crypto_kem_keypair_derand_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 crypto_kem_keypair_derand_harness.c
+ * @brief Implements the proof harness for crypto_kem_keypair_derand function.
+ */
+
+/*
+ * Insert project header files that
+ *   - include the declaration of the function
+ *   - include the types needed to declare function arguments
+ */
+#include <kem.h>
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void) {
+  uint8_t *a, *b, *c;
+  crypto_kem_keypair_derand(a, b, c);
+}

cbmc/proofs/indcpa_keypair_derand/Makefile

@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = indcpa_keypair_derand_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_keypair_derand
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)indcpa_keypair_derand
+USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)sha3_512 $(MLKEM_NAMESPACE)gen_matrix $(MLKEM_NAMESPACE)poly_getnoise_eta1_4x $(MLKEM_NAMESPACE)polyvec_ntt $(MLKEM_NAMESPACE)polyvec_mulcache_compute matvec_mul $(MLKEM_NAMESPACE)polyvec_tomont $(MLKEM_NAMESPACE)polyvec_add $(MLKEM_NAMESPACE)polyvec_reduce pack_sk pack_pk
+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_keypair_derand
+
+# 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

cbmc/proofs/indcpa_keypair_derand/cbmc-proof.txt

@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.

cbmc/proofs/indcpa_keypair_derand/indcpa_keypair_derand_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 indcpa_keypair_derand_harness.c
+ * @brief Implements the proof harness for indcpa_keypair_derand function.
+ */
+
+/*
+ * Insert project header files that
+ *   - include the declaration of the function
+ *   - include the types needed to declare function arguments
+ */
+#include <indcpa.h>
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void) {
+  uint8_t *a, *b, *c;
+  indcpa_keypair_derand(a, b, c);
+}

cbmc/proofs/matvec_mul/Makefile

@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = matvec_mul_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 = matvec_mul
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += matvec_mul.0:4 # Maximum value of MLKEM_K
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c
+
+CHECK_FUNCTION_CONTRACTS=matvec_mul
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_mulcache_compute $(MLKEM_NAMESPACE)polyvec_basemul_acc_montgomery_cached
+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)matvec_mul
+
+# 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

cbmc/proofs/matvec_mul/cbmc-proof.txt

@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.

cbmc/proofs/matvec_mul/matvec_mul_harness.c

@@ -0,0 +1,32 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+/*
+ * Insert copyright notice
+ */
+
+/**
+ * @file matvec_mul_harness.c
+ * @brief Implements the proof harness for poly_reduce function.
+ */
+
+/*
+ * Insert project header files that
+ *   - include the declaration of the function
+ *   - include the types needed to declare function arguments
+ */
+#include "indcpa.h"
+#include "polyvec.h"
+
+void matvec_mul(polyvec *out, polyvec const *a, polyvec const *v,
+                polyvec_mulcache const *vc);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void) {
+  polyvec *out, *a, *v;
+  polyvec_mulcache *vc;
+  matvec_mul(out, a, v, vc);
+}

cbmc/proofs/polyvec_tomont/Makefile

@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = polyvec_tomont_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_tomont
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += $(MLKEM_NAMESPACE)polyvec_tomont.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_tomont
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_tomont
+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_tomont
+
+# 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

cbmc/proofs/polyvec_tomont/cbmc-proof.txt

@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.

cbmc/proofs/polyvec_tomont/polyvec_tomont_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_tomont_harness.c
+ * @brief Implements the proof harness for polyvec_tomont function.
+ */
+
+/*
+ * Insert project header files that
+ *   - include the declaration of the function
+ *   - include the types needed to declare function arguments
+ */
+#include <polyvec.h>
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void) {
+  polyvec *a;
+  polyvec_tomont(a);
+}

fips202/fips202.h

@@ -88,10 +88,25 @@ ASSIGNS(OBJECT_UPTO(output, outlen));
 
 /* One-stop SHA3-256 shop */
 #define sha3_256 FIPS202_NAMESPACE(sha3_256)
-void sha3_256(uint8_t *output, const uint8_t *input, size_t inlen);
+void sha3_256(uint8_t *output, const uint8_t *input, size_t inlen)
+    // clang-format off
+REQUIRES(IS_FRESH(input, inlen))
+REQUIRES(IS_FRESH(output, 32))
+ASSIGNS(OBJECT_WHOLE(output));
+// clang-format on
 
 /* One-stop SHA3-512 shop */
 #define sha3_512 FIPS202_NAMESPACE(sha3_512)
-void sha3_512(uint8_t *output, const uint8_t *input, size_t inlen);
+void sha3_512(uint8_t *output, const uint8_t *input, size_t inlen)
+    // clang-format off
+REQUIRES(
+    /* Case A: Aliasing between input and output */
+    (output == input && inlen <= 64 && IS_FRESH(output, 64))
+ ||
+    /* Case B: Disjoint input and output */
+    (IS_FRESH(input, inlen) && IS_FRESH(output, 64))
+)
+ASSIGNS(OBJECT_WHOLE(output));
+// clang-format on
 
 #endif