unbound proof, issue with appendblock loop invariant

CBMC/proofs/Makefile-project-defines

@@ -41,7 +41,7 @@ CBMC_DEFAULT_UNWIND ?= --unwind 16
 
 USE_DYNAMIC_FRAMES ?= --dfcc
 APPLY_LOOP_CONTRACTS ?= --apply-loop-contracts
-#USE_EXTERNAL_SAT_SOLVER = --smt2
+USE_EXTERNAL_SAT_SOLVER = #--smt2
 # Preprocessor include paths -I...
 # Consider adding
      INCLUDES += -I$(SRCDIR)/inc

CBMC/proofs/Makefile.common

@@ -326,7 +326,7 @@ DEFINES ?=
 # object size to be CBMC_MAX_OBJECT_SIZE.  You are likely to get
 # unexpected results if you try to malloc an object larger than this
 # bound.
-CBMC_OBJECT_BITS ?= 8
+CBMC_OBJECT_BITS ?= 16
 
 # CBMC loop unwinding (Normally set in the proof Makefile)
 #
@@ -435,7 +435,7 @@ CODE_CONTRACTS := $(CHECK_FUNCTION_CONTRACTS)$(USE_FUNCTION_CONTRACTS)$(APPLY_LO
 # Proof writers may also apply function contracts using the Dynamic Frame
 # Condition Checking (DFCC) mode. For more information on DFCC,
 # please see https://diffblue.github.io/cbmc/contracts-dev-spec-dfcc.html.
-USE_DYNAMIC_FRAMES ?= --dfcc
+USE_DYNAMIC_FRAMES ?= 
 ifdef USE_DYNAMIC_FRAMES
   ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
     CBMC_USE_DYNAMIC_FRAMES := $(CBMC_OPT_CONFIG_LIBRARY) --dfcc $(HARNESS_ENTRY) $(CBMC_CHECK_FUNCTION_CONTRACTS_REC)
@@ -447,7 +447,7 @@ endif
 # contracts are not reusable and thus are checked and used simultaneously.
 # These contracts are also ignored by default, but may be enabled by setting
 # the APPLY_LOOP_CONTRACTS variable.
-APPLY_LOOP_CONTRACTS ?= --apply-loop-contracts
+APPLY_LOOP_CONTRACTS ?= 
 ifdef APPLY_LOOP_CONTRACTS
   ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),)
     CBMC_APPLY_LOOP_CONTRACTS := --apply-loop-contracts

CBMC/proofs/SymCryptMd2/Makefile

@@ -9,16 +9,15 @@ DEFINES +=
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
-UNWINDSET +=
+#UNWINDSET += SymCryptMd2AppendBlocks.0.5
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/lib/md2.c
 PROJECT_SOURCES += $(SRCDIR)/lib/env_linuxUserMode.c
 PROJECT_SOURCES += $(SRCDIR)/lib/libmain.c
 PROJECT_SOURCES += $(SRCDIR)/lib/hash.c
-#PROOF_SOURCES += $(PROOF_STUB)/memcpy_override.c
 
-CBMC_DEFAULT_UNWIND ?= --unwind 1
+CBMC_DEFAULT_UNWIND ?= --unwind 70
 CBMC_FLAG_MALLOC_MAY_FAIL ?= 
 CBMC_FLAG_MALLOC_FAIL_NULL ?= 
 CBMC_FLAG_BOUNDS_CHECK ?= --bounds-check
@@ -35,6 +34,7 @@ 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
 # 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

CBMC/proofs/SymCryptMd2/SymCryptMd2_harness.c

@@ -16,6 +16,7 @@
  *   - include the types needed to declare function arguments
  */
 #include <stdlib.h>
+#include <string.h>
 #include "symcrypt.h"
 
 
@@ -29,7 +30,7 @@ void harness(void)
     SIZE_T cbData; // unconstrained value
     PBYTE pbData;
     BYTE abResult[SYMCRYPT_MD2_RESULT_SIZE];
