From 47d4a365ebb7240d0d1ad69d4b1e9b463bf5c260 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Fri, 15 May 2026 04:48:43 +0100 Subject: [PATCH] CBMC: Document and enforce 4 GiB limit of forall/exists quantifiers Acknowledgements: Thanks to @nmouha for identifying this issue. The forall/exists macros in cbmc.h declared the quantified variable as `unsigned`, which on 64-bit platforms is 32 bits wide. When applied to a size_t bound, this silently truncated the upper bound: the quantifier only ranged over indices up to UINT32_MAX rather than the full size_t range, leaving the predicate unchecked for any larger indices. This was demonstrated by @nmouha in pq-code-package/mlkem-native#1690 with a contrived bug in mlk_ct_cmov_zero that corrupts the buffer at i == 2^32 yet still passes CBMC under the old macros. mlkem-native itself never operates on buffers that large, so no real bug is masked, but the quantifier definition is still highly misleading and could mask real bugs in the future. For now, make the limitation explicit rather than widening the quantifier: - Explicitly cast the lower and upper bounds to `uint32_t`, so passing a wider bound triggers CBMC's conversion check rather than silently truncating. - Tighten mlk_ct_cmov_zero's precondition from MLK_MAX_BUFFER_SIZE to UINT32_MAX (the only size_t-bounded buffer in mlkem-native that participates in a quantified contract). - Declare the quantified variable as `uint32_t` (was `unsigned`) as a robustness improvement towards the implementation-defined size of `unsigned`. We may still want to consider widening the quantifier variable as a follow-up, but this is a more intrusive change that prior experiments have proved to significantly impact proof performance. Signed-off-by: Hanno Becker --- mlkem/src/cbmc.h | 44 ++++++++++++++++++++++++++++---------------- mlkem/src/verify.h | 2 +- 2 files changed, 29 insertions(+), 17 deletions(-) diff --git a/mlkem/src/cbmc.h b/mlkem/src/cbmc.h index 80e1a36fc..a6f6fa768 100644 --- a/mlkem/src/cbmc.h +++ b/mlkem/src/cbmc.h @@ -80,24 +80,36 @@ * Quantifiers * Note that the range on qvar is _exclusive_ between qvar_lb .. qvar_ub * https://diffblue.github.io/cbmc/contracts-quantifiers.html + * + * The quantified variable is declared as uint32_t, so these macros + * quantify only over indices in [0, UINT32_MAX). Bounds larger than + * UINT32_MAX (4 GiB) are NOT supported: the explicit (uint32_t) casts + * on the bounds will trigger CBMC's conversion check if a wider bound + * (e.g. a size_t > UINT32_MAX) is passed. + * + * Quantifying over size_t (64-bit) was found to blow up SMT proof + * times, so we deliberately keep the index width at 32 bits. Callers + * dealing with size_t-typed buffers must add an explicit + * requires(len <= UINT32_MAX) + * precondition. */ /* * Prevent clang-format from corrupting CBMC's special ==> operator */ /* clang-format off */ -#define forall(qvar, qvar_lb, qvar_ub, predicate) \ - __CPROVER_forall \ - { \ - unsigned qvar; \ - ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> (predicate) \ +#define forall(qvar, qvar_lb, qvar_ub, predicate) \ + __CPROVER_forall \ + { \ + uint32_t qvar; \ + ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> (predicate) \ } -#define exists(qvar, qvar_lb, qvar_ub, predicate) \ - __CPROVER_exists \ - { \ - unsigned qvar; \ - ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) && (predicate) \ +#define exists(qvar, qvar_lb, qvar_ub, predicate) \ + __CPROVER_exists \ + { \ + uint32_t qvar; \ + ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) && (predicate) \ } /* clang-format on */ @@ -126,8 +138,8 @@ value_lb, value_ub) \ __CPROVER_forall \ { \ - unsigned qvar; \ - ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \ + uint32_t qvar; \ + ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> \ (((int)(value_lb) <= ((array_var)[(qvar)])) && \ (((array_var)[(qvar)]) < (int)(value_ub))) \ } @@ -139,8 +151,8 @@ #define array_unchanged_core(qvar, qvar_lb, qvar_ub, array_var) \ __CPROVER_forall \ { \ - unsigned qvar; \ - ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \ + uint32_t qvar; \ + ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> \ ((array_var)[(qvar)]) == (old(* (int16_t (*)[(qvar_ub)])(array_var)))[(qvar)] \ } @@ -150,8 +162,8 @@ #define array_unchanged_u64_core(qvar, qvar_lb, qvar_ub, array_var) \ __CPROVER_forall \ { \ - unsigned qvar; \ - ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \ + uint32_t qvar; \ + ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> \ ((array_var)[(qvar)]) == (old(* (uint64_t (*)[(qvar_ub)])(array_var)))[(qvar)] \ } diff --git a/mlkem/src/verify.h b/mlkem/src/verify.h index 600afa44a..9c3a40482 100644 --- a/mlkem/src/verify.h +++ b/mlkem/src/verify.h @@ -376,7 +376,7 @@ __contract__( static MLK_INLINE void mlk_ct_cmov_zero(uint8_t *r, const uint8_t *x, size_t len, uint8_t b) __contract__( - requires(len <= MLK_MAX_BUFFER_SIZE) + requires(len <= UINT32_MAX) requires(memory_no_alias(r, len)) requires(memory_no_alias(x, len)) assigns(memory_slice(r, len))