CBMC: Add contracts to native backend

So far, the CBMC proofs covered the combination of C frontend and C
backend. While most native backend functions are drop-in replacements
of functions in the default C backend and should thus inherit their
specification, there are minor differences in signature (in particular
since #675) or functionality (e.g. the native implementation of
rej_uniform may reject certain inputs, and the frontend uses fallback
logic which is not present with the C backend) that merit explicit
contract annotations for all functions in the arithmetic and FIPS202
backend, and proofs against those specs.

This commit takes a step in this direction by adding CBMC contracts
for all functions in the native arithmetic backend, except for
`rej_uniform_native`, and proving that their call-sites still uphold
their spec when the respective MLKEM_USE_NATIVE_XXX option is set.
This is largely trivial, but it is still worth doing for
(a) documentation purposes, and since (b) the native backends operate
on raw arrays, while their call-sites operate in terms of the
`poly_xxx` structs.

The case of `rej_uniform` is more complicated and will be
handled separately.

Signed-off-by: Hanno Becker <[email protected]>

mlkem/native/api.h

@@ -23,8 +23,15 @@
 #define MLKEM_NATIVE_ARITH_NATIVE_API_H
 
 #include <stdint.h>
+#include "../cbmc.h"
 #include "../common.h"
 
+/* Absolute exclusive upper bound for the output of the inverse NTT */
+#define INVNTT_BOUND (8 * MLKEM_Q)
+
+/* Absolute exclusive upper bound for the output of the forward NTT */
+#define NTT_BOUND (8 * MLKEM_Q)
+
 /*
  * This is the C<->native interface allowing for the drop-in of
  * native code for performance critical arithmetic components of ML-KEM.
@@ -66,7 +73,13 @@
  *
  * Arguments:   - int16_t p[MLKEM_N]: pointer to in/output polynomial
  **************************************************/
