unbounded proof object bit 9 unwind 50

microsoft · Jul 23, 2024 · 2dfac45 · 2dfac45
1 parent 8513c6b
commit 2dfac45
Show file tree

Hide file tree

Showing 24 changed files with 89,071 additions and 78 deletions.
diff --git a/CBMC/proofs/Makefile.common b/CBMC/proofs/Makefile.common
@@ -513,7 +513,7 @@ COMMA :=,
 ################################################################
 # Set C compiler defines
 
-#CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
+CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
 #COMPILE_FLAGS += --object-bits $(CBMC_OBJECT_BITS)
 
 DEFINES += -DCBMC=1
@@ -816,7 +816,7 @@ ifdef CBMCFLAGS
   ifeq ($(strip $(CODE_CONTRACTS)),)
     CBMCFLAGS += $(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_OPT_CONFIG_LIBRARY)
   else ifeq ($(strip $(USE_DYNAMIC_FRAMES)),)
-    CBMCFLAGS += $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_OPT_CONFIG_LIBRARY)
+    CBMCFLAGS += $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_OPT_CONFIG_LIBRARY) $(CBMC_DEFAULT_UNWIND)
   endif
 endif
 

diff --git a/CBMC/proofs/SymCryptMd2/Makefile b/CBMC/proofs/SymCryptMd2/Makefile
@@ -17,24 +17,24 @@ PROJECT_SOURCES += $(SRCDIR)/lib/env_linuxUserMode.c
 PROJECT_SOURCES += $(SRCDIR)/lib/libmain.c
 PROJECT_SOURCES += $(SRCDIR)/lib/hash.c
 
-CBMC_DEFAULT_UNWIND ?= --unwind 70
+CBMC_DEFAULT_UNWIND ?= --unwind 50
 CBMC_FLAG_MALLOC_MAY_FAIL ?= 
 CBMC_FLAG_MALLOC_FAIL_NULL ?= 
 CBMC_FLAG_BOUNDS_CHECK ?= --bounds-check
 CBMC_FLAG_CONVERSION_CHECK ?= 
-CBMC_FLAG_MEMORY_LEAK_CHECK ?= 
-CBMC_FLAG_MEMORY_CLEANUP_CHECK ?= 
+CBMC_FLAG_MEMORY_LEAK_CHECK ?= --memory-leak-check
+CBMC_FLAG_MEMORY_CLEANUP_CHECK ?= --memory-cleanup-check
 CBMC_FLAG_DIV_BY_ZERO_CHECK ?= 
 CBMC_FLAG_FLOAT_OVERFLOW_CHECK ?= 
 CBMC_FLAG_NAN_CHECK ?= 
-CBMC_FLAG_POINTER_CHECK ?= 
+CBMC_FLAG_POINTER_CHECK ?= --pointer-check
 CBMC_FLAG_POINTER_OVERFLOW_CHECK ?= 
 CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= 
 CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= 
 CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= 
 CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK ?= 
 CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions
-CBMC_OBJECT_BITS ?= 16
+CBMC_OBJECT_BITS ?= 9
 # If this proof is found to consume huge amounts of RAM, you can set the
 # EXPENSIVE variable. With new enough versions of the proof tools, this will
 # restrict the number of EXPENSIVE CBMC jobs running at once. See the

diff --git a/CBMC/proofs/SymCryptMd2/SymCryptMd2_harness.c b/CBMC/proofs/SymCryptMd2/SymCryptMd2_harness.c
@@ -19,48 +19,40 @@
 #include <string.h>
 #include "symcrypt.h"
 
-
 SYMCRYPT_ENVIRONMENT_LINUX_USERMODE
 /**
  * @brief Starting point for formal analysis
  * 
  */
 void harness(void)
 {
-    SIZE_T cbData; // unconstrained value
-    PBYTE pbData;
+    SIZE_T cbData1; // unconstrained value
+    SIZE_T cbData2;
+    PBYTE pbData1;
+    PBYTE pbData2;
     BYTE abResult[SYMCRYPT_MD2_RESULT_SIZE];
-    __CPROVER_assume(cbData <= 64);
-    pbData = malloc( cbData );
+    pbData1 = malloc( cbData1 );
+    pbData2 = malloc( cbData2 );
 
-    __CPROVER_assume(pbData != NULL);
+    __CPROVER_assume(pbData1 != NULL);
+    __CPROVER_assume(pbData2 != NULL);
 
-    SymCryptMd2( pbData, cbData, abResult );
+    SYMCRYPT_MD2_STATE state;
 
-    free(pbData);
-}
+    SymCryptMd2Init( &state );
+    SymCryptMd2Append( &state, pbData1, cbData1 );
+    SymCryptMd2Append( &state, pbData2, cbData2 );
+    SymCryptMd2Result( &state, abResult );
 
+    free(pbData1);
+    free(pbData2);
+}
 
+// overwrite assembly implementation of SymCryptWipeAsm
 VOID
 SYMCRYPT_CALL
 SymCryptWipeAsm( _Out_writes_bytes_( cbData ) PVOID pbData, SIZE_T cbData )
 {
     volatile BYTE * p = (volatile BYTE *) pbData;
     memset(p, 0, cbData);
-    /*
-    SIZE_T i;
-
-    //__CPROVER_assume( pbData != NULL );
-    //__CPROVER_assume( __CPROVER_w_ok( pbData, cbData ));
-    
-
-    for( i=0; i<cbData; i++ )
-    __CPROVER_assigns( i, __CPROVER_object_upto(p, cbData) )
-    __CPROVER_loop_invariant( i <= cbData )
-    //__CPROVER_loop_invariant(__CPROVER_forall { size_t j; (0 <= j && j < i) ==> p[j] == 0 } )
-    __CPROVER_decreases( cbData - i ) 
-    {
-        p[i] = 0;
-    }
-    */
 }
diff --git a/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness.goto b/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness.goto
diff --git a/CBMC/proofs/SymCryptMd2/md2_result.txt b/CBMC/proofs/SymCryptMd2/md2_result.txt
@@ -0,0 +1,9 @@
+CBMC version 6.0.1 (cbmc-6.0.1) 64-bit x86_64 linux
+Reading GOTO program from file /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness.goto
+Generating GOTO Program
+Adding CPROVER library (x86_64)
+Removal of function pointers and virtual functions
+Generic Property Instrumentation
+Starting Bounded Model Checking
+Passing problem to SMT2 QF_AUFBV using Z3
+converting SSA