diff --git a/CMakeLists.txt b/CMakeLists.txt index 18c3ca51d..e73b23d3c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -198,6 +198,10 @@ add_compile_options( $<$:-fdiagnostics-color=always> $<$:-fcolor-diagnostics> + ## Suppress warnings from kernel port files. + $<$:-Wno-sign-compare> + $<$:-Wno-sign-conversion> + $<$:-Wall> $<$:-Wextra> $<$:-Werror> diff --git a/source/FreeRTOS_DNS_Parser.c b/source/FreeRTOS_DNS_Parser.c index 67fd2d4f6..877bcb61a 100644 --- a/source/FreeRTOS_DNS_Parser.c +++ b/source/FreeRTOS_DNS_Parser.c @@ -613,7 +613,7 @@ } uxResult = DNS_SkipNameField( pxSet->pucByte, - sizeof( pxSet->pcName ) ); + pxSet->uxSourceBytesRemaining ); /* Check for a malformed response. */ if( uxResult == 0U ) diff --git a/test/cbmc/proofs/DNS_ParseDNSReply/Configurations.json b/test/cbmc/proofs/DNS_ParseDNSReply/Configurations.json new file mode 100644 index 000000000..d22815651 --- /dev/null +++ b/test/cbmc/proofs/DNS_ParseDNSReply/Configurations.json @@ -0,0 +1,50 @@ +{ + "ENTRY": "DNS_ParseDNSReply", + "TEST_PAYLOAD_SIZE": 5, + "TEST_IPV4_PACKET_SIZE": 59, + "TEST_IPV6_PACKET_SIZE": 79, + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset DNS_ParseDNSReply.0:{TEST_PAYLOAD_SIZE}", + "--unwindset DNS_ReadNameField.0:{TEST_PAYLOAD_SIZE}", + "--unwindset DNS_ReadNameField.1:{TEST_PAYLOAD_SIZE}", + "--unwindset parseDNSAnswer.0:{TEST_PAYLOAD_SIZE}", + "--unwindset strncpy.0:{TEST_PAYLOAD_SIZE}" + ], + "OPT": + [ + "--export-file-local-symbols" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto" + ], + "DEF": + [ + { + "IPv4": + [ + "TEST_PACKET_SIZE={TEST_IPV4_PACKET_SIZE}", + "ipconfigUSE_LLMNR=1", + "ipconfigUSE_MDNS=1", + "IS_TESTING_IPV6=0" + ] + }, + { + "IPv6": + [ + "TEST_PACKET_SIZE={TEST_IPV6_PACKET_SIZE}", + "ipconfigUSE_LLMNR=1", + "ipconfigUSE_MDNS=1", + "IS_TESTING_IPV6=1" + ] + } + ], + "INC": + [ + "$(FREERTOS_PLUS_TCP)/test/cbmc/include" + ] +} \ No newline at end of file diff --git a/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c b/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c new file mode 100644 index 000000000..9fae89ddc --- /dev/null +++ b/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c @@ -0,0 +1,211 @@ +/* Standard includes. */ +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "list.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_DNS_Parser.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" +#include "IPTraceMacroDefaults.h" + +#include "cbmc.h" +#include "../../utility/memory_assignments.c" + +/**************************************************************** +* Signature of function under test +****************************************************************/ + +uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer, + size_t uxBufferLength, + struct freertos_addrinfo ** ppxAddressInfo, + BaseType_t xExpected, + uint16_t usPort ); + +NetworkBufferDescriptor_t xNetworkBuffer; +int lIsIPv6Packet; + +size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer ) +{ + #if IS_TESTING_IPV6 + return ipSIZE_OF_IPv6_HEADER; + #else + return ipSIZE_OF_IPv4_HEADER; + #endif +} + +NetworkBufferDescriptor_t * pxUDPPayloadBuffer_to_NetworkBuffer( const void * pvBuffer ) +{ + __CPROVER_assert( pvBuffer != NULL, "Precondition: pvBuffer != NULL" ); + NetworkBufferDescriptor_t * pxRBuf; + + if( nondet_bool() ) + { + pxRBuf = NULL; + } + else + { + pxRBuf = &xNetworkBuffer; + } + + return pxRBuf; +} + +uint32_t ulChar2u32( const uint8_t * pucPtr ) +{ + __CPROVER_assert( __CPROVER_r_ok( pucPtr, 4 ), "must be 4 bytes legal address to read" ); +} + +uint16_t usChar2u16( const uint8_t * pucPtr ) +{ + __CPROVER_assert( __CPROVER_r_ok( pucPtr, 2 ), "must be 2 bytes legal address to read" ); +} + +const char * FreeRTOS_inet_ntop( BaseType_t xAddressFamily, + const void * pvSource, + char * pcDestination, + socklen_t uxSize ) +{ + __CPROVER_assert( __CPROVER_r_ok( pcDestination, uxSize ), "input buffer must be available" ); + + #if IS_TESTING_IPV6 + __CPROVER_assert( ( xAddressFamily == FREERTOS_AF_INET6 && __CPROVER_r_ok( pvSource, 16 ) ), "input address must be available" ); + #else + __CPROVER_assert( ( xAddressFamily == FREERTOS_AF_INET && __CPROVER_r_ok( pvSource, 4 ) ), "input address must be available" ); + #endif +} + +BaseType_t xApplicationDNSQueryHook_Multi( struct xNetworkEndPoint * pxEndPoint, + const char * pcName ) +{ + __CPROVER_assert( strlen( pcName ) < ipconfigDNS_CACHE_NAME_LENGTH, "The length of domain name must be less than cache size" ); +} + +void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer ) +{ + __CPROVER_assert( pxNetworkBuffer, "network descriptor must be valid." ); + __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer, "network buffer must be valid." ); + + free( pxNetworkBuffer->pucEthernetBuffer ); + free( pxNetworkBuffer ); +} + +/* The checksum generation is stubbed out since the actual checksum + * does not matter. The stub will return an indeterminate value each time. */ +uint16_t usGenerateChecksum( uint16_t usSum, + const uint8_t * pucNextData, + size_t uxByteCount ) +{ + uint16_t usReturn; + + __CPROVER_assert( __CPROVER_r_ok( pucNextData, uxByteCount ), "Data must be valid" ); + + /* Return an indeterminate value. */ + return usReturn; +} + +/* The checksum generation is stubbed out since the actual checksum + * does not matter. The stub will return an indeterminate value each time. */ +uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer, + size_t uxBufferLength, + BaseType_t xOutgoingPacket ) +{ + uint16_t usReturn; + + __CPROVER_assert( __CPROVER_r_ok( pucEthernetBuffer, uxBufferLength ), "Data must be valid" ); + + /* Return an indeterminate value. */ + return usReturn; +} + +/* pxDuplicateNetworkBufferWithDescriptor() is proved separately */ +NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const NetworkBufferDescriptor_t * const pxNetworkBuffer, + size_t xNewLength ) +{ + NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); + + if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) ) + { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xNewLength ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer ); + pxNetworkBuffer->xDataLength = xNewLength; + } + + return pxNetworkBuffer; +} + +/* vReturnEthernetFrame() is proved separately */ +void vReturnEthernetFrame( NetworkBufferDescriptor_t * pxNetworkBuffer, + BaseType_t xReleaseAfterSend ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, "xNetworkBuffer != NULL" ); + __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "pxNetworkBuffer->pucEthernetBuffer != NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data must be valid" ); +} + +uint32_t parseDNSAnswer( ParseSet_t * pxSet, + struct freertos_addrinfo ** ppxAddressInfo, + size_t * uxBytesRead ) +{ + uint32_t result; + + __CPROVER_assert( __CPROVER_r_ok( pxSet->pucByte, pxSet->uxSourceBytesRemaining ), "Data must be valid" ); + + return result; +} + +/**************************************************************** +* Proof of prvParseDNSReply +****************************************************************/ + +void harness() +{ + size_t uxBufferLength; + uint16_t usPort; + struct freertos_addrinfo * pxAddressInfo; + BaseType_t xExpected; + NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); + const uint32_t ulIpv4UdpOffset = 42, ulIpv6UdpOffset = 62; + uint8_t * pPayloadBuffer; + size_t uxPayloadBufferLength; + + __CPROVER_assert( TEST_PACKET_SIZE < CBMC_MAX_OBJECT_SIZE, + "TEST_PACKET_SIZE < CBMC_MAX_OBJECT_SIZE" ); + + __CPROVER_assume( uxBufferLength < CBMC_MAX_OBJECT_SIZE ); + __CPROVER_assume( uxBufferLength <= TEST_PACKET_SIZE ); + + lIsIPv6Packet = IS_TESTING_IPV6; + + xNetworkBuffer.pucEthernetBuffer = safeMalloc( uxBufferLength ); + xNetworkBuffer.xDataLength = uxBufferLength; + xNetworkBuffer.pxEndPoint = pxNetworkEndPoint_Temp; + + __CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL ); + + if( lIsIPv6Packet ) + { + __CPROVER_assume( uxBufferLength >= ulIpv6UdpOffset ); /* 62 is total size of IPv4 UDP header, including ethernet, IPv6, UDP headers. */ + pPayloadBuffer = xNetworkBuffer.pucEthernetBuffer + ulIpv6UdpOffset; + uxPayloadBufferLength = uxBufferLength - ulIpv6UdpOffset; + } + else + { + __CPROVER_assume( uxBufferLength >= ulIpv4UdpOffset ); /* 42 is total size of IPv4 UDP header, including ethernet, IPv4, UDP headers. */ + pPayloadBuffer = xNetworkBuffer.pucEthernetBuffer + ulIpv4UdpOffset; + uxPayloadBufferLength = uxBufferLength - ulIpv4UdpOffset; + } + + uint32_t index = DNS_ParseDNSReply( pPayloadBuffer, + uxPayloadBufferLength, + &pxAddressInfo, + xExpected, + usPort ); +} diff --git a/test/cbmc/proofs/ParseDNSReply/Makefile.json b/test/cbmc/proofs/ParseDNSReply/Makefile.json deleted file mode 100644 index aefd62da6..000000000 --- a/test/cbmc/proofs/ParseDNSReply/Makefile.json +++ /dev/null @@ -1,68 +0,0 @@ -# The proof depends on one parameter: -# NETWORK_BUFFER_SIZE is the size of the network buffer being parsed -# The buffer size must be bounded because we must bound the number of -# iterations loops iterating over the buffer. - -{ - "ENTRY": "ParseDNSReply", - -################################################################ -# This is the network buffer size. -# Reasonable values are size > 12 = sizeof(xDNSMessage) - "NETWORK_BUFFER_SIZE": 40, - -################################################################ -# This is the size of the buffer into which the name is copied. -# Set to any positive value. -# In the source, NAME_SIZE=254 and NETWORK_BUFFER_SIZE >> NAME_SIZE -# In the proof, NAME_SIZE >= 4 required for good coverage. - "NAME_SIZE": "10", - -################################################################ -# Loop prvParseDNSReply.0: -# file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 915 - "PARSELOOP0": "prvParseDNSReply.0", - -# M = sizeof( DNSMessage_t ) = 12 -# U = sizeof( uint32_t) = 4 -# Loop bound is (NETWORK_BUFFER_SIZE - M) div (U+1) + 1 tight for SIZE >= M -# Loop bound is 1 for 0 <= SIZE < M - "PARSELOOP0_UNWIND": - "__eval 1 if {NETWORK_BUFFER_SIZE} < 12 else ({NETWORK_BUFFER_SIZE} - 12) / 5 + 1", - -################################################################ -# Loop prvParseDNSReply.1: -# file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 989 - "PARSELOOP1": "prvParseDNSReply.1", - -# A = sizeof( DNSAnswerRecord_t ) = 10 -# M = sizeof( DNSMessage_t ) = 12 -# U = sizeof( uint32_t) = 4 -# Loop bound is (NETWORK_BUFFER_SIZE - M - A) div (A+1) + A + 1 tight -# for SIZE >= M + A -# Loop bound is (NETWORK_BUFFER_SIZE - M) + 1 for M <= SIZE < M + A -# Loop bound is 1 for 0 <= SIZE < M - "PARSELOOP1_UNWIND": - "__eval 1 if {NETWORK_BUFFER_SIZE} < 12 else ({NETWORK_BUFFER_SIZE} - 11 if {NETWORK_BUFFER_SIZE} < 22 else ({NETWORK_BUFFER_SIZE} - 12 - 10) / 11 + 11)", - -################################################################ - - "CBMCFLAGS": - [ - "--unwind 1", - "--unwindset {PARSELOOP0}:{PARSELOOP0_UNWIND},{PARSELOOP1}:{PARSELOOP1_UNWIND},prvProcessDNSCache.0:5" - ], - - "OBJS": - [ - "$(ENTRY)_harness.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto", - "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto" - ], - - "DEF": - [ - "NETWORK_BUFFER_SIZE={NETWORK_BUFFER_SIZE}", - "NAME_SIZE={NAME_SIZE}" - ] -} diff --git a/test/cbmc/proofs/ParseDNSReply/ParseDNSReply_harness.c b/test/cbmc/proofs/ParseDNSReply/ParseDNSReply_harness.c deleted file mode 100644 index 74e594fbd..000000000 --- a/test/cbmc/proofs/ParseDNSReply/ParseDNSReply_harness.c +++ /dev/null @@ -1,130 +0,0 @@ -/* Standard includes. */ -#include - -/* FreeRTOS includes. */ -#include "FreeRTOS.h" -#include "task.h" -#include "queue.h" -#include "list.h" -#include "semphr.h" - -/* FreeRTOS+TCP includes. */ -#include "FreeRTOS_IP.h" -#include "FreeRTOS_Sockets.h" -#include "FreeRTOS_IP_Private.h" -#include "FreeRTOS_UDP_IP.h" -#include "FreeRTOS_DNS.h" -#include "FreeRTOS_DNS_Parser.h" -#include "NetworkBufferManagement.h" -#include "NetworkInterface.h" -#include "IPTraceMacroDefaults.h" - -#include "cbmc.h" - -/**************************************************************** -* Signature of function under test -****************************************************************/ - -uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer, - size_t uxBufferLength, - BaseType_t xExpected ); - -/**************************************************************** -* Abstraction of DNS_ReadNameField proved in ReadNameField -****************************************************************/ - -size_t DNS_ReadNameField( const uint8_t * pucByte, - size_t uxRemainingBytes, - char * pcName, - size_t uxDestLen ) -{ - __CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, - "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE" ); - __CPROVER_assert( NAME_SIZE < CBMC_MAX_OBJECT_SIZE, - "NAME_SIZE < CBMC_MAX_OBJECT_SIZE" ); - __CPROVER_assert( NAME_SIZE >= 4, - "NAME_SIZE >= 4 required for good coverage." ); - - - /* Preconditions */ - __CPROVER_assert( uxRemainingBytes < CBMC_MAX_OBJECT_SIZE, - "ReadNameField: uxRemainingBytes < CBMC_MAX_OBJECT_SIZE)" ); - __CPROVER_assert( uxDestLen < CBMC_MAX_OBJECT_SIZE, - "ReadNameField: uxDestLen < CBMC_MAX_OBJECT_SIZE)" ); - - __CPROVER_assert( uxRemainingBytes <= NETWORK_BUFFER_SIZE, - "ReadNameField: uxRemainingBytes <= NETWORK_BUFFER_SIZE)" ); - - /* This precondition in the function contract for prvReadNameField - * fails because prvCheckOptions called prvReadNameField with the - * constant value 254. - * __CPROVER_assert(uxDestLen <= NAME_SIZE, - * "ReadNameField: uxDestLen <= NAME_SIZE)"); - */ - - __CPROVER_assert( pucByte != NULL, - "ReadNameField: pucByte != NULL )" ); - __CPROVER_assert( pcName != NULL, - "ReadNameField: pcName != NULL )" ); - - __CPROVER_assert( uxDestLen > 0, - "ReadNameField: uxDestLen > 0)" ); - - /* Return value */ - size_t index; - - /* Postconditions */ - __CPROVER_assume( index <= uxDestLen + 1 && index <= uxRemainingBytes ); - - return index; -} - -/**************************************************************** -* Abstraction of DNS_SkipNameField proved in SkipNameField -****************************************************************/ - -size_t DNS_SkipNameField( const uint8_t * pucByte, - size_t uxLength ) -{ - __CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, - "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE" ); - - - /* Preconditions */ - __CPROVER_assert( uxLength < CBMC_MAX_OBJECT_SIZE, - "SkipNameField: uxLength < CBMC_MAX_OBJECT_SIZE)" ); - __CPROVER_assert( uxLength <= NETWORK_BUFFER_SIZE, - "SkipNameField: uxLength <= NETWORK_BUFFER_SIZE)" ); - __CPROVER_assert( pucByte != NULL, - "SkipNameField: pucByte != NULL)" ); - - /* Return value */ - size_t index; - - /* Postconditions */ - __CPROVER_assume( index <= uxLength ); - - return index; -} - -/**************************************************************** -* Proof of prvParseDNSReply -****************************************************************/ - -void harness() -{ - size_t uxBufferLength; - BaseType_t xExpected; - uint8_t * pucUDPPayloadBuffer = malloc( uxBufferLength ); - - __CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, - "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE" ); - - __CPROVER_assume( uxBufferLength < CBMC_MAX_OBJECT_SIZE ); - __CPROVER_assume( uxBufferLength <= NETWORK_BUFFER_SIZE ); - __CPROVER_assume( pucUDPPayloadBuffer != NULL ); - - uint32_t index = prvParseDNSReply( pucUDPPayloadBuffer, - uxBufferLength, - xExpected ); -} diff --git a/test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c b/test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c index 0eab41c75..b4a6fd294 100644 --- a/test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c +++ b/test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c @@ -2784,12 +2784,10 @@ void test_parseDNSAnswer_recordNOTstored_gt_count_diffUsType( void ) pxDNSAnswerRecord->usDataLength = FreeRTOS_htons( ipSIZE_OF_IPv4_ADDRESS ); pxDNSAnswerRecord->usType = ( dnsTYPE_AAAA_HOST ); - usChar2u16_ExpectAnyArgsAndReturn( dnsTYPE_AAAA_HOST ); /* usType */ - ret = parseDNSAnswer( &xSet, &pxAddressInfo, &uxBytesRead ); TEST_ASSERT_EQUAL( 0, ret ); - TEST_ASSERT_EQUAL( 40, uxBytesRead ); + TEST_ASSERT_EQUAL( 0, uxBytesRead ); } /**