Skip to content

Commit

Permalink
Fix DNS parse reply proof
Browse files Browse the repository at this point in the history
  • Loading branch information
@tony-josi-aws
tony-josi-aws committed Jun 12, 2024
1 parent cc12b07 commit cd051a4
Show file tree
Hide file tree
Showing 2 changed files with 190 additions and 128 deletions.
224 changes: 152 additions & 72 deletions test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,101 +10,155 @@

/* 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"
#include "../../../utility/memory_assignments.c"

/****************************************************************
* Signature of function under test
****************************************************************/

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
****************************************************************/
NetworkBufferDescriptor_t xNetworkBuffer;
int lIsIPv6Packet;

size_t DNS_ReadNameField( const uint8_t * pucByte,
size_t uxRemainingBytes,
char * pcName,
size_t uxDestLen )
size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer )
{
__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." );
#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;
}

/* 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)" );
uint32_t ulChar2u32( const uint8_t * pucPtr )
{
__CPROVER_assert( __CPROVER_r_ok( pucPtr, 4 ), "must be 4 bytes legal address to read" );
}

__CPROVER_assert( uxRemainingBytes <= NETWORK_BUFFER_SIZE,
"ReadNameField: uxRemainingBytes <= NETWORK_BUFFER_SIZE)" );
uint16_t usChar2u16( const uint8_t * pucPtr )
{
__CPROVER_assert( __CPROVER_r_ok( pucPtr, 2 ), "must be 2 bytes legal address to read" );
}

/* 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)");
*/
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" );

__CPROVER_assert( pucByte != NULL,
"ReadNameField: pucByte != NULL )" );
__CPROVER_assert( pcName != NULL,
"ReadNameField: pcName != NULL )" );
#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
}

__CPROVER_assert( uxDestLen > 0,
"ReadNameField: uxDestLen > 0)" );
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" );
}

/* Return value */
size_t index;
void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
{
__CPROVER_assert( pxNetworkBuffer, "network descriptor must be valid." );
__CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer, "network buffer must be valid." );

/* Postconditions */
__CPROVER_assume( index <= uxDestLen + 1 && index <= uxRemainingBytes );
free( pxNetworkBuffer->pucEthernetBuffer );
free( pxNetworkBuffer );
}

return index;
/* 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;
}

/****************************************************************
* Abstraction of DNS_SkipNameField proved in SkipNameField
****************************************************************/
/* 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;
}

size_t DNS_SkipNameField( const uint8_t * pucByte,
size_t uxLength )
/* pxDuplicateNetworkBufferWithDescriptor() is proved separately */
NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const NetworkBufferDescriptor_t * const pxNetworkBuffer,
size_t xNewLength )
{
__CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE,
"NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE" );
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;
}

/* 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 pxNetworkBuffer;
}

/* Return value */
size_t index;
/* 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" );
}

/* Postconditions */
__CPROVER_assume( index <= uxLength );
uint32_t parseDNSAnswer( ParseSet_t * pxSet,
struct freertos_addrinfo ** ppxAddressInfo,
size_t * uxBytesRead )
{
uint32_t result;

return index;
__CPROVER_assert( __CPROVER_r_ok( pxSet->pucByte, pxSet->uxSourceBytesRemaining ), "Data must be valid" );

return result;
}

/****************************************************************
Expand All @@ -114,17 +168,43 @@ size_t DNS_SkipNameField( const uint8_t * pucByte,
void harness()
{
size_t uxBufferLength;
uint16_t usPort;
struct freertos_addrinfo *pxAddressInfo;
BaseType_t xExpected;
uint8_t * pucUDPPayloadBuffer = malloc( uxBufferLength );
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( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE,
"NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE" );
__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 <= NETWORK_BUFFER_SIZE );
__CPROVER_assume( pucUDPPayloadBuffer != NULL );

uint32_t index = prvParseDNSReply( pucUDPPayloadBuffer,
uxBufferLength,
xExpected );
}
__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 );
}
94 changes: 38 additions & 56 deletions test/cbmc/proofs/DNS_ParseDNSReply/Makefile.json
View file
Original file line number Diff line number Diff line change
@@ -1,68 +1,50 @@
# 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)",

################################################################

"ENTRY": "DNS_ParseDNSReply",
"TEST_PAYLOAD_SIZE": 5,
"TEST_IPV4_PACKET_SIZE": 59,
"TEST_IPV6_PACKET_SIZE": 79,
"CBMCFLAGS":
[
"--unwind 1",
"--unwindset {PARSELOOP0}:{PARSELOOP0_UNWIND},{PARSELOOP1}:{PARSELOOP1_UNWIND},prvProcessDNSCache.0:5"
"--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.goto",
"$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto"
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto",
"$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto"
],

"DEF":
[
"NETWORK_BUFFER_SIZE={NETWORK_BUFFER_SIZE}",
"NAME_SIZE={NAME_SIZE}"
{
"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"
]
}
}

0 comments on commit cd051a4

Please sign in to comment.