Skip to content

Commit e9bb577

Browse files
tony-josi-awskarkhazmarkrtuttle
authored
Fix CBMC proofs for DNS (#718)
* Use CBMC XML output to enable VSCode debugger (#673) Prior to this commit, CBMC would emit logging information in plain text format, which does not contain information required for the CBMC VSCode debugger. This commit makes CBMC use XML instead of plain text. Co-authored-by: Mark Tuttle <[email protected]> * wip * wip DNSgetHostByName * wip DNSgetHostByName * fixed cbmc proof for DNS_ReadNameField * wip DNSgetHostByName_a_harness * Fix CBMC prooff for DNSgetHostByName * wip fix DNSgetHostByName_a CBMC proof * fixed cbmc target func not called issue in DNSclear * fixed cbmc target func not called issue in DNSlookup * fix DNSgetHostByName_a CBMC proof * update comments * more asserts * fixing formatting * updating as per review comments * fix dns after review comments * adding more asserts * adds more asserts * minor fix * fixing comments * fixing comments * fixing minor issue * fixing DNS_ReadReply() signature * making code more consistant * adding more asserts * making code more consistent --------- Co-authored-by: Kareem Khazem <[email protected]> Co-authored-by: Mark Tuttle <[email protected]>
1 parent ff11a14 commit e9bb577

File tree

13 files changed

+208
-54
lines changed

13 files changed

+208
-54
lines changed

‎source/FreeRTOS_DNS.c‎

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -157,8 +157,6 @@
157157
/* TODO: Fix IPv6 DNS query in Windows Simulator. */
158158
IPPreference_t xDNS_IP_Preference = xPreferenceIPv4;
159159

160-
/** @brief Used for additional error checking when asserts are enabled. */
161-
_static struct freertos_addrinfo * pxLastInfo = NULL;
162160
/*-----------------------------------------------------------*/
163161

164162
/**
@@ -315,7 +313,6 @@
315313

316314
if( pxInfo != NULL )
317315
{
318-
configASSERT( pxLastInfo != pxInfo );
319316

320317
while( pxIterator != NULL )
321318
{
@@ -325,7 +322,6 @@
325322
}
326323
}
327324

328-
pxLastInfo = NULL;
329325
}
330326
/*-----------------------------------------------------------*/
331327

@@ -621,7 +617,7 @@
621617
if( ulIPAddress != 0UL )
622618
{
623619
#if ( ipconfigUSE_IPv6 != 0 )
624-
if( ( *ppxAddressInfo )->ai_family == FREERTOS_AF_INET6 )
620+
if( ( ppxAddressInfo != NULL ) && ( ( *ppxAddressInfo )->ai_family == FREERTOS_AF_INET6 ) )
625621
{
626622
FreeRTOS_printf( ( "prvPrepareLookup: found '%s' in cache: %pip\n",
627623
pcHostName, ( *ppxAddressInfo )->xPrivateStorage.sockaddr.sin_address.xIP_IPv6.ucBytes ) );
@@ -663,7 +659,7 @@
663659
( xFamily == FREERTOS_AF_INET6 ) ? pdTRUE : pdFALSE );
664660
}
665661
}
666-
else if( ppxAddressInfo != NULL )
662+
else if( ( ppxAddressInfo != NULL ) && ( *( ppxAddressInfo ) != NULL ) )
667663
{
668664
/* The IP address is known, do the call-back now. */
669665
pCallbackFunction( pcHostName, pvSearchID, *( ppxAddressInfo ) );
@@ -950,6 +946,7 @@
950946
if( ( xDNS_IP_Preference == xPreferenceIPv6 ) && ENDPOINT_IS_IPv6( pxEndPoint ) )
951947
{
952948
uint8_t ucIndex = pxEndPoint->ipv6_settings.ucDNSIndex;
949+
configASSERT(ucIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT);
953950
uint8_t * ucBytes = pxEndPoint->ipv6_settings.xDNSServerAddresses[ ucIndex ].ucBytes;
954951

955952
/* Test if the DNS entry is in used. */
@@ -967,6 +964,7 @@
967964
#endif /* if ( ipconfigUSE_IPv6 != 0 ) */
968965
{
969966
uint8_t ucIndex = pxEndPoint->ipv4_settings.ucDNSIndex;
967+
configASSERT(ucIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT);
970968
uint32_t ulIPAddress = pxEndPoint->ipv4_settings.ulDNSServerAddresses[ ucIndex ];
971969

972970
if( ( ulIPAddress != 0U ) && ( ulIPAddress != ipBROADCAST_IP_ADDRESS ) )

‎source/FreeRTOS_DNS_Networking.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -136,7 +136,7 @@
136136
* @param xAddress address to read from
137137
* @param pxReceiveBuffer buffer to fill with received data
138138
*/
139-
BaseType_t DNS_ReadReply( const ConstSocket_t xDNSSocket,
139+
BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
140140
struct freertos_sockaddr * xAddress,
141141
struct xDNSBuffer * pxReceiveBuffer )
142142
{

‎source/include/FreeRTOS_DNS_Networking.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@
4646
const struct freertos_sockaddr * xAddress,
4747
const struct xDNSBuffer * pxDNSBuf );
4848

49-
BaseType_t DNS_ReadReply( const ConstSocket_t xDNSSocket,
49+
BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
5050
struct freertos_sockaddr * xAddress,
5151
struct xDNSBuffer * pxReceiveBuffer );
5252

‎test/cbmc/proofs/DNS/DNSclear/DNSclear_harness.c‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@
77
#include "FreeRTOS_DNS.h"
88
#include "FreeRTOS_IP_Private.h"
99

10+
void FreeRTOS_dnsclear( void );
11+
1012

1113
void harness()
1214
{

‎test/cbmc/proofs/DNS/DNSclear/Makefile.json‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111
"OBJS":
1212
[
1313
"$(ENTRY)_harness.goto",
14-
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto"
14+
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Cache.goto"
1515
],
1616
"DEF":
1717
[

‎test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c‎

Lines changed: 75 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -22,15 +22,17 @@
2222
uint32_t FreeRTOS_dnslookup( const char * pcHostName );
2323
Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks );
2424
void DNS_CloseSocket( Socket_t xDNSSocket );
25-
void DNS_ReadReply( Socket_t xDNSSocket,
25+
BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
2626
struct freertos_sockaddr * xAddress,
2727
struct xDNSBuffer * pxDNSBuf );
2828
uint32_t DNS_SendRequest( Socket_t xDNSSocket,
2929
struct freertos_sockaddr * xAddress,
3030
struct xDNSBuffer * pxDNSBuf );
3131
uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
32-
size_t xBufferLength,
33-
BaseType_t xExpected );
32+
size_t uxBufferLength,
33+
struct freertos_addrinfo ** ppxAddressInfo,
34+
BaseType_t xExpected,
35+
uint16_t usPort );
3436

3537
/****************************************************************
3638
* We abstract:
@@ -61,8 +63,10 @@ uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
6163
****************************************************************/
6264

6365
uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
64-
size_t xBufferLength,
65-
BaseType_t xExpected )
66+
size_t uxBufferLength,
67+
struct freertos_addrinfo ** ppxAddressInfo,
68+
BaseType_t xExpected,
69+
uint16_t usPort )
6670
{
6771
uint32_t size;
6872

@@ -94,32 +98,39 @@ uint32_t DNS_SendRequest( Socket_t xDNSSocket,
9498
* We stub out this function which returned a dns_buffer filled with random data
9599
*
96100
****************************************************************/
97-
void DNS_ReadReply( Socket_t xDNSSocket,
101+
BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
98102
struct freertos_sockaddr * xAddress,
99103
struct xDNSBuffer * pxDNSBuf )
100104
{
105+
BaseType_t ret;
101106
int len;
102107

103-
pxDNSBuf->pucPayloadBuffer = safeMalloc( len );
108+
__CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < CBMC_MAX_OBJECT_SIZE ) );
109+
110+
pxDNSBuf->pucPayloadBuffer = malloc( len );
104111

105112
pxDNSBuf->uxPayloadLength = len;
106113

107-
__CPROVER_assume( len < CBMC_MAX_OBJECT_SIZE );
108114
__CPROVER_assume( pxDNSBuf->pucPayloadBuffer != NULL );
109115

110-
__CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadSize );
116+
__CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadLength );
117+
118+
return ret;
111119
}
112120

