CBMC: Use instrumented malloc/free for MLD_ALLOC/MLD_FREE

The default implementation of MLD_ALLOC and MLD_FREE uses stack
allocation, which the compiler can assume not to fail. This means
that CBMC does not exercise the cleanup paths which handle fallible
dynamic allocation -- a significant proof gap.

This commit changes the configuration uses for the CBMC proofs
to use the (instrumented) calls to malloc/free for MLD_ALLOC/MLD_FREE.

Importantly, we set --malloc-may-fail to model allocation as fallible,
and --malloc-fail-null to return NULL in case of allocation failure.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Author: hanno-becker

proofs/cbmc/H/H_harness.c

@@ -9,6 +9,11 @@ void mld_H(uint8_t *out, size_t outlen, const uint8_t *in1, size_t in1len,
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   uint8_t *out;
   size_t outlen;
   const uint8_t *in1;

proofs/cbmc/Makefile.common

@@ -247,7 +247,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 ?= --malloc-fail-assert
+CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-may-fail --malloc-fail-null # alloc may fail with returning NULL
 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/check_pct/Makefile

@@ -10,7 +10,7 @@ HARNESS_FILE = check_pct_harness
 # Litani dashboard. It can be human-readable and contain spaces if you wish.
 PROOF_UID = mld_check_pct
 
-DEFINES += -DMLD_CONFIG_KEYGEN_PCT
+DEFINES +=
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=

proofs/cbmc/compute_pack_z/compute_pack_z_harness.c

@@ -10,6 +10,11 @@ int mld_compute_pack_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *cp,
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   uint8_t *sig;
   mld_poly *cp;
   mld_sk_s1hat *s1;

proofs/cbmc/mldsa_native_config_cbmc.h

@@ -25,11 +25,14 @@
  */
 
 /*
- * Test configuration: mldsa-native configuration used for CBMC proofs
+ * Test configuration: mldsa-native configuration used for CBMC proofs, using
+ * instrumented alloc/free
  *
  * This configuration differs from the default mldsa/mldsa_native_config.h in
  * the following places:
  *   - MLD_CONFIG_NAMESPACE_PREFIX
+ *   - MLD_CONFIG_KEYGEN_PCT
+ *   - MLD_CONFIG_CUSTOM_ALLOC_FREE
  */
 
 
@@ -499,15 +502,13 @@
  * target pointer should simply be set to NULL. The calling
  * code will handle this case and invoke MLD_CUSTOM_FREE.
  */
-/* #define MLD_CONFIG_CUSTOM_ALLOC_FREE
-   #if !defined(__ASSEMBLER__)
-   #include <stdlib.h>
-   #define MLD_CUSTOM_ALLOC(v, T, N)                              \
-     T* (v) = (T *)aligned_alloc(MLD_DEFAULT_ALIGN,               \
-                                 MLD_ALIGN_UP(sizeof(T) * (N)))
-   #define MLD_CUSTOM_FREE(v, T, N) free(v)
-   #endif
-*/
+#define MLD_CONFIG_CUSTOM_ALLOC_FREE
+#if !defined(__ASSEMBLER__)
+#include <stdlib.h>
+#define MLD_CUSTOM_ALLOC(v, T, N) T *v = (T *)malloc(sizeof(T) * (N))
+#define MLD_CUSTOM_FREE(v, T, N) free(v)
+#endif
+
 
 /**
  * MLD_CONFIG_CUSTOM_MEMCPY
@@ -629,7 +630,7 @@
  * and MLD_CONFIG_NO_VERIFY_API as the current PCT implementation
  * requires signature() and verify().
  */
-/* #define MLD_CONFIG_KEYGEN_PCT */
+#define MLD_CONFIG_KEYGEN_PCT
 
 /**
  * MLD_CONFIG_KEYGEN_PCT_BREAKAGE_TEST

proofs/cbmc/prepare_domain_separation_prefix/prepare_domain_separation_prefix_harness.c

@@ -5,6 +5,11 @@
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   uint8_t *prefix;
   const uint8_t *ph;
   size_t phlen;

proofs/cbmc/sample_s1_s2/sample_s1_s2_harness.c

@@ -8,6 +8,11 @@ static void mld_sample_s1_s2(mld_polyvecl *s1, mld_polyveck *s2,
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   mld_polyvecl *s1;
   mld_polyveck *s2;
   uint8_t *seed;

proofs/cbmc/sample_s1_s2_serial/sample_s1_s2_harness.c

@@ -8,6 +8,11 @@ static void mld_sample_s1_s2(mld_polyvecl *s1, mld_polyveck *s2,
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   mld_polyvecl *s1;
   mld_polyveck *s2;
   uint8_t *seed;

proofs/cbmc/sign_attempt/sign_attempt_harness.c

@@ -5,6 +5,11 @@
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   uint16_t attempt;
   int rc;
   /* `context` is consumed by the call macro (the CBMC config has no context

proofs/cbmc/sign_finish/sign_finish_harness.c

@@ -7,6 +7,11 @@
  * parameter), exactly as at the call sites in sign.c. */
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   uint16_t attempt;
   mld_sign_finish(attempt, context);
 }