From 0d57715b503ece8a8f50caa1593fba9bf0170572 Mon Sep 17 00:00:00 2001 From: Paschal Amusuo Date: Tue, 15 Apr 2025 12:12:45 -0400 Subject: [PATCH 1/2] Fixes for FreeRTOS proof errors. --- .../DNS_ParseDNSReply_harness.c | 16 +++++++++++++--- .../ProcessReceivedTCPPacket_harness.c | 7 +++++-- 2 files changed, 18 insertions(+), 5 deletions(-) diff --git a/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c b/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c index 9fae89ddc8..fc6862c265 100644 --- a/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c +++ b/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c @@ -119,6 +119,7 @@ uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer, { uint16_t usReturn; + // BUG: This assertion is violated by this proof. This may be a real bug in the calling function or just an overly constrained assertion. __CPROVER_assert( __CPROVER_r_ok( pucEthernetBuffer, uxBufferLength ), "Data must be valid" ); /* Return an indeterminate value. */ @@ -131,11 +132,17 @@ NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const Networ { NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); - if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) ) + // BUG: Changed this condition because the previous version reported an assertion + if( pxNetworkBuffer != NULL ) { pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xNewLength ); - __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); pxNetworkBuffer->xDataLength = xNewLength; + + // Added this to resolve a null pointer violation in a location where pxEndPoint was used. + // This may be a real NULL pointer dereferencing bug if pxEndpoint can be NULL. + pxNetworkBuffer->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL ); } return pxNetworkBuffer; @@ -147,6 +154,7 @@ void vReturnEthernetFrame( NetworkBufferDescriptor_t * pxNetworkBuffer, { __CPROVER_assert( pxNetworkBuffer != NULL, "xNetworkBuffer != NULL" ); __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "pxNetworkBuffer->pucEthernetBuffer != NULL" ); + // BUG: This assertion is violated by this proof. This may be a real bug in the calling function or just an overly constrained assertion. __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data must be valid" ); } @@ -180,7 +188,9 @@ void harness() "TEST_PACKET_SIZE < CBMC_MAX_OBJECT_SIZE" ); __CPROVER_assume( uxBufferLength < CBMC_MAX_OBJECT_SIZE ); - __CPROVER_assume( uxBufferLength <= TEST_PACKET_SIZE ); + // BUG: Removing this assumption because TEST_PACKET_SIZE is only 29 bytes. + // With this assumption, the target function is never verified. + // __CPROVER_assume( uxBufferLength <= TEST_PACKET_SIZE ); lIsIPv6Packet = IS_TESTING_IPV6; diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c index c15387b900..161c4cc240 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c @@ -47,6 +47,8 @@ void prvTCPReturnPacket( FreeRTOS_Socket_t * pxSocket, uint32_t ulLen, BaseType_t xReleaseAfterSend ) { + // BUG: xProcessReceivedTCPPacket calls this prvTCPReturnPacket function with pxSocket being NULL. + // This causes this assertion to be violated. __CPROVER_assert( pxSocket != NULL, "pxSocket should not be NULL" ); __CPROVER_assert( pxDescriptor != NULL, "pxDescriptor should not be NULL" ); __CPROVER_assert( pxDescriptor->pucEthernetBuffer != NULL, "pucEthernetBuffer should not be NULL" ); @@ -151,7 +153,7 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS if( pxNetworkBuffer ) { pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes ); - __CPROVER_assume( pxNetworkBuffer->xDataLength == ipSIZE_OF_ETH_HEADER + sizeof( int32_t ) ); + pxNetworkBuffer->xDataLength = xRequestedSizeBytes; } return pxNetworkBuffer; @@ -174,8 +176,9 @@ size_t uxIPHeaderSizeSocket( const FreeRTOS_Socket_t * pxSocket ) void harness() { NetworkBufferDescriptor_t * pxNetworkBuffer; + size_t tcpPacketSize; - pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( sizeof( TCPPacket_t ), 0 ); + pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( tcpPacketSize, 0 ); /* To avoid asserting on the network buffer being NULL. */ __CPROVER_assume( pxNetworkBuffer != NULL ); From 902d3a4fa5bff29bd5d0104b59d7ccef1bf7525d Mon Sep 17 00:00:00 2001 From: Paschal Amusuo Date: Tue, 15 Apr 2025 12:16:57 -0400 Subject: [PATCH 2/2] Added more comments --- .../ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c index 161c4cc240..444b6e646d 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c @@ -153,6 +153,7 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS if( pxNetworkBuffer ) { pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes ); + // BUG: The previous version fixed the xDataLength value, preventing code coverage. pxNetworkBuffer->xDataLength = xRequestedSizeBytes; } @@ -176,6 +177,7 @@ size_t uxIPHeaderSizeSocket( const FreeRTOS_Socket_t * pxSocket ) void harness() { NetworkBufferDescriptor_t * pxNetworkBuffer; + // BUG: We need to make the size of input packet nondeterministic. size_t tcpPacketSize; pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( tcpPacketSize, 0 );