113121

114122
void DNS_CloseSocket( Socket_t xDNSSocket )
115123
{
124+
__CPROVER_assert( xDNSSocket != NULL, "The xDNSSocket cannot be NULL." );
125+
free( xDNSSocket );
116126
}
117127

118128
Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks )
119129
{
120-
Socket_t sock;
121130

131+
Socket_t sock = malloc( sizeof(struct xSOCKET) );
122132
return sock;
133+
123134
}
124135

125136
uint32_t FreeRTOS_dnslookup( const char * pcHostName )
@@ -132,6 +143,16 @@ uint32_t FreeRTOS_dnslookup( const char * pcHostName )
132143
return ret;
133144
}
134145

146+
BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
147+
NetworkBufferDescriptor_t * const pxNetworkBuffer,
148+
BaseType_t xReleaseAfterSend )
149+
{
150+
__CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
151+
__CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
152+
__CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The ethernet buffer cannot be NULL." );
153+
BaseType_t ret;
154+
return ret;
155+
}
135156

136157
/****************************************************************
137158
* Abstract prvCreateDNSMessage
@@ -144,14 +165,40 @@ uint32_t FreeRTOS_dnslookup( const char * pcHostName )
144165

145166
size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer,
146167
const char * pcHostName,
147-
TickType_t uxIdentifier )
168+
TickType_t uxIdentifier,
169+
UBaseType_t uxHostType )
148170
{
149171
__CPROVER_havoc_object( pucUDPPayloadBuffer );
150172
size_t size;
151173

152174
return size;
153175
}
154176

177+
/*We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. */
178+
/*This is the mock to mimic the correct expected behavior. If this allocation fails, this might invalidate the proof. */
179+
NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
180+
TickType_t xBlockTimeTicks )
181+
{
182+
NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) malloc( sizeof( NetworkBufferDescriptor_t ) );
183+
184+
if( pxNetworkBuffer != NULL )
185+
{
186+
pxNetworkBuffer->pucEthernetBuffer = malloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET );
187+
if( pxNetworkBuffer->pucEthernetBuffer == NULL )
188+
{
189+
free( pxNetworkBuffer );
190+
pxNetworkBuffer = NULL;
191+
}
192+
else
193+
{
194+
pxNetworkBuffer->pucEthernetBuffer = ( (uint8_t *) pxNetworkBuffer->pucEthernetBuffer ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
195+
pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
196+
}
197+
}
198+
199+
return pxNetworkBuffer;
200+
}
201+
155202
/****************************************************************
156203
* The proof for FreeRTOS_gethostbyname.
157204
****************************************************************/
@@ -160,12 +207,28 @@ void harness()
160207
{
161208
size_t len;
162209

210+
pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
211+
__CPROVER_assume( pxNetworkEndPoints != NULL );
212+
213+
/* Asserts are added in the src code to make sure ucDNSIndex
214+
will be less than ipconfigENDPOINT_DNS_ADDRESS_COUNT */
215+
__CPROVER_assume( pxNetworkEndPoints->ipv6_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT );
216+
__CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT );
217+
pxNetworkEndPoints->pxNext = NULL;
218+
219+
/* Interface init. */
220+
pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
221+
__CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
222+
223+
pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
224+
163225
__CPROVER_assume( len <= MAX_HOSTNAME_LEN );
164-
char * pcHostName = safeMalloc( len );
226+
char * pcHostName = malloc( len );
165227