-    __CPROVER_assume(cbData <= 8);
+    __CPROVER_assume(cbData <= 64);
     pbData = malloc( cbData );
 
     __CPROVER_assume(pbData != NULL);
@@ -45,19 +46,21 @@ 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( __CPROVER_typed_target(i), __CPROVER_object_upto(p, cbData) )
+    __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;
     }
-
+    */
 }

lib/libmain.c

@@ -207,6 +207,9 @@ SymCryptXorBytes(
     else
     {
         while( cbBytes >= 8 )
+        __CPROVER_assigns(pbResult, pbSrc1, pbSrc2, cbBytes)
+        __CPROVER_loop_invariant( cbBytes >= 0 )
+        __CPROVER_decreases( cbBytes )
         {
             *(UINT64 *)pbResult = *(UINT64 *)pbSrc1 ^ *(UINT64 *)pbSrc2;
             pbSrc1 += 8;
@@ -216,6 +219,9 @@ SymCryptXorBytes(
         }
 
         while( cbBytes > 0 )
+        __CPROVER_assigns(pbResult, pbSrc1, pbSrc2, cbBytes)
+        __CPROVER_loop_invariant( cbBytes >= 0 )
+        __CPROVER_decreases( cbBytes )
         {
             *pbResult = *pbSrc1 ^ *pbSrc2;
             pbResult++;

lib/md2.c

@@ -116,7 +116,8 @@ SymCryptMd2Result(  _Inout_                                 PSYMCRYPT_MD2_STATE
     //
     // The buffer is never completely full, so it is easy to compute the actual padding.
     //
-    SIZE_T tmp;
+    SIZE_T tmp; 
+    __CPROVER_assert(state->bytesInBuffer <= 16, "hash buffer length should always <= 16");
     SIZE_T paddingBytes = 16 - state->bytesInBuffer;
 
 
@@ -157,6 +158,10 @@ SymCryptMd2AppendBlocks(
     int j,k;
 
     while( cbData >= SYMCRYPT_MD2_INPUT_BLOCK_SIZE )
+    __CPROVER_assigns(t, j, k, cbData, pbData, __CPROVER_object_whole(pChain->C), __CPROVER_object_whole(pChain->X))
+    __CPROVER_loop_invariant( cbData % 16 == __CPROVER_loop_entry( cbData ) % 16 && __CPROVER_same_object(pbData, __CPROVER_loop_entry(pbData)))
+    __CPROVER_loop_invariant( __CPROVER_POINTER_OFFSET(pbData)+ cbData == __CPROVER_POINTER_OFFSET(__CPROVER_loop_entry(pbData))+ __CPROVER_loop_entry(cbData))
+    __CPROVER_decreases( cbData )
     {
         BYTE L;
         //
@@ -171,8 +176,8 @@ SymCryptMd2AppendBlocks(
         L = pChain->C[15];
 
         for( j=0; j<16; j++ )
-        __CPROVER_assigns(__CPROVER_typed_target(j), __CPROVER_typed_target(L), __CPROVER_object_whole(pChain->C))
-        __CPROVER_loop_invariant(0 <= j <= 16)
+        __CPROVER_assigns(j, L, __CPROVER_object_whole(pChain->C))
+        __CPROVER_loop_invariant(0 <= j && j <= 16)
         __CPROVER_decreases(18 - j)
         {
             pChain->C[j] = L = pChain->C[j] ^  SymCryptMd2STable[ L ^ pChain->X[16+j] ];
@@ -185,13 +190,13 @@ SymCryptMd2AppendBlocks(
 
         t = 0;
         for( j=0; j<18; j++ )
-        __CPROVER_assigns(__CPROVER_typed_target(t))
-        __CPROVER_loop_invariant(0 <= j <= 18)
+        __CPROVER_assigns(t, j, k, __CPROVER_object_whole(pChain->X))
+        __CPROVER_loop_invariant(0 <= j && j <= 18)
         __CPROVER_decreases(18 - j)
         {
             for( k=0; k<48; k++ )
-            __CPROVER_assigns(__CPROVER_typed_target(t), __CPROVER_typed_target(k), __CPROVER_object_whole(pChain->X))
-            __CPROVER_loop_invariant(0 <= k <= 48)
+            __CPROVER_assigns(t, k, __CPROVER_object_whole(pChain->X))
+            __CPROVER_loop_invariant(0 <= k && k <= 48 && t < 256)
             __CPROVER_decreases(48 - k)
             {
                 t = pChain->X[k] ^ SymCryptMd2STable[t];

lib/sha256.c

@@ -579,6 +579,9 @@ SymCryptSha256AppendBlocks_ul1(
     UINT32 Wt;
 
     while( cbData >= 64 )
+    __CPROVER_assigns( cbData, round, __CPROVER_object_whole( ah ), __CPROVER_object_whole( pChain->H), __CPROVER_object_whole( W ) )
+    __CPROVER_loop_invariant( cbData <= __CPROVER_loop_entry(cbData) )
+    __CPROVER_decreases( cbData )
     {
         ah[7] = pChain->H[0];
         ah[6] = pChain->H[1];
@@ -615,6 +618,9 @@ SymCryptSha256AppendBlocks_ul1(
         // rounds 16 to 64.
         //
         for( round=16; round<64; round += 16 )
+        __CPROVER_assigns( round,  __CPROVER_object_whole( W ) )
+        __CPROVER_loop_invariant( round <= 64 )
+        __CPROVER_decreases( 64 - round )
         {
             FROUND(  0, round );
             FROUND(  1, round );
@@ -686,11 +692,17 @@ SymCryptSha256AppendBlocks_ul2(
     ha[0] = pChain->H[7];
 
     while( cbData >= 64 )
+    __CPROVER_assigns( cbData, A, B, C, D, T, r, __CPROVER_object_whole( buf ), __CPROVER_object_whole( ha ), __CPROVER_object_whole( W ) )
+    __CPROVER_loop_invariant( cbData <= __CPROVER_loop_entry(cbData) )
+    __CPROVER_decreases( cbData )
     {
         //
         // Capture the input into W[0..15]
         //
         for( r=0; r<16; r++ )
+        __CPROVER_assigns( r, __CPROVER_object_whole( W ) )
+        __CPROVER_loop_invariant( r <= 16 )
+        __CPROVER_decreases( 16 - r )
         {
             W[r] = SYMCRYPT_LOAD_MSBFIRST32( &pbData[ 4*r ] );
         }
@@ -702,6 +714,9 @@ SymCryptSha256AppendBlocks_ul2(
         B = W[14];
         D = W[0];
         for( r=16; r<64; r+= 2 )
+        //__CPROVER_assigns( A, B, C, D, T, r, __CPROVER_whole_object( buf ), __CPROVER_whole_object( ha ), __CPROVER_whole_object( W ) )
+        __CPROVER_loop_invariant(r >= 16 && r%2==0 && r <= 64 && A == W[r-1] && B == W[r - 2] && D == W[r - 16])
+        __CPROVER_decreases( 64 - r )
         {
             // Loop invariant: A=W[r-1], B = W[r-2], D = W[r-16]
 
@@ -728,6 +743,9 @@ SymCryptSha256AppendBlocks_ul2(
         D = ha[4];
 
         for( r=0; r<64; r += 4 )
+        //__CPROVER_assigns( A, B, C, D, T, r, __CPROVER_whole_object( buf ), __CPROVER_whole_object( ha ), __CPROVER_whole_object( W ) )
+        __CPROVER_loop_invariant( r <= 64 && r%4 == 0)
+        __CPROVER_decreases( 64 - r )
         {
             //
             // Loop invariant: