diff --git a/source/sigv4.c b/source/sigv4.c index 8f108c2d..48bd7aa1 100644 --- a/source/sigv4.c +++ b/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. */ diff --git a/test/cbmc/include/sigv4_stubs.h b/test/cbmc/include/sigv4_stubs.h new file mode 100644 index 00000000..cde2d84f --- /dev/null +++ b/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 +#include + +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_ */ diff --git a/test/cbmc/proofs/Makefile-json.common b/test/cbmc/proofs/Makefile-json.common new file mode 100644 index 00000000..8c2b4b0b --- /dev/null +++ b/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 diff --git a/test/cbmc/proofs/Makefile-project-targets b/test/cbmc/proofs/Makefile-project-targets index 2d4d4602..e5857246 100644 --- a/test/cbmc/proofs/Makefile-project-targets +++ b/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" diff --git a/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/Makefile b/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/Makefile index cd3580f2..a7977100 100644 --- a/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/Makefile +++ b/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/&_/ diff --git a/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/SigV4_AwsIotDateToIso8601_harness.c b/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/SigV4_AwsIotDateToIso8601_harness.c index d404aee8..ac7ab20f 100644 --- a/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/SigV4_AwsIotDateToIso8601_harness.c +++ 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" ); } diff --git a/test/cbmc/stubs/sigv4_stubs.c b/test/cbmc/stubs/sigv4_stubs.c new file mode 100644 index 00000000..8052771f --- /dev/null +++ b/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 +#include +#include + +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; + } +} diff --git a/test/unit-test/sigv4_utest.c b/test/unit-test/sigv4_utest.c index 0c5e3023..a200aeb6 100644 --- a/test/unit-test/sigv4_utest.c +++ b/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 )