-static INLINE void ntt_native(int16_t p[MLKEM_N]);
+static INLINE void ntt_native(int16_t p[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
+  requires(array_abs_bound(p, 0, MLKEM_N, MLKEM_Q))
+  assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
+  ensures(array_abs_bound(p, 0, MLKEM_N, NTT_BOUND))
+);
 #endif /* MLKEM_USE_NATIVE_NTT */
 
 #if defined(MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER)
@@ -98,7 +111,14 @@ and to/from bytes conversions."
  * Arguments:   - int16_t p[MLKEM_N]: pointer to in/output polynomial
  *
  **************************************************/
-static INLINE void poly_permute_bitrev_to_custom(int16_t p[MLKEM_N]);
+static INLINE void poly_permute_bitrev_to_custom(int16_t p[MLKEM_N])
+__contract__(
+  /* We don't specify that this should be a permutation, but only
+   * that it does not change the bound established at the end of gen_matrix. */
+  requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
+  requires(array_bound(p, 0, MLKEM_N, 0, MLKEM_Q))
+  assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
+  ensures(array_bound(p, 0, MLKEM_N, 0, MLKEM_Q)));
 #endif /* MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER */
 
 #if defined(MLKEM_USE_NATIVE_INTT)
@@ -116,7 +136,12 @@ static INLINE void poly_permute_bitrev_to_custom(int16_t p[MLKEM_N]);
  *
  * Arguments:   - uint16_t *a: pointer to in/output polynomial
  **************************************************/
-static INLINE void intt_native(int16_t p[MLKEM_N]);
+static INLINE void intt_native(int16_t p[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
+  assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
+  ensures(array_abs_bound(p, 0, MLKEM_N, INVNTT_BOUND))
+);
 #endif /* MLKEM_USE_NATIVE_INTT */
 
 #if defined(MLKEM_USE_NATIVE_POLY_REDUCE)
@@ -127,7 +152,12 @@ static INLINE void intt_native(int16_t p[MLKEM_N]);
  *
  * Arguments:   - int16_t r[MLKEM_N]: pointer to input/output polynomial
  **************************************************/
-static INLINE void poly_reduce_native(int16_t p[MLKEM_N]);
+static INLINE void poly_reduce_native(int16_t p[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
+  assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
+  ensures(array_bound(p, 0, MLKEM_N, 0, MLKEM_Q))
+);
 #endif /* MLKEM_USE_NATIVE_POLY_REDUCE */
 
 #if defined(MLKEM_USE_NATIVE_POLY_TOMONT)
@@ -139,7 +169,12 @@ static INLINE void poly_reduce_native(int16_t p[MLKEM_N]);
  *
  * Arguments:   - int16_t r[MLKEM_N]: pointer to input/output polynomial
  **************************************************/
-static INLINE void poly_tomont_native(int16_t p[MLKEM_N]);
+static INLINE void poly_tomont_native(int16_t p[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
+  assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
+  ensures(array_abs_bound(p, 0, MLKEM_N, MLKEM_Q))
+);
 #endif /* MLKEM_USE_NATIVE_POLY_TOMONT */
 
 #if defined(MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE)
@@ -165,7 +200,12 @@ static INLINE void poly_tomont_native(int16_t p[MLKEM_N]);
  *              - cache: pointer to multiplication cache
  **************************************************/
 static INLINE void poly_mulcache_compute_native(int16_t cache[MLKEM_N / 2],
-                                                const int16_t poly[MLKEM_N]);
+                                                const int16_t poly[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(cache, sizeof(int16_t) * (MLKEM_N / 2)))
+  requires(memory_no_alias(poly, sizeof(int16_t) * MLKEM_N))
+  assigns(object_whole(cache))
+);
 #endif /* MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE */
 
 #if defined(MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED)
@@ -190,7 +230,25 @@ static INLINE void poly_mulcache_compute_native(int16_t cache[MLKEM_N / 2],
 static INLINE void polyvec_basemul_acc_montgomery_cached_native(
     int16_t r[MLKEM_N], const int16_t a[MLKEM_K * MLKEM_N],
     const int16_t b[MLKEM_K * MLKEM_N],
-    const int16_t b_cache[MLKEM_K * (MLKEM_N / 2)]);
+    const int16_t b_cache[MLKEM_K * (MLKEM_N / 2)])
+__contract__(
+  requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
+  requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_K * MLKEM_N))
+  requires(memory_no_alias(b, sizeof(int16_t) * MLKEM_K * MLKEM_N))
+  requires(memory_no_alias(b_cache, sizeof(int16_t) * MLKEM_K * (MLKEM_N / 2)))
+  /* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
+   * just use a single flattened array_bound(...) here.
+   *
+   * Once fixed, change to:
+   * ```
+   * requires(array_bound(a, 0, MLKEM_K * MLKEM_N, 0, UINT12_LIMIT))
+   * ```
+   */
+  requires(forall(kN, 0, MLKEM_K,					  \
+              array_bound(&((int16_t(*)[MLKEM_N])(a))[kN][0], 0, MLKEM_N, \
+			  0, UINT12_LIMIT)))
+  assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+);
 #endif
 
 #if defined(MLKEM_USE_NATIVE_POLY_TOBYTES)
@@ -209,7 +267,13 @@ static INLINE void polyvec_basemul_acc_montgomery_cached_native(
  *                   (of MLKEM_POLYBYTES bytes)
  **************************************************/
 static INLINE void poly_tobytes_native(uint8_t r[MLKEM_POLYBYTES],
-                                       const int16_t a[MLKEM_N]);
+                                       const int16_t a[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(r, MLKEM_POLYBYTES))
+  requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
+  requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
+  assigns(object_whole(r))
+);
 #endif /* MLKEM_USE_NATIVE_POLY_TOBYTES */
 
 #if defined(MLKEM_USE_NATIVE_POLY_FROMBYTES)
@@ -227,7 +291,13 @@ static INLINE void poly_tobytes_native(uint8_t r[MLKEM_POLYBYTES],
  *                   (of MLKEM_POLYBYTES bytes)
  **************************************************/
 static INLINE void poly_frombytes_native(int16_t a[MLKEM_N],
-                                         const uint8_t r[MLKEM_POLYBYTES]);
+                                         const uint8_t r[MLKEM_POLYBYTES])
+__contract__(
+  requires(memory_no_alias(r, MLKEM_POLYBYTES))
+  requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
+  assigns(memory_slice(a, sizeof(int16_t) * MLKEM_N))
+  ensures(array_bound(a, 0, MLKEM_N, 0, UINT12_LIMIT))
+);
 #endif /* MLKEM_USE_NATIVE_POLY_FROMBYTES */
 
 #if defined(MLKEM_USE_NATIVE_REJ_UNIFORM)

proofs/cbmc/Makefile.common

@@ -321,6 +321,7 @@ ADD_LIBRARY_FLAG := --add-library
 # Preprocessor include paths -I...
 INCLUDES ?=
 INCLUDES += -I$(PROOFDIR)
+INCLUDES += -I$(SRCDIR)/proofs/cbmc
 INCLUDES += -I$(SRCDIR)/mlkem
 INCLUDES += -I$(SRCDIR)/mlkem/fips202
 

proofs/cbmc/dummy_backend.h

@@ -0,0 +1,18 @@
+/*
+ * Copyright (c) 2024 The mlkem-native project authors
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+#ifdef MLKEM_NATIVE_ARITH_PROFILE_H
+#error Only one MLKEM_ARITH assembly profile can be defined -- did you include multiple profiles?
+#else
+#define MLKEM_NATIVE_ARITH_PROFILE_H
+
+#define MLKEM_NATIVE_ARITH_BACKEND_NAME DUMMY_BACKEND
+
+/* Filename of the C backend implementation.
+ * This is not inlined here because this header is included in assembly
+ * files as well. */
+#define MLKEM_NATIVE_ARITH_BACKEND_IMPL "dummy_backend_impl.h"
+
+#endif /* MLKEM_NATIVE_ARITH_PROFILE_H */

proofs/cbmc/dummy_backend_impl.h

@@ -0,0 +1,26 @@
+/*
+ * Copyright (c) 2024 The mlkem-native project authors
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+/* ML-KEM arithmetic native profile for clean assembly */
+
+#ifdef MLKEM_NATIVE_ARITH_PROFILE_IMPL_H
+#error Only one MLKEM_ARITH assembly profile can be defined -- did you include multiple profiles?
+#else
+#define MLKEM_NATIVE_ARITH_PROFILE_IMPL_H
+
+#define MLKEM_USE_NATIVE_REJ_UNIFORM
+#define MLKEM_USE_NATIVE_NTT
+#define MLKEM_USE_NATIVE_INTT
+#define MLKEM_USE_NATIVE_POLY_REDUCE
+#define MLKEM_USE_NATIVE_POLY_TOMONT
+#define MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED
+#define MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE
+#define MLKEM_USE_NATIVE_POLY_TOBYTES
+#define MLKEM_USE_NATIVE_POLY_FROMBYTES
+#define MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER
+
+#include "../mlkem/native/api.h"
+
+#endif /* MLKEM_NATIVE_ARITH_PROFILE_IMPL_H */

proofs/cbmc/gen_matrix_native_order/Makefile

@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = gen_matrix_native_order_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 = gen_matrix_native_order
+
+DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\""
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += $(MLKEM_NAMESPACE)gen_matrix.0:4 $(MLKEM_NAMESPACE)gen_matrix.1:4 $(MLKEM_NAMESPACE)gen_matrix.2:4 $(MLKEM_NAMESPACE)gen_matrix.3:4 $(MLKEM_NAMESPACE)gen_matrix.4:4
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)gen_matrix
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_rej_uniform $(MLKEM_NAMESPACE)poly_rej_uniform_x4 poly_permute_bitrev_to_custom
+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)gen_matrix_native_order
+
+# 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

proofs/cbmc/gen_matrix_native_order/cbmc-proof.txt

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

proofs/cbmc/gen_matrix_native_order/gen_matrix_native_order_harness.c

@@ -0,0 +1,14 @@
+// Copyright (c) 2024 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <stdint.h>
+#include "indcpa.h"
+
+void harness(void)
+{
+  polyvec *a;
+  uint8_t *seed;
+  int transposed;
+  gen_matrix(a, seed, transposed);
+}

proofs/cbmc/poly_frombytes_native/Makefile

@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = poly_frombytes_native_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 = poly_frombytes_native
+
+DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\""
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/compress.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_frombytes
+USE_FUNCTION_CONTRACTS=poly_frombytes_native
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--bitwuzla
+
+FUNCTION_NAME = poly_frombytes_native
+
+# 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

proofs/cbmc/poly_frombytes_native/cbmc-proof.txt

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

proofs/cbmc/poly_frombytes_native/poly_frombytes_native_harness.c

@@ -0,0 +1,14 @@
+// Copyright (c) 2024 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include "compress.h"
+
+void harness(void)
+{
+  poly *a;
+  uint8_t *r;
+
+  /* Contracts for this function are in poly.h */
+  poly_frombytes(a, r);
+}