CBMC: Add functional spec for runtime bounds check

README.md

@@ -13,7 +13,7 @@
 mlkem-native is a secure, fast, and portable C90[^C90] implementation of ML-KEM[^FIPS203].
 It is a fork of the ML-KEM reference implementation[^REF].
 
-All C code in [mlkem/src/*](mlkem) and [mlkem/src/fips202/*](mlkem/src/fips202), except for the backends for platforms other than AArch64 and x86_64 and the debug code, is proved memory-safe (no memory overflow) and type-safe (no integer overflow)
+All C code in [mlkem/src/*](mlkem) and [mlkem/src/fips202/*](mlkem/src/fips202), except for the backends for platforms other than AArch64 and x86_64, is proved memory-safe (no memory overflow) and type-safe (no integer overflow)
 using CBMC[^CBMC]. All AArch64 and x86_64 assembly is proved to be functionally correct,
 memory-safe, and of secret-independent timing (constant-time), using HOL-Light[^HOL-Light].
 
@@ -54,7 +54,7 @@ mlkem-native is used in
 
 ## Formal Verification
 
-All C code in [mlkem/src/*](mlkem) and [mlkem/src/fips202/*](mlkem/src/fips202), except for the backends for platforms other than AArch64 and x86_64 and the debug code, is proved memory-safe (no memory overflow) and type-safe (no integer overflow).
+All C code in [mlkem/src/*](mlkem) and [mlkem/src/fips202/*](mlkem/src/fips202), except for the backends for platforms other than AArch64 and x86_64, is proved memory-safe (no memory overflow) and type-safe (no integer overflow).
 This uses the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) and builds on function contracts and loop invariant annotations
 in the source code. See [proofs/cbmc](proofs/cbmc) for details.
 

SOUNDNESS.md

@@ -163,6 +163,10 @@ coefficient bounds after arithmetic operations, or the functional specification
 `mlk_ct_memcmp`. See [`proofs/cbmc/Makefile.common`](proofs/cbmc/Makefile.common) for the
 full list of checked classes of undefined behavior.
 
+The scalar debug helpers are proved using CBMC's libc models, which do
+not parse `fprintf` formats or inspect variadic arguments. These proofs
+do not establish safety or output behavior of real formatted diagnostics.
+
 The CBMC proofs do **not** currently cover:
 
 - **Functional correctness.** There is no machine-checked proof that the C code computes

flake.nix

@@ -129,6 +129,9 @@
           };
           devShells.cbmc = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) cbmc toolchains_native; } ++ [ pkgs.gh ];
+            # Fortified glibc stdio wrappers use __builtin_va_arg_pack, which
+            # CBMC does not model. Keep the calls to the modeled libc functions.
+            hardeningDisable = [ "fortify" ];
           };
           devShells.slothy = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) slothy linters toolchains_native; };

mlkem/mlkem_native.c

@@ -621,11 +621,8 @@
 /* mlkem/src/native/riscv64/src/rv64v_debug.h */
 #undef MLK_NATIVE_RISCV64_SRC_RV64V_DEBUG_H
 #undef mlk_assert_abs_bound_int16m1
-#undef mlk_assert_abs_bound_int16m2
 #undef mlk_assert_bound_int16m1
-#undef mlk_assert_bound_int16m2
 #undef mlk_debug_check_bounds_int16m1
-#undef mlk_debug_check_bounds_int16m2
 #endif /* MLK_SYS_RISCV64 */
 #if defined(MLK_SYS_PPC64LE)
 /*

mlkem/mlkem_native_asm.S

@@ -652,11 +652,8 @@
 /* mlkem/src/native/riscv64/src/rv64v_debug.h */
 #undef MLK_NATIVE_RISCV64_SRC_RV64V_DEBUG_H
 #undef mlk_assert_abs_bound_int16m1
-#undef mlk_assert_abs_bound_int16m2
 #undef mlk_assert_bound_int16m1
-#undef mlk_assert_bound_int16m2
 #undef mlk_debug_check_bounds_int16m1
-#undef mlk_debug_check_bounds_int16m2
 #endif /* MLK_SYS_RISCV64 */
 #if defined(MLK_SYS_PPC64LE)
 /*

mlkem/src/debug.c

@@ -16,8 +16,23 @@
 
 #define MLK_DEBUG_ERROR_HEADER "[ERROR:%s:%04d] "
 
-void mlk_debug_check_assert(const char *file, int line, const int val)
+/*
+ * Spell out C-string validity using a length because CBMC 6.11 ignores
+ * __CPROVER_is_cstring and ignores __CPROVER_is_zero_string without string
+ * abstraction. String abstraction is incompatible with the dynamic-frame
+ * contract pass used by these proofs.
+ */
+void mlk_debug_check_assert(const char *file, size_t file_len, int line,
+                            const int val)
+__contract__(
+  requires(file_len > 0)
+  requires(file_len <= MLK_MAX_BUFFER_SIZE)
+  requires(memory_no_alias(file, file_len))
+  requires(file[file_len - 1] == '\0')
+  /* Safety proof only; no functional postcondition intended. */)
 {
+  (void)file_len;
+
   if (val == 0)
   {
     fprintf(stderr, MLK_DEBUG_ERROR_HEADER "Assertion failed (value %d)\n",
@@ -26,28 +41,72 @@ void mlk_debug_check_assert(const char *file, int line, const int val)
   }
 }
 
-void mlk_debug_check_bounds(const char *file, int line, const int16_t *ptr,
-                            unsigned len, int lower_bound_exclusive,
-                            int upper_bound_exclusive)
+/*
+ * The len bound controls proof complexity only. All repository call sites
+ * use lengths no greater than UINT16_MAX.
+ */
+static int mlk_debug_check_bounds_report(const char *file, size_t file_len,
+                                         int line, const int16_t *ptr,
+                                         unsigned len,
+                                         int lower_bound_exclusive,
+                                         int upper_bound_exclusive)
+__contract__(
+  requires(file_len > 0)
+  requires(file_len <= MLK_MAX_BUFFER_SIZE)
+  requires(memory_no_alias(file, file_len))
+  requires(file[file_len - 1] == '\0')
+  requires(len <= UINT16_MAX)
+  requires(lower_bound_exclusive < INT32_MAX)
+  requires(memory_no_alias(ptr, sizeof(int16_t) * len))
+  ensures(return_value ==
+          array_bound(ptr, 0, len, lower_bound_exclusive + 1,
+                      upper_bound_exclusive)))
 {
-  int err = 0;
+  int valid = 1;
   unsigned i;
+
+  (void)file_len;
+
   for (i = 0; i < len; i++)
+  __loop__(
+    invariant(i <= len)
+    invariant(valid ==
+              array_bound(ptr, 0, i, lower_bound_exclusive + 1,
+                          upper_bound_exclusive))
+    decreases(len - i))
   {
     int16_t val = ptr[i];
     if (!(val > lower_bound_exclusive && val < upper_bound_exclusive))
     {
-      fprintf(
-          stderr,
-          MLK_DEBUG_ERROR_HEADER
-          "Bounds assertion failed: Index %u, value %d out of bounds (%d,%d)\n",
-          file, line, i, (int)val, lower_bound_exclusive,
-          upper_bound_exclusive);
-      err = 1;
+      fprintf(stderr,
+              MLK_DEBUG_ERROR_HEADER
+              "Bounds assertion failed: Index %u, value %d out of bounds "
+              "(%d,%d)\n",
+              file, line, i, (int)val, lower_bound_exclusive,
+              upper_bound_exclusive);
+      valid = 0;
     }
   }
 
-  if (err == 1)
+  return valid;
+}
+
+void mlk_debug_check_bounds(const char *file, size_t file_len, int line,
+                            const int16_t *ptr, unsigned len,
+                            int lower_bound_exclusive,
+                            int upper_bound_exclusive)
+__contract__(
+  requires(file_len > 0)
+  requires(file_len <= MLK_MAX_BUFFER_SIZE)
+  requires(memory_no_alias(file, file_len))
+  requires(file[file_len - 1] == '\0')
+  requires(len <= UINT16_MAX)
+  requires(lower_bound_exclusive < INT32_MAX)
+  requires(memory_no_alias(ptr, sizeof(int16_t) * len)))
+{
+  if (!mlk_debug_check_bounds_report(file, file_len, line, ptr, len,
+                                     lower_bound_exclusive,
+                                     upper_bound_exclusive))
   {
     exit(1);
   }

mlkem/src/debug.h

@@ -14,44 +14,51 @@
  * Prints an error message to stderr and calls exit(1) on failure.
  *
  * @param[in] file Filename.
+ * @param     file_len Length of @p file, including its terminating null byte.
  * @param     line Line number.
  * @param     val  Value asserted to be non-zero.
  */
 #define mlk_debug_check_assert MLK_NAMESPACE(mlkem_debug_assert)
-void mlk_debug_check_assert(const char *file, int line, const int val);
+void mlk_debug_check_assert(const char *file, size_t file_len, int line,
+                            const int val);
 
 /**
  * Check whether values in an array of int16_t are within specified bounds.
  *
  * Prints an error message to stderr and calls exit(1) on failure.
  *
  * @param[in] file                  Filename.
+ * @param     file_len              Length of @p file, including its
+ *                                  terminating null byte.
  * @param     line                  Line number.
  * @param[in] ptr                   Base of array to be checked.
  * @param     len                   Number of int16_t in @p ptr.
  * @param     lower_bound_exclusive Exclusive lower bound.
  * @param     upper_bound_exclusive Exclusive upper bound.
  */
 #define mlk_debug_check_bounds MLK_NAMESPACE(mlkem_debug_check_bounds)
-void mlk_debug_check_bounds(const char *file, int line, const int16_t *ptr,
-                            unsigned len, int lower_bound_exclusive,
+void mlk_debug_check_bounds(const char *file, size_t file_len, int line,
+                            const int16_t *ptr, unsigned len,
+                            int lower_bound_exclusive,
                             int upper_bound_exclusive);
 
 /* Check assertion, calling exit() upon failure
  *
  * val: Value that's asserted to be non-zero
  */
-#define mlk_assert(val) mlk_debug_check_assert(__FILE__, __LINE__, (val))
+#define mlk_assert(val) \
+  mlk_debug_check_assert(__FILE__, sizeof(__FILE__), __LINE__, (val))
 
 /* Check bounds in array of int16_t's
  * ptr: Base of int16_t array; will be explicitly cast to int16_t*,
  *      so you may pass a byte-compatible type such as mlk_poly or mlk_polyvec.
  * len: Number of int16_t in array
  * value_lb: Inclusive lower value bound
  * value_ub: Exclusive upper value bound */
-#define mlk_assert_bound(ptr, len, value_lb, value_ub)                      \
-  mlk_debug_check_bounds(__FILE__, __LINE__, (const int16_t *)(ptr), (len), \
-                         (value_lb) - 1, (value_ub))
+#define mlk_assert_bound(ptr, len, value_lb, value_ub)                  \
+  mlk_debug_check_bounds(__FILE__, sizeof(__FILE__), __LINE__,          \
+                         (const int16_t *)(ptr), (len), (value_lb) - 1, \
+                         (value_ub))
 
 /* Check absolute bounds in array of int16_t's
  * ptr: Base of array, expression of type int16_t*

mlkem/src/native/riscv64/src/rv64v_debug.c

@@ -10,64 +10,34 @@
 #if defined(MLK_ARITH_BACKEND_RISCV64) && \
     !defined(MLK_CONFIG_MULTILEVEL_NO_SHARED) && defined(MLKEM_DEBUG)
 
-#include <stdio.h>
-#include <stdlib.h>
-
-#include "../../../debug.h"
 #include "rv64v_debug.h"
 
-#define MLK_DEBUG_ERROR_HEADER "[ERROR:%s:%04d] "
-
 /**
  * Check whether values in a vint16m1_t vector are within specified bounds.
  *
  * @param[in] file                  Filename.
+ * @param     file_len              Length of @p file, including its
+ *                                  terminating null byte.
  * @param     line                  Line number.
  * @param     vec                   RISC-V vector to be checked.
  * @param     vl                    Vector length (number of active elements).
  * @param     lower_bound_exclusive Exclusive lower bound.
  * @param     upper_bound_exclusive Exclusive upper bound.
  */
-void mlk_debug_check_bounds_int16m1(const char *file, int line, vint16m1_t vec,
-                                    size_t vl, int lower_bound_exclusive,
+void mlk_debug_check_bounds_int16m1(const char *file, size_t file_len, int line,
+                                    vint16m1_t vec, size_t vl,
+                                    int lower_bound_exclusive,
                                     int upper_bound_exclusive)
 {
   /* Allocate temporary array to store vector elements.
    * vl is at most MLKEM_N, as it is always obtained from
    * vsetvl with an AVL of at most MLKEM_N. */
   int16_t temp_array[MLKEM_N];
 
-  /* Store vector elements to temporary array for inspection */
+  mlk_debug_check_assert(file, file_len, line, vl <= MLKEM_N);
   __riscv_vse16_v_i16m1(temp_array, vec, vl);
 
-  /* Reuse existing array bounds checking function */
-  mlk_debug_check_bounds(file, line, temp_array, (unsigned)vl,
-                         lower_bound_exclusive, upper_bound_exclusive);
-}
-
-/**
- * Check whether values in a vint16m2_t vector are within specified bounds.
- *
- * @param[in] file                  Filename.
- * @param     line                  Line number.
- * @param     vec                   RISC-V vector to be checked.
- * @param     vl                    Vector length (active elements per m1 half).
- * @param     lower_bound_exclusive Exclusive lower bound.
- * @param     upper_bound_exclusive Exclusive upper bound.
- */
-void mlk_debug_check_bounds_int16m2(const char *file, int line, vint16m2_t vec,
-                                    size_t vl, int lower_bound_exclusive,
-                                    int upper_bound_exclusive)
-{
-  /* Allocate temporary array to store vector elements
-   * m2 vectors hold 2x the elements of m1 vectors */
-  int16_t temp_array[2 * MLKEM_N];
-
-  /* Store vector elements to temporary array for inspection */
-  __riscv_vse16_v_i16m2(temp_array, vec, 2 * vl);
-
-  /* Reuse existing array bounds checking function for all elements */
-  mlk_debug_check_bounds(file, line, temp_array, (unsigned)(2 * vl),
+  mlk_debug_check_bounds(file, file_len, line, temp_array, (unsigned)vl,
                          lower_bound_exclusive, upper_bound_exclusive);
 }
 
@@ -78,7 +48,3 @@ MLK_EMPTY_CU(rv64v_debug)
 
 #endif /* !(MLK_ARITH_BACKEND_RISCV64 && !MLK_CONFIG_MULTILEVEL_NO_SHARED && \
           MLKEM_DEBUG) */
-
-/* To facilitate single-compilation-unit (SCU) builds, undefine all macros.
- * Don't modify by hand -- this is auto-generated by scripts/autogen. */
-#undef MLK_DEBUG_ERROR_HEADER