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

BIBLIOGRAPHY.md

@@ -39,6 +39,7 @@ source code and documentation.
   - [integration/liboqs/config_x86_64.h](integration/liboqs/config_x86_64.h)
   - [mldsa/mldsa_native_config.h](mldsa/mldsa_native_config.h)
   - [mldsa/src/sign.c](mldsa/src/sign.c)
+  - [proofs/cbmc/mldsa_native_config_cbmc.h](proofs/cbmc/mldsa_native_config_cbmc.h)
   - [test/break_pct_config.h](test/break_pct_config.h)
   - [test/custom_heap_alloc_config.h](test/custom_heap_alloc_config.h)
   - [test/custom_memcpy_config.h](test/custom_memcpy_config.h)
@@ -94,6 +95,7 @@ source code and documentation.
   - [mldsa/src/rounding.h](mldsa/src/rounding.h)
   - [mldsa/src/sign.c](mldsa/src/sign.c)
   - [mldsa/src/sign.h](mldsa/src/sign.h)
+  - [proofs/cbmc/mldsa_native_config_cbmc.h](proofs/cbmc/mldsa_native_config_cbmc.h)
   - [test/break_pct_config.h](test/break_pct_config.h)
   - [test/custom_memcpy_config.h](test/custom_memcpy_config.h)
   - [test/custom_memset_config.h](test/custom_memset_config.h)

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
@@ -555,6 +555,7 @@ ifndef MLD_CONFIG_PARAMETER_SET
     $(error MLD_CONFIG_PARAMETER_SET not set)
 endif
 
+DEFINES += -DMLD_CONFIG_FILE="\"mldsa_native_config_cbmc.h\""
 DEFINES += -DMLD_CONFIG_PARAMETER_SET=$(MLD_CONFIG_PARAMETER_SET)
 # Give visibility to all static functions
 DEFINES += -Dstatic=

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/crypto_sign_signature_internal/Makefile

@@ -46,7 +46,7 @@ FUNCTION_NAME = crypto_sign_signature_internal
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 8
+CBMC_OBJECT_BITS = 9
 
 # If you require access to a file-local ("static") function or object to conduct
 # your proof, set the following (and do not include the original source file