Unbounded proofs of memory safety (#146)

* Add a CBMC proof harness for multiSearch function

Signed-off-by: Felipe R. Monteiro <[email protected]>

* Make all CBMC proofs unbounded

Signed-off-by: Felipe R. Monteiro <[email protected]>

* Make coreJSON more verification friendly

In order to turn all bounded CBMC proofs into unbounded proofs,
we must make some small changes to coreJSON. Basically, we want
to avoid uninitialized variables (CBMC sees them as non-deterministic
values) and make sure the code in loops is resilient enough when
working with inputs of arbitrary size. The latter is important
because we must annotate all loops with loop invariants.
The implementation should work together with these annotations
in order to prove memory safety for inputs of arbitrary size.

Signed-off-by: Felipe R. Monteiro <[email protected]>

* Include patch with loop invariants

Modify existing CBMC proofs to remove any assumptions over the size
of the input (a.k.a. bound). Instrument all loops with Hoare-style
loop invariants and assigns clauses (define the modified memory
within a loop), which CBMC uses to prove correctness. Annotate all
loops using decreases clauses, which CBMC uses to prove termination.

Signed-off-by: Felipe R. Monteiro <[email protected]>

* Add patch for loop invariants in CI

Signed-off-by: Felipe R. Monteiro <[email protected]>

---------

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

.github/workflows/ci.yml

@@ -161,3 +161,4 @@ jobs:
         uses: FreeRTOS/CI-CD-Github-Actions/run_cbmc@main
         with:
           proofs_dir: test/cbmc/proofs
+          run_cbmc_proofs_command: cd ../../../; git apply -v loop_invariants.patch; cd test/cbmc/proofs; ./run-cbmc-proofs.py

loop_invariants.patch

@@ -0,0 +1,202 @@
+diff --git a/source/core_json.c b/source/core_json.c
+index 901b2e1..8bdd89c 100644
+--- a/source/core_json.c
++++ b/source/core_json.c
+@@ -62,6 +62,21 @@ typedef union
+ #define isSquareOpen_( x )            ( ( x ) == '[' )
+ #define isSquareClose_( x )           ( ( x ) == ']' )
+ 
++/**
++ * Renaming all loop-contract clauses from CBMC for readability.
++ * For more information about loop contracts in CBMC, see
++ * https://diffblue.github.io/cbmc/contracts-user.html.
++ */
++#ifdef CBMC
++#define loopInvariant(...)            __CPROVER_loop_invariant(__VA_ARGS__)
++#define decreases(...)             __CPROVER_decreases(__VA_ARGS__)
++#define assigns(...)             __CPROVER_assigns(__VA_ARGS__)
++#else
++#define loopInvariant(...)
++#define decreases(...)
++#define assigns(...)
++#endif
++
+ /**
+  * @brief Advance buffer index beyond whitespace.
+  *
+@@ -78,6 +93,9 @@ static void skipSpace( const char * buf,
+     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
+ 
+     for( i = *start; i < max; i++ )
++    assigns( i )
++    loopInvariant( *start <= i && i <= max )
++    decreases( max - i )
+     {
+         if( !isspace_( buf[ i ] ) )
+         {
+@@ -102,6 +120,13 @@ static size_t countHighBits( uint8_t c )
+     size_t i = 0;
+ 
+     while( ( n & 0x80U ) != 0U )
++    assigns( i, n )
++    loopInvariant (
++        ( 0U <= i ) && ( i <= 8U )
++        && ( n == ( c & ( 0xFF >> i ) ) << i )
++        && ( ( ( c >> ( 8U - i ) ) + 1U ) == ( 1U << i ) )
++    )
++    decreases( 8U - i )
+     {
+         i++;
+         n = ( n & 0x7FU ) << 1U;
+@@ -210,6 +235,13 @@ static bool skipUTF8MultiByte( const char * buf,
+         /* The bit count is 1 greater than the number of bytes,
+          * e.g., when j is 2, we skip one more byte. */
+         for( j = bitCount - 1U; j > 0U; j-- )
++        assigns( j, i, value, c.c )
++        loopInvariant(
++            ( 0 <= j ) && ( j <= bitCount - 1 )
++            && ( *start <= i ) && ( i <= max )
++            && ( ( i == max ) ==> ( j > 0 ) )
++        )
++        decreases( j )
+         {
+             i++;
+ 
+@@ -345,6 +377,12 @@ static bool skipOneHexEscape( const char * buf,
+     if( ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) )
+     {
+         for( i += 2U; i < end; i++ )
++        assigns( value, i )
++        loopInvariant(
++            ( *start + 2U <= i ) && ( i <= end ) &&
++            ( 0U <= value ) && ( value < ( 1U << ( 4U * ( i - ( 2U + *start ) ) ) ) )
++        )
++        decreases( end - i )
+         {
+             uint8_t n = hexToInt( buf[ i ] );
+ 
+@@ -522,6 +560,9 @@ static bool skipString( const char * buf,
+         i++;
+ 
+         while( i < max )
++        assigns( i )
++        loopInvariant( *start + 1U <= i && i <= max )
++        decreases( max - i )
+         {
+             if( buf[ i ] == '"' )
+             {
+@@ -580,6 +621,9 @@ static bool strnEq( const char * a,
+     assert( ( a != NULL ) && ( b != NULL ) );
+ 
+     for( i = 0; i < n; i++ )
++    assigns( i )
++    loopInvariant( i <= n )
++    decreases( n - i )
+     {
+         if( a[ i ] != b[ i ] )
+         {
+@@ -681,6 +725,7 @@ static bool skipAnyLiteral( const char * buf,
+  * false otherwise.
+  */
+ #define MAX_FACTOR    ( MAX_INDEX_VALUE / 10 )
++
+ static bool skipDigits( const char * buf,
+                         size_t * start,
+                         size_t max,
+@@ -695,6 +740,9 @@ static bool skipDigits( const char * buf,
+     saveStart = *start;
+ 
+     for( i = *start; i < max; i++ )
++    assigns( value, i )
++    loopInvariant( *start <= i && i <= max )
++    decreases( max - i )
+     {
+         if( !isdigit_( buf[ i ] ) )
+         {
+@@ -944,6 +992,9 @@ static void skipArrayScalars( const char * buf,
+     i = *start;
+ 
+     while( i < max )
++    assigns( i )
++    loopInvariant( *start <= i && i <= max )
++    decreases( max - i )
+     {
+         if( skipAnyScalar( buf, &i, max ) != true )
+         {
+@@ -986,6 +1037,13 @@ static void skipObjectScalars( const char * buf,
+     i = *start;
+ 
+     while( i < max )
++    assigns( i, *start, comma )
++    loopInvariant(
++        i >= *start
++        && __CPROVER_loop_entry( i ) <= i && i <= max
++        && __CPROVER_loop_entry( *start ) <= *start && *start <= max
++    )
++    decreases( max - i )
+     {
+         if( skipString( buf, &i, max ) != true )
+         {
+@@ -1082,6 +1140,14 @@ static JSONStatus_t skipCollection( const char * buf,
+     i = *start;
+ 
+     while( i < max )
++    assigns( i, depth, c, __CPROVER_object_whole( stack ), ret )
++    loopInvariant(
++        -1 <= depth && depth <= JSON_MAX_DEPTH
++        && *start <= i && i <= max
++        && ( ( ret == JSONSuccess ) ==> i >= *start + 2U )
++        && ( ret == JSONSuccess || ret == JSONPartial || ret == JSONIllegalDocument || ret == JSONMaxDepthExceeded )
++    )
++    decreases( max - i )
+     {
+         c = buf[ i ];
+         i++;
+@@ -1363,6 +1429,9 @@ static bool objectSearch( const char * buf,
+         skipSpace( buf, &i, max );
+ 
+         while( i < max )
++        assigns( i, key, keyLength, value, valueLength )
++        loopInvariant( __CPROVER_loop_entry( i ) <= i && i <= max )
++        decreases( max - i )
+         {
+             if( nextKeyValuePair( buf, &i, max, &key, &keyLength,
+                                   &value, &valueLength ) != true )
+@@ -1430,6 +1499,9 @@ static bool arraySearch( const char * buf,
+         skipSpace( buf, &i, max );
+ 
+         while( i < max )
++        assigns( i, currentIndex, value, valueLength )
++        loopInvariant( __CPROVER_loop_entry( i ) <= i && i <= max && currentIndex < i )
++        decreases( max - i )
+         {
+             if( nextValue( buf, &i, max, &value, &valueLength ) != true )
+             {
+@@ -1495,6 +1567,9 @@ static bool skipQueryPart( const char * buf,
+     while( ( i < max ) &&
+            !isSeparator_( buf[ i ] ) &&
+            !isSquareOpen_( buf[ i ] ) )
++    assigns( i )
++    loopInvariant( i  <= max )
++    decreases( max - i )
+     {
+         i++;
+     }
+@@ -1541,6 +1616,17 @@ static JSONStatus_t multiSearch( const char * buf,
+     assert( ( max > 0U ) && ( queryLength > 0U ) );
+ 
+     while( i < queryLength )
++    assigns( i, start, queryStart, value, length )
++    loopInvariant(
++           0U <= start && start < max
++        && 0U < length && length <= max
++        && start + length <= max
++        && ( ( i == queryLength && ret == JSONSuccess && buf[ start ] == '"' ) ==> length >= 2U )
++        && 0U <= value && value < max
++        && 0U <= i && i <= queryLength
++        && 0U <= queryStart && queryStart <= queryLength
++    )
++    decreases( queryLength - i )
+     {
+         bool found = false;
+