Fix CBMC proofs for DNS

source/FreeRTOS_DNS.c

@@ -157,8 +157,6 @@
 /* TODO: Fix IPv6 DNS query in Windows Simulator. */
     IPPreference_t xDNS_IP_Preference = xPreferenceIPv4;
 
-/** @brief Used for additional error checking when asserts are enabled. */
-    _static struct freertos_addrinfo * pxLastInfo = NULL;
 /*-----------------------------------------------------------*/
 
 /**
@@ -315,7 +313,6 @@
 
         if( pxInfo != NULL )
         {
-            configASSERT( pxLastInfo != pxInfo );
 
             while( pxIterator != NULL )
             {
@@ -325,7 +322,6 @@
             }
         }
 
-        pxLastInfo = NULL;
     }
 /*-----------------------------------------------------------*/
 
@@ -621,7 +617,7 @@
                     if( ulIPAddress != 0UL )
                     {
                         #if ( ipconfigUSE_IPv6 != 0 )
-                            if( ( *ppxAddressInfo )->ai_family == FREERTOS_AF_INET6 )
+                            if( ( ppxAddressInfo != NULL ) && ( ( *ppxAddressInfo )->ai_family == FREERTOS_AF_INET6 ) )
                             {
                                 FreeRTOS_printf( ( "prvPrepareLookup: found '%s' in cache: %pip\n",
                                                    pcHostName, ( *ppxAddressInfo )->xPrivateStorage.sockaddr.sin_address.xIP_IPv6.ucBytes ) );
@@ -663,7 +659,7 @@
                                                  ( xFamily == FREERTOS_AF_INET6 ) ? pdTRUE : pdFALSE );
                             }
                         }
-                        else if( ppxAddressInfo != NULL )
+                        else if( ( ppxAddressInfo != NULL ) && ( *( ppxAddressInfo ) != NULL ) )
                         {
                             /* The IP address is known, do the call-back now. */
                             pCallbackFunction( pcHostName, pvSearchID, *( ppxAddressInfo ) );
@@ -950,6 +946,7 @@
                     if( ( xDNS_IP_Preference == xPreferenceIPv6 ) && ENDPOINT_IS_IPv6( pxEndPoint ) )
                     {
                         uint8_t ucIndex = pxEndPoint->ipv6_settings.ucDNSIndex;
+                        configASSERT(ucIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT);
                         uint8_t * ucBytes = pxEndPoint->ipv6_settings.xDNSServerAddresses[ ucIndex ].ucBytes;
 
                         /* Test if the DNS entry is in used. */
@@ -967,6 +964,7 @@
                 #endif /* if ( ipconfigUSE_IPv6 != 0 ) */
                 {
                     uint8_t ucIndex = pxEndPoint->ipv4_settings.ucDNSIndex;
+                    configASSERT(ucIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT);
                     uint32_t ulIPAddress = pxEndPoint->ipv4_settings.ulDNSServerAddresses[ ucIndex ];
 
                     if( ( ulIPAddress != 0U ) && ( ulIPAddress != ipBROADCAST_IP_ADDRESS ) )

source/FreeRTOS_DNS_Networking.c

@@ -136,7 +136,7 @@
  * @param xAddress address to read from
  * @param pxReceiveBuffer buffer to fill with received data
  */
-    BaseType_t DNS_ReadReply( const ConstSocket_t xDNSSocket,
+    BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
                               struct freertos_sockaddr * xAddress,
                               struct xDNSBuffer * pxReceiveBuffer )
     {

source/include/FreeRTOS_DNS_Networking.h

@@ -46,7 +46,7 @@
                                 const struct freertos_sockaddr * xAddress,
                                 const struct xDNSBuffer * pxDNSBuf );
 
-    BaseType_t DNS_ReadReply( const ConstSocket_t xDNSSocket,
+    BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
                               struct freertos_sockaddr * xAddress,
                               struct xDNSBuffer * pxReceiveBuffer );
 

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

@@ -7,6 +7,8 @@
 #include "FreeRTOS_DNS.h"
 #include "FreeRTOS_IP_Private.h"
 
+void FreeRTOS_dnsclear( void );
+
 
 void harness()
 {

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

@@ -11,7 +11,7 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Cache.goto"
   ],
   "DEF":
   [

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

@@ -22,15 +22,17 @@
 uint32_t FreeRTOS_dnslookup( const char * pcHostName );
 Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks );
 void DNS_CloseSocket( Socket_t xDNSSocket );
-void DNS_ReadReply( Socket_t xDNSSocket,
+BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
                     struct freertos_sockaddr * xAddress,
                     struct xDNSBuffer * pxDNSBuf );
 uint32_t DNS_SendRequest( Socket_t xDNSSocket,
                           struct freertos_sockaddr * xAddress,
                           struct xDNSBuffer * pxDNSBuf );
 uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
-                            size_t xBufferLength,
-                            BaseType_t xExpected );
+                            size_t uxBufferLength,
+                            struct freertos_addrinfo ** ppxAddressInfo,
+                            BaseType_t xExpected,
+                            uint16_t usPort );
 
 /****************************************************************
 * We abstract:
@@ -61,8 +63,10 @@ uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
 ****************************************************************/
 
 uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
-                            size_t xBufferLength,
-                            BaseType_t xExpected )
+                            size_t uxBufferLength,
+                            struct freertos_addrinfo ** ppxAddressInfo,
+                            BaseType_t xExpected,
+                            uint16_t usPort )
 {
     uint32_t size;
 
@@ -94,32 +98,39 @@ uint32_t DNS_SendRequest( Socket_t xDNSSocket,
 * We stub out this function which returned a dns_buffer filled with random data
 *
 ****************************************************************/
-void DNS_ReadReply( Socket_t xDNSSocket,
+BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
                     struct freertos_sockaddr * xAddress,
                     struct xDNSBuffer * pxDNSBuf )
 {
+    BaseType_t ret;
     int len;
 
-    pxDNSBuf->pucPayloadBuffer = safeMalloc( len );
+    __CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < CBMC_MAX_OBJECT_SIZE ) );
+
+    pxDNSBuf->pucPayloadBuffer = malloc( len );
 
     pxDNSBuf->uxPayloadLength = len;
 
-    __CPROVER_assume( len < CBMC_MAX_OBJECT_SIZE );
     __CPROVER_assume( pxDNSBuf->pucPayloadBuffer != NULL );
 
-    __CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadSize );
+    __CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadLength );
+
+    return ret;
 }
 
 
 void DNS_CloseSocket( Socket_t xDNSSocket )
 {
+    __CPROVER_assert( xDNSSocket != NULL, "The xDNSSocket cannot be NULL." );
+    free( xDNSSocket );
 }
 
 Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks )
 {
-    Socket_t sock;
 
+    Socket_t sock = malloc( sizeof(struct xSOCKET) );
     return sock;
+
 }
 
 uint32_t FreeRTOS_dnslookup( const char * pcHostName )
