From 39c2e171eb48e907473d9f0057ca6e17b2573399 Mon Sep 17 00:00:00 2001 From: Paschal Amusuo Date: Wed, 16 Oct 2024 18:49:48 -0400 Subject: [PATCH] Changes to recreate and expose CVEs --- source/FreeRTOS_ICMP.c | 6 ++- source/FreeRTOS_TCP_IP.c | 2 + source/FreeRTOS_TCP_Reception.c | 37 +++++++++------- .../ARPProcessPacket_harness.c | 10 +++-- .../CheckOptions/CheckOptions_harness.c | 13 ++---- .../proofs/CheckOptionsOuter/Makefile.json | 3 +- .../ProcessICMPPacket_harness.c | 12 +++++- test/cbmc/proofs/ParseDNSReply/Makefile.json | 2 +- .../ParseDNSReply/ParseDNSReply_harness.c | 43 +++++++++++++------ .../ProcessReceivedTCPPacket_harness.c | 8 +++- 10 files changed, 86 insertions(+), 50 deletions(-) diff --git a/source/FreeRTOS_ICMP.c b/source/FreeRTOS_ICMP.c index 75e51bb79b..d518731a05 100644 --- a/source/FreeRTOS_ICMP.c +++ b/source/FreeRTOS_ICMP.c @@ -86,9 +86,11 @@ iptraceICMP_PACKET_RECEIVED(); - configASSERT( pxNetworkBuffer->xDataLength >= sizeof( ICMPPacket_t ) ); + // ICSE-NIER: Commented out the following two checks to expose CVE-2018-16527 + // configASSERT( pxNetworkBuffer->xDataLength >= sizeof( ICMPPacket_t ) ); - if( pxNetworkBuffer->xDataLength >= sizeof( ICMPPacket_t ) ) + // if( pxNetworkBuffer->xDataLength >= sizeof( ICMPPacket_t ) ) + // if (pdTRUE) { /* Map the buffer onto a ICMP-Packet struct to easily access the * fields of ICMP packet. */ diff --git a/source/FreeRTOS_TCP_IP.c b/source/FreeRTOS_TCP_IP.c index cfba8d04fb..c36619129a 100644 --- a/source/FreeRTOS_TCP_IP.c +++ b/source/FreeRTOS_TCP_IP.c @@ -703,7 +703,9 @@ uxIPHeaderOffset = ipSIZE_OF_ETH_HEADER + uxIPHeaderSizePacket( pxNetworkBuffer ); /* Check for a minimum packet size. */ + // ICSE-NIER: Commented out the validation to expose CVE-2018-16603 if( pxNetworkBuffer->xDataLength < ( uxIPHeaderOffset + ipSIZE_OF_TCP_HEADER ) ) + // if (pdFALSE) { xResult = pdFAIL; } diff --git a/source/FreeRTOS_TCP_Reception.c b/source/FreeRTOS_TCP_Reception.c index 4dcd396b6a..24b07d2f4e 100644 --- a/source/FreeRTOS_TCP_Reception.c +++ b/source/FreeRTOS_TCP_Reception.c @@ -131,7 +131,10 @@ if( pxNetworkBuffer->xDataLength > uxOptionOffset ) { /* Validate options size calculation. */ - if( uxOptionsLength <= ( pxNetworkBuffer->xDataLength - uxOptionOffset ) ) + + // ICSE-NIER - Commented out to reproduce CVE-2018-16524 + // if( uxOptionsLength <= ( pxNetworkBuffer->xDataLength - uxOptionOffset ) ) + if (pdTRUE) { if( ( pxTCPHeader->ucTCPFlags & tcpTCP_FLAG_SYN ) != ( uint8_t ) 0U ) { @@ -262,17 +265,19 @@ if( pxSocket->u.xTCP.usMSS != uxNewMSS ) { /* Perform a basic check on the the new MSS. */ - if( uxNewMSS == 0U ) - { - lIndex = -1; - /* Return Condition found. */ - xReturn = pdTRUE; - } - else - { - FreeRTOS_debug_printf( ( "MSS change %u -> %u\n", pxSocket->u.xTCP.usMSS, ( unsigned ) uxNewMSS ) ); - } + // ICSE-NIER - Commented out to reproduce CVE-2018-16523 + // if( uxNewMSS == 0U ) + // { + // lIndex = -1; + + // /* Return Condition found. */ + // xReturn = pdTRUE; + // } + // else + // { + // FreeRTOS_debug_printf( ( "MSS change %u -> %u\n", pxSocket->u.xTCP.usMSS, ( unsigned ) uxNewMSS ) ); + // } } /* If a 'return' condition has not been found. */ @@ -280,10 +285,12 @@ { /* Restrict the minimum value of segment length to the ( Minimum IP MTU (576) - IP header(20) - TCP Header(20) ). * See "RFC 791 section 3.1 Total Length" for more details. */ - if( uxNewMSS < tcpMINIMUM_SEGMENT_LENGTH ) - { - uxNewMSS = tcpMINIMUM_SEGMENT_LENGTH; - } + + // ICSE-NIER - Commented out to reproduce CVE-2018-16523 + // if( uxNewMSS < tcpMINIMUM_SEGMENT_LENGTH ) + // { + // uxNewMSS = tcpMINIMUM_SEGMENT_LENGTH; + // } if( pxSocket->u.xTCP.usMSS > uxNewMSS ) { diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c index 539f02d180..31cd8fd0ae 100644 --- a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c +++ b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c @@ -70,16 +70,18 @@ void harness() * is at least allocated to sizeof(ARPPacket_t) size but eventually an even larger buffer. * This is not checked inside eARPProcessPacket. */ - uint8_t ucBUFFER_SIZE; - - void * xBuffer = malloc( ucBUFFER_SIZE + sizeof( ARPPacket_t ) ); + uint8_t ucBUFFER_SIZE; + // ICSE-NIER: Updated the buffer size so it can contain truncated ARP header, reproducing CVE-2018-16600 + // void * xBuffer = malloc( ucBUFFER_SIZE + sizeof( ARPPacket_t ) ); + void * xBuffer = malloc( ucBUFFER_SIZE + sizeof( EthernetHeader_t ) ); + __CPROVER_assume( xBuffer != NULL ); NetworkBufferDescriptor_t xNetworkBuffer2; xNetworkBuffer2.pucEthernetBuffer = xBuffer; - xNetworkBuffer2.xDataLength = ucBUFFER_SIZE + sizeof( ARPPacket_t ); + xNetworkBuffer2.xDataLength = ucBUFFER_SIZE + sizeof( EthernetHeader_t ); /* * This proof assumes one end point is present. diff --git a/test/cbmc/proofs/CheckOptions/CheckOptions_harness.c b/test/cbmc/proofs/CheckOptions/CheckOptions_harness.c index 134d73c550..c09bea3c72 100644 --- a/test/cbmc/proofs/CheckOptions/CheckOptions_harness.c +++ b/test/cbmc/proofs/CheckOptions/CheckOptions_harness.c @@ -51,6 +51,9 @@ int32_t __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOpti FreeRTOS_Socket_t * const pxSocket, BaseType_t xHasSYNFlag ) { + // ICSE-NIER: Added this constraint to expose CVE-2018-16524 + __CPROVER_assert(__CPROVER_rw_ok(pucPtr, uxTotalLength), "p is readable and writable"); + /* CBMC model of pointers limits the size of the buffer */ /* Preconditions */ @@ -73,16 +76,6 @@ int32_t __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOpti return index; } -size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer ) -{ - __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer should not be NULL" ); - return uxIPHeaderSizePacket_uxResult; -} - -/**************************************************************** -* Proof of CheckOptions -****************************************************************/ - void harness() { /* Give buffer_size an unconstrained value */ diff --git a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json b/test/cbmc/proofs/CheckOptionsOuter/Makefile.json index d97be23e62..7dc183be26 100644 --- a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json +++ b/test/cbmc/proofs/CheckOptionsOuter/Makefile.json @@ -2,7 +2,8 @@ "ENTRY": "CheckOptionsOuter", "CBMCFLAGS": [ - "--unwind 1", + "--div-by-zero-check", + "--unwind 1", "--unwindset __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOptions.0:32" ], "OPT": diff --git a/test/cbmc/proofs/ICMP/ProcessICMPPacket/ProcessICMPPacket_harness.c b/test/cbmc/proofs/ICMP/ProcessICMPPacket/ProcessICMPPacket_harness.c index 185cbee92d..288ac5e213 100644 --- a/test/cbmc/proofs/ICMP/ProcessICMPPacket/ProcessICMPPacket_harness.c +++ b/test/cbmc/proofs/ICMP/ProcessICMPPacket/ProcessICMPPacket_harness.c @@ -58,13 +58,21 @@ void harness() { NetworkBufferDescriptor_t xNetworkBuffer; + // ICSE-NIER: Updated this harness to expose CVE-2018-16527 + uint8_t data_size; + + __CPROVER_assume( data_size < 1000 ); + /* Allocate a ICMP packet */ - ICMPPacket_t * const pxICMPPacket = safeMalloc( sizeof( ICMPPacket_t ) ); + // ICMPPacket_t * const pxICMPPacket = safeMalloc( sizeof( ICMPPacket_t ) ); + ICMPPacket_t * const pxICMPPacket = safeMalloc( data_size ); __CPROVER_assume( pxICMPPacket != NULL ); - xNetworkBuffer.xDataLength = sizeof( ICMPPacket_t ); + // xNetworkBuffer.xDataLength = sizeof( ICMPPacket_t ); + xNetworkBuffer.xDataLength = data_size; xNetworkBuffer.pucEthernetBuffer = pxICMPPacket; ProcessICMPPacket( &xNetworkBuffer ); } + diff --git a/test/cbmc/proofs/ParseDNSReply/Makefile.json b/test/cbmc/proofs/ParseDNSReply/Makefile.json index aefd62da62..e55c337dae 100644 --- a/test/cbmc/proofs/ParseDNSReply/Makefile.json +++ b/test/cbmc/proofs/ParseDNSReply/Makefile.json @@ -56,7 +56,7 @@ "OBJS": [ "$(ENTRY)_harness.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto", "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto" ], diff --git a/test/cbmc/proofs/ParseDNSReply/ParseDNSReply_harness.c b/test/cbmc/proofs/ParseDNSReply/ParseDNSReply_harness.c index 74e594fbd2..1fa20c1b32 100644 --- a/test/cbmc/proofs/ParseDNSReply/ParseDNSReply_harness.c +++ b/test/cbmc/proofs/ParseDNSReply/ParseDNSReply_harness.c @@ -25,18 +25,28 @@ * Signature of function under test ****************************************************************/ -uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer, - size_t uxBufferLength, - BaseType_t xExpected ); +// ICSE-NIER: Updated the function signature to expose CVE-2018-16525 +// uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer, +// size_t uxBufferLength, +// BaseType_t xExpected ); + +uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer, + size_t uxBufferLength, + struct freertos_addrinfo ** ppxAddressInfo, + BaseType_t xExpected, + uint16_t usPort ); /**************************************************************** * Abstraction of DNS_ReadNameField proved in ReadNameField ****************************************************************/ -size_t DNS_ReadNameField( const uint8_t * pucByte, - size_t uxRemainingBytes, - char * pcName, - size_t uxDestLen ) +// ICSE-NIER: Updated the function signature to expose CVE-2018-16525 +size_t DNS_ReadNameField( ParseSet_t * pxSet, + size_t uxDestLen ) +// 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" ); @@ -47,12 +57,12 @@ size_t DNS_ReadNameField( const uint8_t * pucByte, /* Preconditions */ - __CPROVER_assert( uxRemainingBytes < CBMC_MAX_OBJECT_SIZE, + __CPROVER_assert( pxSet->uxSourceBytesRemaining < 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, + __CPROVER_assert( pxSet->uxSourceBytesRemaining <= NETWORK_BUFFER_SIZE, "ReadNameField: uxRemainingBytes <= NETWORK_BUFFER_SIZE)" ); /* This precondition in the function contract for prvReadNameField @@ -62,9 +72,9 @@ size_t DNS_ReadNameField( const uint8_t * pucByte, * "ReadNameField: uxDestLen <= NAME_SIZE)"); */ - __CPROVER_assert( pucByte != NULL, + __CPROVER_assert( pxSet->pucByte != NULL, "ReadNameField: pucByte != NULL )" ); - __CPROVER_assert( pcName != NULL, + __CPROVER_assert( pxSet->pcName != NULL, "ReadNameField: pcName != NULL )" ); __CPROVER_assert( uxDestLen > 0, @@ -74,7 +84,7 @@ size_t DNS_ReadNameField( const uint8_t * pucByte, size_t index; /* Postconditions */ - __CPROVER_assume( index <= uxDestLen + 1 && index <= uxRemainingBytes ); + __CPROVER_assume( index <= uxDestLen + 1 && index <= pxSet->uxSourceBytesRemaining ); return index; } @@ -115,6 +125,8 @@ void harness() { size_t uxBufferLength; BaseType_t xExpected; + uint16_t usPort; + struct freertos_addrinfo * pxAddressInfo; uint8_t * pucUDPPayloadBuffer = malloc( uxBufferLength ); __CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, @@ -124,7 +136,10 @@ void harness() __CPROVER_assume( uxBufferLength <= NETWORK_BUFFER_SIZE ); __CPROVER_assume( pucUDPPayloadBuffer != NULL ); - uint32_t index = prvParseDNSReply( pucUDPPayloadBuffer, + // ICSE-NIER: Updated the function invocation to expose CVE-2018-16525 + uint32_t index = DNS_ParseDNSReply( pucUDPPayloadBuffer, uxBufferLength, - xExpected ); + &pxAddressInfo, + xExpected, + usPort ); } diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c index 00f6e8014c..949d12a21d 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c @@ -103,7 +103,13 @@ void harness() /* To avoid asserting on the network buffer being NULL. */ __CPROVER_assume( pxNetworkBuffer != NULL ); - pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) ); + // ICSE-NIER: Made the buffer size non-deterministic to recreate CVE-2018-16603 + // pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) ); + + uint8_t data_size; + __CPROVER_assume(data_size > 54); + pxNetworkBuffer->pucEthernetBuffer = safeMalloc( data_size ); + pxNetworkBuffer->xDataLength = data_size; /* To avoid asserting on the ethernet buffer being NULL. */ __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );