From 93e86ff11462c5ce166fe7a7f0d53592c8421a94 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 12 Oct 2026 06:23:26 +0100 Subject: [PATCH 1/3] CBMC: Prove debug bounds logic `mlk_debug_check_bounds_report()` scans an `int16_t` array and reports values outside exclusive bounds. Prove that its return value equals `array_bound(ptr, 0, len, lower_bound_exclusive + 1, upper_bound_exclusive)`. The loop invariant establishes the same claim for each processed prefix. The `+ 1` conversion assumes `lower_bound_exclusive < INT32_MAX`. Also check the public bounds wrapper and assertion helper for safety. Pass `file_len` through the debug APIs and require a nonempty fresh range ending in a null byte. Macros pass `sizeof(__FILE__)`; harnesses keep the inputs arbitrary. Use an explicit length because CBMC 6.11's string predicates do not work with the current dynamic-frame pass. CBMC's `vfprintf` model does not parse formats or inspect variadic arguments. These proofs therefore do not establish memory safety or output behavior of the real `fprintf`; they check only the surrounding C code under CBMC's library model. Declare `exit` in the shared data-model shims. Diagnostics, ordering, and exit behavior are unchanged. Signed-off-by: Hanno Becker --- mlkem/src/debug.c | 85 ++++++++++++++++--- mlkem/src/debug.h | 21 +++-- proofs/cbmc/debug_check_assert/Makefile | 37 ++++++++ .../debug_check_assert_harness.c | 15 ++++ proofs/cbmc/debug_check_bounds/Makefile | 37 ++++++++ .../debug_check_bounds_harness.c | 19 +++++ proofs/cbmc/include/ILP32/stdlib.h | 2 + proofs/cbmc/include/LP64/stdlib.h | 2 + 8 files changed, 198 insertions(+), 20 deletions(-) create mode 100644 proofs/cbmc/debug_check_assert/Makefile create mode 100644 proofs/cbmc/debug_check_assert/debug_check_assert_harness.c create mode 100644 proofs/cbmc/debug_check_bounds/Makefile create mode 100644 proofs/cbmc/debug_check_bounds/debug_check_bounds_harness.c diff --git a/mlkem/src/debug.c b/mlkem/src/debug.c index 386f5264ff..98c85a472b 100644 --- a/mlkem/src/debug.c +++ b/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); } diff --git a/mlkem/src/debug.h b/mlkem/src/debug.h index ce4a33a373..8cf830cc1c 100644 --- a/mlkem/src/debug.h +++ b/mlkem/src/debug.h @@ -14,11 +14,13 @@ * 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. @@ -26,6 +28,8 @@ void mlk_debug_check_assert(const char *file, int line, const int val); * 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. @@ -33,15 +37,17 @@ void mlk_debug_check_assert(const char *file, int line, const int val); * @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*, @@ -49,9 +55,10 @@ void mlk_debug_check_bounds(const char *file, int line, const int16_t *ptr, * 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* diff --git a/proofs/cbmc/debug_check_assert/Makefile b/proofs/cbmc/debug_check_assert/Makefile new file mode 100644 index 0000000000..00164ae9a4 --- /dev/null +++ b/proofs/cbmc/debug_check_assert/Makefile @@ -0,0 +1,37 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = debug_check_assert_harness + +PROOF_UID = mlk_debug_check_assert + +# Use native stdio declarations that match CBMC's libc model. The data-model +# stdlib.h supplies declarations for the linked libc models. +COMPILE_FLAGS = -Wall -Werror --native-compiler gcc \ + -I$(PROOF_INCLUDE) $(GOTO_CC_DM_FLAG) + +DEFINES += -DMLKEM_DEBUG + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/debug.c + +CHECK_FUNCTION_CONTRACTS = mlk_mlkem_debug_assert +USE_FUNCTION_CONTRACTS = +APPLY_LOOP_CONTRACTS = +USE_DYNAMIC_FRAMES = 1 + +# Supported CBMC configurations +CBMC_SUPPORTED_CONFIGS = LP64:z3 ILP32:z3 +CBMC_DEFAULT_CONFIG = LP64:z3 + +FUNCTION_NAME = mlk_debug_check_assert + +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/debug_check_assert/debug_check_assert_harness.c b/proofs/cbmc/debug_check_assert/debug_check_assert_harness.c new file mode 100644 index 0000000000..6cd71f6ac2 --- /dev/null +++ b/proofs/cbmc/debug_check_assert/debug_check_assert_harness.c @@ -0,0 +1,15 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +#include "debug.h" + +void harness(void) +{ + const char *file; + size_t file_len; + int line; + int val; + + mlk_debug_check_assert(file, file_len, line, val); +} diff --git a/proofs/cbmc/debug_check_bounds/Makefile b/proofs/cbmc/debug_check_bounds/Makefile new file mode 100644 index 0000000000..74c0e1c227 --- /dev/null +++ b/proofs/cbmc/debug_check_bounds/Makefile @@ -0,0 +1,37 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = debug_check_bounds_harness + +PROOF_UID = mlk_debug_check_bounds_report + +DEFINES += -DMLKEM_DEBUG + +# Use native stdio declarations that match CBMC's libc model. The data-model +# stdlib.h supplies declarations for the linked libc models. +COMPILE_FLAGS = -Wall -Werror --native-compiler gcc \ + -I$(PROOF_INCLUDE) $(GOTO_CC_DM_FLAG) + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/debug.c + +CHECK_FUNCTION_CONTRACTS = mlk_debug_check_bounds_report \ + mlk_mlkem_debug_check_bounds +USE_FUNCTION_CONTRACTS = +APPLY_LOOP_CONTRACTS = on +USE_DYNAMIC_FRAMES = 1 + +CBMC_SUPPORTED_CONFIGS = LP64:z3 ILP32:z3 +CBMC_DEFAULT_CONFIG = LP64:z3 + +FUNCTION_NAME = mlk_debug_check_bounds_report + +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/debug_check_bounds/debug_check_bounds_harness.c b/proofs/cbmc/debug_check_bounds/debug_check_bounds_harness.c new file mode 100644 index 0000000000..82b7d37dd5 --- /dev/null +++ b/proofs/cbmc/debug_check_bounds/debug_check_bounds_harness.c @@ -0,0 +1,19 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +#include "debug.h" + +void harness(void) +{ + const char *file; + size_t file_len; + int line; + const int16_t *ptr; + unsigned len; + int lower_bound_exclusive; + int upper_bound_exclusive; + + mlk_debug_check_bounds(file, file_len, line, ptr, len, lower_bound_exclusive, + upper_bound_exclusive); +} diff --git a/proofs/cbmc/include/ILP32/stdlib.h b/proofs/cbmc/include/ILP32/stdlib.h index 46d5fbaee1..d405716ed4 100644 --- a/proofs/cbmc/include/ILP32/stdlib.h +++ b/proofs/cbmc/include/ILP32/stdlib.h @@ -13,4 +13,6 @@ void *malloc(size_t size); void free(void *ptr); +void exit(int status); + #endif /* !_STDLIB_H */ diff --git a/proofs/cbmc/include/LP64/stdlib.h b/proofs/cbmc/include/LP64/stdlib.h index 2908e34145..0814c165e9 100644 --- a/proofs/cbmc/include/LP64/stdlib.h +++ b/proofs/cbmc/include/LP64/stdlib.h @@ -12,4 +12,6 @@ void *malloc(size_t size); void free(void *ptr); +void exit(int status); + #endif /* !_STDLIB_H */ From 51d5701005f78ccc4d5c39f431a13a73f387dfde Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 12 Oct 2026 06:23:34 +0100 Subject: [PATCH 2/3] RV64: Remove m2 debug helper and guard m1 spill RVV debug bounds checks spill active vector lanes into scalar arrays before calling the generic checker. In-tree assertions use only the m1 adapter; the m2 helper and macros have no callers. The m1 adapter sizes its buffer to `MLKEM_N` but does not check `vl` before the vector store. Remove the m2 function, macros, and generated single-compilation-unit undefinitions. Assert `vl <= MLKEM_N` before `__riscv_vse16_v_i16m1`. Include `riscv_vector.h` in the debug-only header branch. Preserve the compilation-unit guard and give `MLKEM_DEBUG` priority over `CBMC`, as the scalar helpers do. The CBMC-only vector macros remain no-ops. Pass `file_len` through the remaining m1 adapter so calls to the scalar debug helpers preserve their bounded filename contracts. Its macro passes `sizeof(__FILE__)`. Contract lint finds proofs by directory name. The bounds reporter and wrapper previously shared `debug_check_bounds`, so the reporter had no matching proof directory and lint rejected its contract. Give `mlk_debug_check_bounds_report` its own harness and proof directory. Keep `debug_check_bounds` for the wrapper and use the reporter's contract there. Both proofs retain the existing LP64 and ILP32 configurations and CBMC library model. Keep `MLKEM_DEBUG` enabled in the scalar debug-helper proofs so they compile the runtime implementations rather than the assertion macros used by ordinary CBMC proofs. The debug proofs include native stdio headers. On Linux, Nix enables glibc's fortified `fprintf` wrapper, whose `__builtin_va_arg_pack` call has no CBMC model. The assertion and bounds-reporter proofs therefore fail when they take a diagnostic path. Disable `fortify` in the CBMC Nix shell to retain calls to the modeled libc functions. Keep hardening in other shells unchanged. CBMC's `fprintf` model does not inspect variadic arguments. These scalar proofs do not establish memory safety or output behavior of the real `fprintf`, or cover the RVV store intrinsic. Signed-off-by: Hanno Becker --- flake.nix | 3 + mlkem/mlkem_native.c | 3 - mlkem/mlkem_native_asm.S | 3 - mlkem/src/native/riscv64/src/rv64v_debug.c | 48 ++--------- mlkem/src/native/riscv64/src/rv64v_debug.h | 84 ++++--------------- proofs/cbmc/debug_check_bounds/Makefile | 9 +- .../cbmc/debug_check_bounds_report/Makefile | 36 ++++++++ .../debug_check_bounds_report_harness.c | 24 ++++++ 8 files changed, 90 insertions(+), 120 deletions(-) create mode 100644 proofs/cbmc/debug_check_bounds_report/Makefile create mode 100644 proofs/cbmc/debug_check_bounds_report/debug_check_bounds_report_harness.c diff --git a/flake.nix b/flake.nix index 7b152899bb..13fc2aebc9 100644 --- a/flake.nix +++ b/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; }; diff --git a/mlkem/mlkem_native.c b/mlkem/mlkem_native.c index 84adf0806c..60fbf42c0f 100644 --- a/mlkem/mlkem_native.c +++ b/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) /* diff --git a/mlkem/mlkem_native_asm.S b/mlkem/mlkem_native_asm.S index e0a0213c57..8323ca2e77 100644 --- a/mlkem/mlkem_native_asm.S +++ b/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) /* diff --git a/mlkem/src/native/riscv64/src/rv64v_debug.c b/mlkem/src/native/riscv64/src/rv64v_debug.c index 22e60f9a6c..f8f5087519 100644 --- a/mlkem/src/native/riscv64/src/rv64v_debug.c +++ b/mlkem/src/native/riscv64/src/rv64v_debug.c @@ -10,26 +10,23 @@ #if defined(MLK_ARITH_BACKEND_RISCV64) && \ !defined(MLK_CONFIG_MULTILEVEL_NO_SHARED) && defined(MLKEM_DEBUG) -#include -#include - -#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. @@ -37,37 +34,10 @@ void mlk_debug_check_bounds_int16m1(const char *file, int line, vint16m1_t vec, * 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 diff --git a/mlkem/src/native/riscv64/src/rv64v_debug.h b/mlkem/src/native/riscv64/src/rv64v_debug.h index 18d4b123f8..fbedc0663a 100644 --- a/mlkem/src/native/riscv64/src/rv64v_debug.h +++ b/mlkem/src/native/riscv64/src/rv64v_debug.h @@ -7,14 +7,11 @@ #include "../../../debug.h" -#include - /************************************************* * RISC-V Vector Bounds Assertion Macros * - * These macros provide runtime bounds checking for RISC-V vector types - * vint16m1_t and vint16m2_t, following the same pattern as the scalar - * bounds assertions in debug.h + * These macros provide runtime bounds checking for RISC-V vint16m1_t values, + * following the same pattern as the scalar bounds assertions in debug.h. * * The macros are only active when MLKEM_DEBUG is defined, otherwise they * compile to no-ops for zero runtime overhead in release builds. @@ -22,10 +19,14 @@ #if defined(MLKEM_DEBUG) +#include + /** * 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). @@ -34,35 +35,19 @@ */ #define mlk_debug_check_bounds_int16m1 \ MLK_NAMESPACE(mlkem_debug_check_bounds_int16m1) -void mlk_debug_check_bounds_int16m1(const char *file, int line, vint16m1_t vec, - size_t vl, int lower_bound_exclusive, - int upper_bound_exclusive); - -/** - * Check whether values in a vint16m2_t vector are within specified bounds - * by splitting into m1 vectors. - * - * @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. - */ -#define mlk_debug_check_bounds_int16m2 \ - MLK_NAMESPACE(mlkem_debug_check_bounds_int16m2) -void mlk_debug_check_bounds_int16m2(const char *file, int line, vint16m2_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); /* Check bounds in vint16m1_t vector * vec: RISC-V vector of type vint16m1_t * vl: Vector length (number of active elements) * value_lb: Inclusive lower value bound - * value_ub: Exclusive upper value bound */ -#define mlk_assert_bound_int16m1(vec, vl, value_lb, value_ub) \ - mlk_debug_check_bounds_int16m1(__FILE__, __LINE__, (vec), (vl), \ - (value_lb) - 1, (value_ub)) + * value_ub: Exclusive upper bound */ +#define mlk_assert_bound_int16m1(vec, vl, value_lb, value_ub) \ + mlk_debug_check_bounds_int16m1(__FILE__, sizeof(__FILE__), __LINE__, (vec), \ + (vl), (value_lb) - 1, (value_ub)) /* Check absolute bounds in vint16m1_t vector * vec: RISC-V vector of type vint16m1_t @@ -71,27 +56,10 @@ void mlk_debug_check_bounds_int16m2(const char *file, int line, vint16m2_t vec, #define mlk_assert_abs_bound_int16m1(vec, vl, value_abs_bd) \ mlk_assert_bound_int16m1((vec), (vl), (-(value_abs_bd) + 1), (value_abs_bd)) -/* Check bounds in vint16m2_t vector - * vec: RISC-V vector of type vint16m2_t - * vl: Vector length (number of active elements per m1 half) - * value_lb: Inclusive lower value bound - * value_ub: Exclusive upper value bound */ -#define mlk_assert_bound_int16m2(vec, vl, value_lb, value_ub) \ - mlk_debug_check_bounds_int16m2(__FILE__, __LINE__, (vec), (vl), \ - (value_lb) - 1, (value_ub)) - -/* Check absolute bounds in vint16m2_t vector - * vec: RISC-V vector of type vint16m2_t - * vl: Vector length (number of active elements per m1 half) - * value_abs_bd: Exclusive absolute upper bound */ -#define mlk_assert_abs_bound_int16m2(vec, vl, value_abs_bd) \ - mlk_assert_bound_int16m2((vec), (vl), (-(value_abs_bd) + 1), (value_abs_bd)) - #elif defined(CBMC) -/* For CBMC, we would need to implement vector bounds checking using CBMC - * primitives This is complex and would require extracting vector elements, so - * for now we provide empty implementations that could be extended later */ +/* CBMC does not model scalable RVV vector types, so callers containing vector + * operations cannot be compiled by CBMC. */ #define mlk_assert_bound_int16m1(vec, vl, value_lb, value_ub) \ do \ { \ @@ -102,19 +70,9 @@ void mlk_debug_check_bounds_int16m2(const char *file, int line, vint16m2_t vec, { \ } while (0) -#define mlk_assert_bound_int16m2(vec, vl, value_lb, value_ub) \ - do \ - { \ - } while (0) - -#define mlk_assert_abs_bound_int16m2(vec, vl, value_abs_bd) \ - do \ - { \ - } while (0) - #else /* !MLKEM_DEBUG && CBMC */ -/* When debugging is disabled, all assertions become no-ops */ +/* When debugging is disabled, all assertions become no-ops. */ #define mlk_assert_bound_int16m1(vec, vl, value_lb, value_ub) \ do \ { \ @@ -125,16 +83,6 @@ void mlk_debug_check_bounds_int16m2(const char *file, int line, vint16m2_t vec, { \ } while (0) -#define mlk_assert_bound_int16m2(vec, vl, value_lb, value_ub) \ - do \ - { \ - } while (0) - -#define mlk_assert_abs_bound_int16m2(vec, vl, value_abs_bd) \ - do \ - { \ - } while (0) - #endif /* !MLKEM_DEBUG && !CBMC */ #endif /* !MLK_NATIVE_RISCV64_SRC_RV64V_DEBUG_H */ diff --git a/proofs/cbmc/debug_check_bounds/Makefile b/proofs/cbmc/debug_check_bounds/Makefile index 74c0e1c227..4aa6a9e363 100644 --- a/proofs/cbmc/debug_check_bounds/Makefile +++ b/proofs/cbmc/debug_check_bounds/Makefile @@ -6,7 +6,7 @@ include ../Makefile_params.common HARNESS_ENTRY = harness HARNESS_FILE = debug_check_bounds_harness -PROOF_UID = mlk_debug_check_bounds_report +PROOF_UID = mlk_debug_check_bounds DEFINES += -DMLKEM_DEBUG @@ -21,16 +21,15 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/src/debug.c -CHECK_FUNCTION_CONTRACTS = mlk_debug_check_bounds_report \ - mlk_mlkem_debug_check_bounds -USE_FUNCTION_CONTRACTS = +CHECK_FUNCTION_CONTRACTS = mlk_mlkem_debug_check_bounds +USE_FUNCTION_CONTRACTS = mlk_debug_check_bounds_report APPLY_LOOP_CONTRACTS = on USE_DYNAMIC_FRAMES = 1 CBMC_SUPPORTED_CONFIGS = LP64:z3 ILP32:z3 CBMC_DEFAULT_CONFIG = LP64:z3 -FUNCTION_NAME = mlk_debug_check_bounds_report +FUNCTION_NAME = mlk_debug_check_bounds CBMC_OBJECT_BITS = 8 diff --git a/proofs/cbmc/debug_check_bounds_report/Makefile b/proofs/cbmc/debug_check_bounds_report/Makefile new file mode 100644 index 0000000000..04ebea51b3 --- /dev/null +++ b/proofs/cbmc/debug_check_bounds_report/Makefile @@ -0,0 +1,36 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = debug_check_bounds_report_harness + +PROOF_UID = mlk_debug_check_bounds_report + +DEFINES += -DMLKEM_DEBUG + +# Use native stdio declarations that match CBMC's libc model. The data-model +# stdlib.h supplies declarations for the linked libc models. +COMPILE_FLAGS = -Wall -Werror --native-compiler gcc \ + -I$(PROOF_INCLUDE) $(GOTO_CC_DM_FLAG) + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/debug.c + +CHECK_FUNCTION_CONTRACTS = mlk_debug_check_bounds_report +USE_FUNCTION_CONTRACTS = +APPLY_LOOP_CONTRACTS = on +USE_DYNAMIC_FRAMES = 1 + +CBMC_SUPPORTED_CONFIGS = LP64:z3 ILP32:z3 +CBMC_DEFAULT_CONFIG = LP64:z3 + +FUNCTION_NAME = mlk_debug_check_bounds_report + +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/debug_check_bounds_report/debug_check_bounds_report_harness.c b/proofs/cbmc/debug_check_bounds_report/debug_check_bounds_report_harness.c new file mode 100644 index 0000000000..2a07c2f730 --- /dev/null +++ b/proofs/cbmc/debug_check_bounds_report/debug_check_bounds_report_harness.c @@ -0,0 +1,24 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +#include "debug.h" + +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); + +void harness(void) +{ + const char *file; + size_t file_len; + int line; + const int16_t *ptr; + unsigned len; + int lower_bound_exclusive; + int upper_bound_exclusive; + + mlk_debug_check_bounds_report(file, file_len, line, ptr, len, + lower_bound_exclusive, upper_bound_exclusive); +} From e76f0dc68beb46fc757d515541be67eb21658aab Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 19 Oct 2026 20:50:41 +0100 Subject: [PATCH 3/3] CBMC: Include scalar debug helpers in coverage docs The README excludes all debug code from the CBMC safety claim, even though dedicated proofs now cover the scalar helpers. Remove that exclusion from both coverage statements. State in `SOUNDNESS.md` that the proofs use libc models which do not parse `fprintf` formats or inspect variadic arguments, and therefore do not establish safety or output behavior of real formatted diagnostics. Signed-off-by: Hanno Becker --- README.md | 4 ++-- SOUNDNESS.md | 4 ++++ 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 12b03f75d2..f4a7386564 100644 --- a/README.md +++ b/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. diff --git a/SOUNDNESS.md b/SOUNDNESS.md index 692f2db9dd..5558d82a62 100644 --- a/SOUNDNESS.md +++ b/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