[SigV4] CBMC proof for Sigv4_awsIotdatetoISO8601 API (#19)

* Sigv4_AWSIOtDateToISO8601 CBMC PROOF

* Unit test coverage changes

source/sigv4.c

@@ -136,8 +136,9 @@ static void intToAscii( int32_t value,
 
     /* Write base-10 remainder in its ASCII representation, and fill any
      * remaining width with '0' characters. */
-    while( lenRemaining-- > 0U )
+    while( lenRemaining > 0U )
     {
+        lenRemaining--;
         ( *pBuffer )[ lenRemaining ] = ( char ) ( ( currentVal % 10 ) + '0' );
         currentVal /= 10;
     }
@@ -313,10 +314,8 @@ static SigV4Status_t scanValue( const char * pDate,
     }
 
     /* Determine if month value is non-numeric. */
-    if( ( formatChar == 'M' ) && ( *pLoc >= 'A' ) && ( *pLoc <= 'Z' ) )
+    if( ( formatChar == 'M' ) && ( remainingLenToRead == MONTH_ASCII_LEN ) )
     {
-        assert( remainingLenToRead == MONTH_ASCII_LEN );
-
         while( result++ < 12 )
         {
             /* Search month array for parsed string. */

test/cbmc/include/sigv4_stubs.h

@@ -0,0 +1,45 @@
+/*
+ * SigV4 Utility Library v1.0.0
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/**
+ * @file sigv4_stubs.h
+ * @brief Declarations for the (normally) static functions from sigv4.c.
+ * Please see sigv4.c for documentation.
+ */
+
+#ifndef SIGV4_STUBS_H_
+#define SIGV4_STUBS_H_
+
+#include <sigv4.h>
+#include <sigv4_internal.h>
+
+void addToDate( const char formatChar,
+                int32_t result,
+                SigV4DateTime_t * pDateElements );
+
+SigV4Status_t scanValue( const char * pDate,
+                         const char formatChar,
+                         size_t readLoc,
+                         size_t lenToRead,
+                         SigV4DateTime_t * pDateElements );
+
+#endif /* ifndef SIGV4_STUBS_H_ */

test/cbmc/proofs/Makefile-json.common

@@ -0,0 +1,22 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY=harness
+
+DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)
+ifdef CBMC_MAX_QUERYKEYLENGTH
+    DEFINES += -DCBMC_MAX_QUERYKEYLENGTH=$(CBMC_MAX_QUERYKEYLENGTH)
+endif
+
+INCLUDES += -I$(CBMC_ROOT)/include
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+
+PROJECT_SOURCES += $(PROOFDIR)/sigv4.c
+
+CHECKFLAGS += --pointer-primitive-check
+
+include ../Makefile.common
+
+cleanclean: veryclean
+	-$(RM) $(PROOFDIR)/sigv4.c

test/cbmc/proofs/Makefile-project-targets

@@ -8,3 +8,18 @@
 # Use this file to give project-specific targets, including targets
 # that may depend on targets defined in Makefile.common.
 ################################################################
+
+# Each proof requires sigv4.c to be patched (using sed) and dumped into the
+# proof directory. The exact sed invocation differs for each proof. So each
+# proof must set the SIGV4_SED_EXPR variable, which this rule uses as the
+# argument to sed.
+$(PROOFDIR)/sigv4.c: $(SRCDIR)/source/sigv4.c
+	$(LITANI) add-job \
+	  --command \
+	    "sed -E '$(SIGV4_SED_EXPR)' $^" \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $@ \
+	  --ci-stage build \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --description "$(PROOF_UID): patching sigv4.c"

test/cbmc/proofs/SigV4_AwsIotDateToIso8601/Makefile

@@ -12,18 +12,20 @@ DEFINES +=
 INCLUDES +=
 
 MONTH_ASCII_LEN=3
-ISO_YEAR_LEN=4
+ISO_YEAR_LEN=5
 MONTHS_IN_YEAR=12
 FORMAT_RFC_5322_LEN=32
 
 REMOVE_FUNCTION_BODY +=
-UNWINDSET += __CPROVER_file_local_sigv4_c_parseDate.0:$(FORMAT_RFC_5322_LEN)
-UNWINDSET += __CPROVER_file_local_sigv4_c_scanValue.0:$(MONTHS_IN_YEAR)
-UNWINDSET += __CPROVER_file_local_sigv4_c_scanValue.1:$(ISO_YEAR_LEN)
-UNWINDSET += __CPROVER_file_local_sigv4_c_intToAscii.0:$(ISO_YEAR_LEN)
-UNWINDSET += strncmp.0:$(MONTH_ASCII_LEN)
+UNWINDSET += parseDate.0:$(FORMAT_RFC_5322_LEN)
+UNWINDSET += scanValue.0:$(ISO_YEAR_LEN)
+UNWINDSET += intToAscii.0:$(ISO_YEAR_LEN)
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/source/sigv4.c
+PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/sigv4_stubs.c
 
-include ../Makefile.common
+include ../Makefile-json.common
+
+# Substitution command to pass to sed for patching sigv4.c. The
+# characters " and # must be escaped with backslash.
+SIGV4_SED_EXPR = 1s/^/\#include \"sigv4_stubs.h\" /; s/^static //; s/SigV4Status_t scanValue\b/&_/

test/cbmc/proofs/SigV4_AwsIotDateToIso8601/SigV4_AwsIotDateToIso8601_harness.c

@@ -25,7 +25,7 @@
  * @brief Implements the proof harness for SigV4_AwsIotDateToIso8601 function.
  */
 
-/* Include paths for public enums, structures, and macros. */
+#include "stdlib.h"
 #include "sigv4.h"
 
 void harness()
@@ -34,12 +34,17 @@ void harness()
     size_t dateLen;
     char * pDateISO8601;
     size_t dateISO8601Len;
+    SigV4Status_t status;
 
     __CPROVER_assume( dateLen == SIGV4_EXPECTED_LEN_RFC_3339 || dateLen == SIGV4_EXPECTED_LEN_RFC_5322 || dateLen == 0 );
+
     pInputDate = malloc( dateLen );
 
     __CPROVER_assume( dateISO8601Len < CBMC_MAX_OBJECT_SIZE );
+
     pDateISO8601 = malloc( dateISO8601Len );
 
-    SigV4_AwsIotDateToIso8601( pInputDate, dateLen, pDateISO8601, dateISO8601Len );
+    status = SigV4_AwsIotDateToIso8601( pInputDate, dateLen, pDateISO8601, dateISO8601Len );
+
+    __CPROVER_assert( status == SigV4InvalidParameter || status == SigV4Success || status == SigV4ISOFormattingError, "This is not a valid SigV4 return status" );
 }

test/cbmc/stubs/sigv4_stubs.c

@@ -0,0 +1,129 @@
+/*
+ * SigV4 Utility Library v1.0.0
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/**
+ * @file sigv4_stubs.c
+ * @brief Implements the functions declared in sigv4_stubs.h
+ */
+
+#include <sigv4.h>
+#include <sigv4_internal.h>
+#include <sigv4_stubs.h>
+
+SigV4Status_t scanValue( const char * pDate,
+                         const char formatChar,
+                         size_t readLoc,
+                         size_t lenToRead,
+                         SigV4DateTime_t * pDateElements )
+{
+    SigV4Status_t returnStatus = SigV4InvalidParameter;
+    const char * pMonthNames[] = MONTH_NAMES;
+    const char * pLoc = pDate + readLoc;
+    size_t remainingLenToRead = lenToRead;
+    int32_t result = 0;
+    static flag = 0;
+
+    assert( pDate != NULL );
+    assert( pDateElements != NULL );
+
+    if( formatChar == '*' )
+    {
+        remainingLenToRead = 0U;
+    }
+
+    /* Determine if month value is non-numeric. */
+    if( ( formatChar == 'M' ) && ( remainingLenToRead == MONTH_ASCII_LEN ) )
+    {
+        returnStatus = SigV4Success;
+
+        remainingLenToRead = 0U;
+    }
+
+    /* Interpret integer value of numeric representation. */
+    while( ( remainingLenToRead > 0U ) && ( *pLoc >= '0' ) && ( *pLoc <= '9' ) )
+    {
+        result = ( result * 10 ) + ( int32_t ) ( *pLoc - '0' );
+        remainingLenToRead--;
+        pLoc += 1;
+    }
+
+    if( remainingLenToRead != 0U )
+    {
+        LogError( ( "Parsing Error: Expected numerical string of type '%%%d%c', "
+                    "but received '%.*s'.",
+                    ( int ) lenToRead,
+                    formatChar,
+                    ( int ) lenToRead,
+                    pLoc ) );
+        returnStatus = SigV4ISOFormattingError;
+    }
+
+    if( returnStatus != SigV4ISOFormattingError )
+    {
+        addToDate( formatChar,
+                   result,
+                   pDateElements );
+    }
+
+    return returnStatus;
+}
+
+void addToDate( const char formatChar,
+                int32_t result,
+                SigV4DateTime_t * pDateElements )
+{
+    assert( pDateElements != NULL );
+    assert( result >= 0 );
+
+    switch( formatChar )
+    {
+        case 'Y':
+            pDateElements->tm_year = result;
+            break;
+
+        case 'M':
+            pDateElements->tm_mon = result;
+            break;
+
+        case 'D':
+            pDateElements->tm_mday = result;
+            break;
+
+        case 'h':
+            pDateElements->tm_hour = result;
+            break;
+
+        case 'm':
+            pDateElements->tm_min = result;
+            break;
+
+        case 's':
+            pDateElements->tm_sec = result;
+            break;
+
+        default:
+
+            /* Do not assign values for skipped characters ('*'), or
+             * unrecognized format specifiers. */
+            break;
+    }
+}

test/unit-test/sigv4_utest.c

@@ -29,7 +29,7 @@
 
 /* The number of invalid date inputs tested in
  * test_SigV4_AwsIotDateToIso8601_Formatting_Error() */
-#define SIGV4_TEST_INVALID_DATE_COUNT    22U
+#define SIGV4_TEST_INVALID_DATE_COUNT    24U
 
 /* File-scoped global variables */
 static char pTestBufferValid[ SIGV4_ISO_STRING_LEN ] = { 0 };
@@ -50,6 +50,7 @@ void formatAndVerifyInputDate( const char * pInputDate,
                                                          strlen( pInputDate ),
                                                          pTestBufferValid,
                                                          SIGV4_ISO_STRING_LEN );
+
     TEST_ASSERT_EQUAL( expectedStatus, returnVal );
 
     if( returnVal == SigV4Success )
@@ -201,7 +202,8 @@ void test_SigV4_AwsIotDateToIso8601_Formatting_Error()
         "1800-02-28T03:61:09Z", "Wed, 18 Jan 2018 09:99:06 GMT", /* minute > 59 */
         "1800-01-29T03:21:70Z", "Wed, 18 Jan 2018 09:18:75 GMT", /* seconds > 60 */
         "2018-01-18X09:18:06Z", "Wed. 31 Apr 2018T09:18:06 GMT", /* Unexpected character 'X'. */
-        "2018-01-1!X09:18:06Z", "Wed. 31 Apr 2018T0A:18:06 GMT"  /* Unexpected non-digit found in date element. */
+        "2018-01-1@X09:18:06Z", "Wed. 31 Apr 2018T0A:18:06 GMT", /* Unexpected non-digit found in date element. */
+        "2018-01-1!X09:18:06Z", "Wed. 31 Apr 2018T!9:18:06 GMT"  /* Unexpected non-digit found in date element. */
     };
 
     for( index = 0U; index < SIGV4_TEST_INVALID_DATE_COUNT - 1; index += 2 )