Introduce explicit upper bounds on lengths of

input and output buffers where appropriate.

Force CBMC to use --malloc-fail-assert for
all proofs to remove assumption on buffer lengths.

Update autogenerated files following this change.

Update Proof Guide with notes on max buffer size

Signed-off-by: Rod Chapman <rodchap@amazon.com>

Author: rod-chapman

mlkem/src/cbmc.h

@@ -8,14 +8,15 @@
 /***************************************************
  * Basic replacements for __CPROVER_XXX contracts
  ***************************************************/
-
 #ifndef CBMC
 
 #define __contract__(x)
 #define __loop__(x)
 
 #else /* !CBMC */
 
+#include <stdint.h>
+
 #define __contract__(x) x
 #define __loop__(x) x
 
@@ -59,6 +60,17 @@
 #define readable(...) __CPROVER_r_ok(__VA_ARGS__)
 #define writeable(...) __CPROVER_w_ok(__VA_ARGS__)
 
+/* Maximum supported buffer size
+ *
+ * Larger buffers may be supported, but due to internal modeling constraints
+ * in CBMC, the proofs of memory- and type-safety won't be able to run.
+ *
+ * If you find yourself in need for a buffer size larger than this,
+ * please contact the maintainers, so we can prioritize work to relax
+ * this somewhat artificial bound.
+ */
+#define MLK_MAX_BUFFER_SIZE (SIZE_MAX >> 12)
+
 /*
  * History variables
  * https://diffblue.github.io/cbmc/contracts-history-variables.html

mlkem/src/fips202/fips202.c

@@ -60,6 +60,7 @@
 static void mlk_keccak_absorb_once(uint64_t *s, uint32_t r, const uint8_t *m,
                                    size_t mlen, uint8_t p)
 __contract__(
+    requires(mlen <= MLK_MAX_BUFFER_SIZE)
     requires(r <= sizeof(uint64_t) * MLK_KECCAK_LANES)
     requires(memory_no_alias(s, sizeof(uint64_t) * MLK_KECCAK_LANES))
     requires(memory_no_alias(m, mlen))
@@ -153,6 +154,7 @@ __contract__(
 static void mlk_keccak_squeeze_once(uint8_t *h, size_t outlen, uint64_t *s,
                                     uint32_t r)
 __contract__(
+    requires(outlen <= MLK_MAX_BUFFER_SIZE)
     requires(r <= sizeof(uint64_t) * MLK_KECCAK_LANES)
     requires(memory_no_alias(s, sizeof(uint64_t) * MLK_KECCAK_LANES))
     requires(memory_no_alias(h, outlen))

mlkem/src/fips202/fips202.h

@@ -47,6 +47,7 @@ typedef struct
 void mlk_shake128_absorb_once(mlk_shake128ctx *state, const uint8_t *input,
                               size_t inlen)
 __contract__(
+  requires(inlen <= MLK_MAX_BUFFER_SIZE)
   requires(memory_no_alias(state, sizeof(mlk_shake128ctx)))
   requires(memory_no_alias(input, inlen))
   assigns(memory_slice(state, sizeof(mlk_shake128ctx)))
@@ -96,6 +97,8 @@ void mlk_shake128_release(mlk_shake128ctx *state);
 void mlk_shake256(uint8_t *output, size_t outlen, const uint8_t *input,
                   size_t inlen)
 __contract__(
+  requires(inlen <= MLK_MAX_BUFFER_SIZE)
+  requires(outlen <= MLK_MAX_BUFFER_SIZE)
   requires(memory_no_alias(input, inlen))
   requires(memory_no_alias(output, outlen))
   assigns(memory_slice(output, outlen))
@@ -116,6 +119,7 @@ __contract__(
  **************************************************/
 void mlk_sha3_256(uint8_t *output, const uint8_t *input, size_t inlen)
 __contract__(
+  requires(inlen <= MLK_MAX_BUFFER_SIZE)
   requires(memory_no_alias(input, inlen))
   requires(memory_no_alias(output, SHA3_256_HASHBYTES))
   assigns(memory_slice(output, SHA3_256_HASHBYTES))
@@ -136,6 +140,7 @@ __contract__(
  **************************************************/
 void mlk_sha3_512(uint8_t *output, const uint8_t *input, size_t inlen)
 __contract__(
+  requires(inlen <= MLK_MAX_BUFFER_SIZE)
   requires(memory_no_alias(input, inlen))
   requires(memory_no_alias(output, SHA3_512_HASHBYTES))
   assigns(memory_slice(output, SHA3_512_HASHBYTES))

mlkem/src/fips202/fips202x4.c

@@ -28,6 +28,7 @@ static void mlk_keccak_absorb_once_x4(uint64_t *s, uint32_t r,
                                       const uint8_t *in2, const uint8_t *in3,
                                       size_t inlen, uint8_t p)
 __contract__(
+  requires(inlen <= MLK_MAX_BUFFER_SIZE)
   requires(memory_no_alias(s, sizeof(uint64_t) * MLK_KECCAK_LANES * MLK_KECCAK_WAY))
   requires(r <= sizeof(uint64_t) * MLK_KECCAK_LANES)
   requires(memory_no_alias(in0, inlen))
@@ -78,7 +79,8 @@ static void mlk_keccak_squeezeblocks_x4(uint8_t *out0, uint8_t *out1,
                                         size_t nblocks, uint64_t *s, uint32_t r)
 __contract__(
     requires(r <= sizeof(uint64_t) * MLK_KECCAK_LANES)
-    requires(nblocks <= 8 /* somewhat arbitrary bound */)
+    requires(r == SHAKE128_RATE || r == SHAKE256_RATE)
+    requires(nblocks <= (MLK_MAX_BUFFER_SIZE / SHAKE256_RATE))
     requires(memory_no_alias(s, sizeof(uint64_t) * MLK_KECCAK_LANES * MLK_KECCAK_WAY))
     requires(memory_no_alias(out0, nblocks * r))
     requires(memory_no_alias(out1, nblocks * r))

mlkem/src/fips202/fips202x4.h

@@ -25,6 +25,7 @@ void mlk_shake128x4_absorb_once(mlk_shake128x4ctx *state, const uint8_t *in0,
                                 const uint8_t *in1, const uint8_t *in2,
                                 const uint8_t *in3, size_t inlen)
 __contract__(
+  requires(inlen <= MLK_MAX_BUFFER_SIZE)
   requires(memory_no_alias(state, sizeof(mlk_shake128x4ctx)))
   requires(memory_no_alias(in0, inlen))
   requires(memory_no_alias(in1, inlen))
@@ -62,7 +63,8 @@ void mlk_shake256x4(uint8_t *out0, uint8_t *out1, uint8_t *out2, uint8_t *out3,
                     size_t outlen, uint8_t *in0, uint8_t *in1, uint8_t *in2,
                     uint8_t *in3, size_t inlen)
 __contract__(
-  requires(outlen <= 8 * SHAKE256_RATE /* somewhat arbitrary bound */)
+  requires(inlen <= MLK_MAX_BUFFER_SIZE)
+  requires(outlen <= MLK_MAX_BUFFER_SIZE)
   requires(memory_no_alias(in0, inlen))
   requires(memory_no_alias(in1, inlen))
   requires(memory_no_alias(in2, inlen))

mlkem/src/verify.h

@@ -318,7 +318,8 @@ __contract__(ensures(return_value == (cond ? a : b)))
  *
  * Arguments:   const uint8_t *a: pointer to first byte array
  *              const uint8_t *b: pointer to second byte array
- *              size_t len:       length of the byte arrays
+ *              size_t len:       length of the byte arrays, upper-bounded
+ *                                to INT_MAX to control proof complexity
  *
  * Returns 0 if the byte arrays are equal, a non-zero value otherwise
  *
@@ -338,9 +339,9 @@ __contract__(ensures(return_value == (cond ? a : b)))
 static MLK_INLINE uint8_t mlk_ct_memcmp(const uint8_t *a, const uint8_t *b,
                                         const size_t len)
 __contract__(
+  requires(len <= INT_MAX)
   requires(memory_no_alias(a, len))
   requires(memory_no_alias(b, len))
-  requires(len <= INT_MAX)
   ensures((return_value == 0) == forall(i, 0, len, (a[i] == b[i]))))
 {
   uint8_t r = 0, s = 0;
@@ -391,6 +392,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(memory_no_alias(r, len))
   requires(memory_no_alias(x, len))
   assigns(memory_slice(r, len)))

proofs/cbmc/Makefile.common

@@ -246,7 +246,7 @@ endif
 #   * an entire project when added to Makefile-project-defines
 #   * a specific proof when added to the harness Makefile
 
-CBMC_FLAG_MALLOC_MAY_FAIL ?= # set to --no-malloc-may-fail to disable
+CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-fail-assert
 CBMC_FLAG_BOUNDS_CHECK ?= # set to --no-bounds-check to disable
 CBMC_FLAG_CONVERSION_CHECK ?= --conversion-check
 CBMC_FLAG_DIV_BY_ZERO_CHECK ?= # set to --no-div-by-zero-check to disable

proofs/cbmc/proof_guide.md

@@ -73,6 +73,41 @@ for some struct `foo`, you cannot pass `&foo[0]`, `&foo[1]` as arguments to a fu
 `memory_no_alias(...)` for both, because `&foo[0]`, `&foo[1]` point to the same object. In mlkem-native, we sometimes
 work around this by manually splitting statically-sized arrays into multiple separate objects.
 
+
+### Maximum buffer sizes
+
+CBMC assumes that allocated objects are less than `__CPROVER_max_malloc_size`
+which is an an internal constant defined to be `SIZE_MAX >> (OBJECT_BITS + 1)`
+for that particular run of CBMC, where `SIZE_MAX` is an implementation-defined
+constant (declared in `stdint.h`) and `OBJECT_BITS` is a command-line parameter
+with value typically in the range 8 .. 12
+
+See the [memory bounds checking](https://diffblue.github.io/cbmc/memory-bounds-checking.html)
+section of the CBMC manual for more details.
+
+Pragmatically, `SIZE_MAX` will either be `2**64-1` or `2**32-1` depending on the
+host platform, and we choose the largest value of `OBJECT_BITS` that is used
+for all proofs in this repository.
+
+This matters where a function takes a formal parameter `p` of some pointer type
+`t` and a `len` parameter of type `size_t` that denotes the number of elements
+pointed to by `p`, and those parameters are subject to a
+`memory_no_alias(p, len * sizeof(t))` contract.
+
+In such cases, len must be explicitly bounded to be less that or equal to
+MLK_MAX_BUFFER_SIZE which might be defined in `cbmc.h` as:
+```c
+#define MLK_MAX_BUFFER_SIZE (SIZE_MAX >> 12)
+```
+and used, for example, as follows:
+```c
+void f(t *p, size_t len)
+__contract__(
+  requires(len * sizeof(t) <= MLK_MAX_BUFFER_SIZE)
+  requires(memory_no_alias(p, len * sizeof(t)))
+);
+```
+
 ### Memory footprint
 
 The most common way to specify memory footprint in `assigns(...)` clauses is via `memory_slice(ptr, len)`. This asserts