Skip to content

Commit 764b4e0

Browse files
hanno-beckerhanno-becker
committed
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 #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 was misleading and unsound for any future use beyond UINT32_MAX. Make the limitation explicit rather than widening the quantifier (which prior experiments showed blows up SMT proof times for size_t-quantified formulas): - Declare the quantified variable as `uint32_t` (was `unsigned`). - 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). - Change the loop counters in mlk_ct_memcmp and mlk_ct_cmov_zero to `uint32_t` to make the index width explicit at the use site. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
1 parent 57d18f4 commit 764b4e0

2 files changed

Lines changed: 31 additions & 19 deletions

File tree

‎mlkem/src/cbmc.h‎

Lines changed: 28 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -80,24 +80,36 @@
8080
* Quantifiers
8181
* Note that the range on qvar is _exclusive_ between qvar_lb .. qvar_ub
8282
* https://diffblue.github.io/cbmc/contracts-quantifiers.html
83+
*
84+
* The quantified variable is declared as uint32_t, so these macros
85+
* quantify only over indices in [0, UINT32_MAX). Bounds larger than
86+
* UINT32_MAX (4 GiB) are NOT supported: the explicit (uint32_t) casts
87+
* on the bounds will trigger CBMC's conversion check if a wider bound
88+
* (e.g. a size_t > UINT32_MAX) is passed.
89+
*
90+
* Quantifying over size_t (64-bit) was found to blow up SMT proof
91+
* times, so we deliberately keep the index width at 32 bits. Callers
92+
* dealing with size_t-typed buffers must add an explicit
93+
* requires(len <= UINT32_MAX)
94+
* precondition.
8395
*/
8496

8597
/*
8698
* Prevent clang-format from corrupting CBMC's special ==> operator
8799
*/
88100
/* clang-format off */
89-
#define forall(qvar, qvar_lb, qvar_ub, predicate) \
90-
__CPROVER_forall \
91-
{ \
92-
unsigned qvar; \
93-
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> (predicate) \
101+
#define forall(qvar, qvar_lb, qvar_ub, predicate) \
102+
__CPROVER_forall \
103+
{ \
104+
uint32_t qvar; \
105+
((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> (predicate) \
94106
}
95107

96-
#define exists(qvar, qvar_lb, qvar_ub, predicate) \
97-
__CPROVER_exists \
98-
{ \
99-
unsigned qvar; \
100-
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) && (predicate) \
108+
#define exists(qvar, qvar_lb, qvar_ub, predicate) \
109+
__CPROVER_exists \
110+
{ \
111+
uint32_t qvar; \
112+
((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) && (predicate) \
101113
}
102114
/* clang-format on */
103115

@@ -126,8 +138,8 @@
126138
value_lb, value_ub) \
127139
__CPROVER_forall \
128140
{ \
129-
unsigned qvar; \
130-
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \
141+
uint32_t qvar; \
142+
((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> \
131143
(((int)(value_lb) <= ((array_var)[(qvar)])) && \
132144
(((array_var)[(qvar)]) < (int)(value_ub))) \
133145
}
@@ -139,8 +151,8 @@
139151
#define array_unchanged_core(qvar, qvar_lb, qvar_ub, array_var) \
140152
__CPROVER_forall \
141153
{ \
142-
unsigned qvar; \
143-
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \
154+
uint32_t qvar; \
155+
((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> \
144156
((array_var)[(qvar)]) == (old(* (int16_t (*)[(qvar_ub)])(array_var)))[(qvar)] \
145157
}
146158

@@ -150,8 +162,8 @@
150162
#define array_unchanged_u64_core(qvar, qvar_lb, qvar_ub, array_var) \
151163
__CPROVER_forall \
152164
{ \
153-
unsigned qvar; \
154-
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \
165+
uint32_t qvar; \
166+
((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> \
155167
((array_var)[(qvar)]) == (old(* (uint64_t (*)[(qvar_ub)])(array_var)))[(qvar)] \
156168
}
157169

‎mlkem/src/verify.h‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -333,7 +333,7 @@ __contract__(
333333
ensures((return_value == 0) == forall(i, 0, len, (a[i] == b[i]))))
334334
{
335335
uint8_t r = 0, s = 0;
336-
unsigned i;
336+
uint32_t i;
337337

338338
for (i = 0; i < len; i++)
339339
__loop__(
@@ -376,13 +376,13 @@ __contract__(
376376
static MLK_INLINE void mlk_ct_cmov_zero(uint8_t *r, const uint8_t *x,
377377
size_t len, uint8_t b)
378378
__contract__(
379-
requires(len <= MLK_MAX_BUFFER_SIZE)
379+
requires(len <= UINT32_MAX)
380380
requires(memory_no_alias(r, len))
381381
requires(memory_no_alias(x, len))
382382
assigns(memory_slice(r, len))
383383
ensures(forall(i, 0, len, (r[i] == (b == 0 ? x[i] : old(r)[i])))))
384384
{
385-
size_t i;
385+
uint32_t i;
386386
for (i = 0; i < len; i++)
387387
__loop__(
388388
invariant(i <= len)

0 commit comments

Comments
 (0)