@@ -132,6 +143,16 @@ uint32_t FreeRTOS_dnslookup( const char * pcHostName )
     return ret;
 }
 
+BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
+                                                NetworkBufferDescriptor_t * const pxNetworkBuffer,
+                                                BaseType_t xReleaseAfterSend )
+{
+    __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The ethernet buffer cannot be NULL." );
+    BaseType_t ret;
+    return ret;
+}
 
 /****************************************************************
 * Abstract prvCreateDNSMessage
@@ -144,14 +165,40 @@ uint32_t FreeRTOS_dnslookup( const char * pcHostName )
 
 size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer,
                             const char * pcHostName,
-                            TickType_t uxIdentifier )
+                            TickType_t uxIdentifier,
+                            UBaseType_t uxHostType )
 {
     __CPROVER_havoc_object( pucUDPPayloadBuffer );
     size_t size;
 
     return size;
 }
 
+/*We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. */
+/*This is the mock to mimic the correct expected behavior. If this allocation fails, this might invalidate the proof. */
+NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
+                                                              TickType_t xBlockTimeTicks )
+{
+    NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) malloc( sizeof( NetworkBufferDescriptor_t ) );
+
+    if( pxNetworkBuffer != NULL )
+    {
+        pxNetworkBuffer->pucEthernetBuffer = malloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET );
+        if( pxNetworkBuffer->pucEthernetBuffer == NULL )
+        {
+            free( pxNetworkBuffer );
+            pxNetworkBuffer = NULL;
+        }
+        else 
+        {
+            pxNetworkBuffer->pucEthernetBuffer = ( (uint8_t *) pxNetworkBuffer->pucEthernetBuffer ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
+            pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
+        }
+    }
+
+    return pxNetworkBuffer;
+}
+
 /****************************************************************
 * The proof for FreeRTOS_gethostbyname.
 ****************************************************************/
@@ -160,12 +207,28 @@ void harness()
 {
     size_t len;
 
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+
+    /* Asserts are added in the src code to make sure ucDNSIndex 
+    will be less than ipconfigENDPOINT_DNS_ADDRESS_COUNT  */
+    __CPROVER_assume( pxNetworkEndPoints->ipv6_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); 
+    __CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); 
+    pxNetworkEndPoints->pxNext = NULL;
+
+    /* Interface init. */
+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+
+    pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
+
     __CPROVER_assume( len <= MAX_HOSTNAME_LEN );
-    char * pcHostName = safeMalloc( len );
+    char * pcHostName = malloc( len );
 
     __CPROVER_assume( len > 0 ); /* prvProcessDNSCache strcmp */
     __CPROVER_assume( pcHostName != NULL );
     pcHostName[ len - 1 ] = NULL;
 
     FreeRTOS_gethostbyname( pcHostName );
+
 }

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

@@ -8,11 +8,17 @@
 
   "callback": 0,
   "MAX_HOSTNAME_LEN": 10,
+  "ENDPOINT_DNS_ADDRESS_COUNT": 5,
   "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1",
+  "ENDPOINT_DNS_ADDRESS_COUNT_UNWIND": "__eval {ENDPOINT_DNS_ADDRESS_COUNT} + 1",
 
   "CBMCFLAGS":
   [
     "--unwind 1",
+    "--unwindset strchr.0:{HOSTNAME_UNWIND}", 
+    "--unwindset prvIncreaseDNS4Index.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}",
+    "--unwindset prvIncreaseDNS6Index.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}",
+    "--unwindset prvFillSockAddress.0:2,prvFillSockAddress.1:2",
     "--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}",
     "--unwindset prvGetHostByNameOp_WithRetry.0:{HOSTNAME_UNWIND}",
     "--nondet-static"
@@ -22,15 +28,17 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
-    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto"
   ],
 
   "DEF":
   [
+    "ipconfigUSE_IPv6=1",
     "ipconfigDNS_USE_CALLBACKS={callback}",
-    "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}"
+    "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}",
+    "ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}"
   ]
 }