166228
__CPROVER_assume( len > 0 ); /* prvProcessDNSCache strcmp */
167229
__CPROVER_assume( pcHostName != NULL );
168230
pcHostName[ len - 1 ] = NULL;
169231

170232
FreeRTOS_gethostbyname( pcHostName );
233+
171234
}

‎test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,17 @@
88

99
"callback": 0,
1010
"MAX_HOSTNAME_LEN": 10,
11+
"ENDPOINT_DNS_ADDRESS_COUNT": 5,
1112
"HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1",
13+
"ENDPOINT_DNS_ADDRESS_COUNT_UNWIND": "__eval {ENDPOINT_DNS_ADDRESS_COUNT} + 1",
1214

1315
"CBMCFLAGS":
1416
[
1517
"--unwind 1",
18+
"--unwindset strchr.0:{HOSTNAME_UNWIND}",
19+
"--unwindset prvIncreaseDNS4Index.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}",
20+
"--unwindset prvIncreaseDNS6Index.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}",
21+
"--unwindset prvFillSockAddress.0:2,prvFillSockAddress.1:2",
1622
"--unwindset prvCreateDNSMessage.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.1:{HOSTNAME_UNWIND},strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},strcmp.0:{HOSTNAME_UNWIND},strcpy.0:{HOSTNAME_UNWIND}",
1723
"--unwindset prvGetHostByNameOp_WithRetry.0:{HOSTNAME_UNWIND}",
1824
"--nondet-static"
@@ -22,15 +28,17 @@
2228
[
2329
"$(ENTRY)_harness.goto",
2430
"$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
25-
"$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
31+
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
2632
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
2733
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
2834
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto"
2935
],
3036

3137
"DEF":
3238
[
39+
"ipconfigUSE_IPv6=1",
3340
"ipconfigDNS_USE_CALLBACKS={callback}",
34-
"MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}"
41+
"MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}",
42+
"ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}"
3543
]
3644
}

0 commit comments

Comments
 (0)