Fix potential out of bounds write (CWE-787) when processing LLMNR or mDNS queries

source/FreeRTOS_DNS_Parser.c

@@ -486,31 +486,30 @@
                             LLMNRAnswer_t * pxAnswer;
                             uint8_t * pucNewBuffer = NULL;
                             size_t uxExtraLength;
+                            size_t uxDataLength = uxBufferLength +
+                                                  sizeof( UDPHeader_t ) +
+                                                  sizeof( EthernetHeader_t ) +
+                                                  uxIPHeaderSizePacket( pxNetworkBuffer );
 
-                            if( xBufferAllocFixedSize == pdFALSE )
-                            {
-                                size_t uxDataLength = uxBufferLength +
-                                                      sizeof( UDPHeader_t ) +
-                                                      sizeof( EthernetHeader_t ) +
-                                                      uxIPHeaderSizePacket( pxNetworkBuffer );
-
-                                #if ( ipconfigUSE_IPv6 != 0 )
-                                    if( xSet.usType == dnsTYPE_AAAA_HOST )
-                                    {
-                                        uxExtraLength = sizeof( LLMNRAnswer_t ) + ipSIZE_OF_IPv6_ADDRESS - sizeof( pxAnswer->ulIPAddress );
-                                    }
-                                    else
-                                #endif /* ( ipconfigUSE_IPv6 != 0 ) */
-                                #if ( ipconfigUSE_IPv4 != 0 )
-                                {
-                                    uxExtraLength = sizeof( LLMNRAnswer_t );
-                                }
-                                #else /* ( ipconfigUSE_IPv4 != 0 ) */
+                            #if ( ipconfigUSE_IPv6 != 0 )
+                                if( xSet.usType == dnsTYPE_AAAA_HOST )
                                 {
-                                    /* do nothing, coverity happy */
+                                    uxExtraLength = sizeof( LLMNRAnswer_t ) + ipSIZE_OF_IPv6_ADDRESS - sizeof( pxAnswer->ulIPAddress );
                                 }
-                                #endif /* ( ipconfigUSE_IPv4 != 0 ) */
+                                else
+                            #endif /* ( ipconfigUSE_IPv6 != 0 ) */
+                            #if ( ipconfigUSE_IPv4 != 0 )
+                            {
+                                uxExtraLength = sizeof( LLMNRAnswer_t );
+                            }
+                            #else /* ( ipconfigUSE_IPv4 != 0 ) */
+                            {
+                                /* do nothing, coverity happy */
+                            }
+                            #endif /* ( ipconfigUSE_IPv4 != 0 ) */
 
+                            if( xBufferAllocFixedSize == pdFALSE )
+                            {
                                 /* Set the size of the outgoing packet. */
                                 pxNetworkBuffer->xDataLength = uxDataLength;
                                 pxNewBuffer = pxDuplicateNetworkBufferWithDescriptor( pxNetworkBuffer,
@@ -539,7 +538,17 @@
                             }
                             else
                             {
-                                pucNewBuffer = &( pxNetworkBuffer->pucEthernetBuffer[ uxUDPOffset ] );
+                                /* When xBufferAllocFixedSize is TRUE, check if the buffer size is big enough to
+                                 * store the answer. */
+                                if( ( uxDataLength + uxExtraLength ) <= ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER )
+                                {
+                                    pucNewBuffer = &( pxNetworkBuffer->pucEthernetBuffer[ uxUDPOffset ] );
+                                }
+                                else
+                                {
+                                    /* Just to indicate that the message may not be answered. */
+                                    pxNetworkBuffer = NULL;
+                                }
                             }
 
                             if( ( pxNetworkBuffer != NULL ) )
@@ -1214,7 +1223,11 @@
                 {
                     /* BufferAllocation_1.c is used, the Network Buffers can contain at least
                      * ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER. */
-                    configASSERT( uxSizeNeeded < ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER );
+                    if( uxSizeNeeded > ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) )
+                    {
+                        /* The buffer is too small to reply. Drop silently. */
+                        break;
+                    }
                 }
 
                 pxNetworkBuffer->xDataLength = uxSizeNeeded;

source/portable/BufferManagement/BufferAllocation_1.c

@@ -237,11 +237,8 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
     BaseType_t xInvalid = pdFALSE;
     UBaseType_t uxCount;
 
-    /* The current implementation only has a single size memory block, so
-     * the requested size parameter is not used (yet). */
-    ( void ) xRequestedSizeBytes;
-
-    if( xNetworkBufferSemaphore != NULL )
+    if( ( xNetworkBufferSemaphore != NULL ) &&
+        ( xRequestedSizeBytes <= ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) ) )
     {
         /* If there is a semaphore available, there is a network buffer
          * available. */
@@ -432,10 +429,18 @@ UBaseType_t uxGetNumberOfFreeNetworkBuffers( void )
 NetworkBufferDescriptor_t * pxResizeNetworkBufferWithDescriptor( NetworkBufferDescriptor_t * pxNetworkBuffer,
                                                                  size_t xNewSizeBytes )
 {
-    /* In BufferAllocation_1.c all network buffer are allocated with a
-     * maximum size of 'ipTOTAL_ETHERNET_FRAME_SIZE'.No need to resize the
-     * network buffer. */
-    pxNetworkBuffer->xDataLength = xNewSizeBytes;
+    if( xNewSizeBytes <= ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) )
+    {
+        /* In BufferAllocation_1.c all network buffer are allocated with a
+         * maximum size of 'ipTOTAL_ETHERNET_FRAME_SIZE'.No need to resize the
+         * network buffer. */
+        pxNetworkBuffer->xDataLength = xNewSizeBytes;
+    }
+    else
+    {
+        pxNetworkBuffer = NULL;
+    }
+
     return pxNetworkBuffer;
 }
 

test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c

@@ -122,10 +122,7 @@ void harness()
 
     BaseType_t xDataSize;
 
-    /* When re-adjusting the buffer, (sizeof( NBNSAnswer_t ) - 2 * sizeof( uint16_t )) more bytes are
-     * required to be added to the existing buffer. Make sure total bytes doesn't exceed  ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER
-     * when re-resizing. This will prevent hitting an assert if Buffer Allocation 1 is used. */
-    __CPROVER_assume( ( xDataSize != 0 ) && ( xDataSize < ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER - ( sizeof( NBNSAnswer_t ) - 2 * sizeof( uint16_t ) ) ) ) );
+    __CPROVER_assume( ( xDataSize > 0 ) && ( xDataSize < ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) ) );
 
     xNetworkBuffer.pucEthernetBuffer = safeMalloc( xDataSize );
     xNetworkBuffer.xDataLength = xDataSize;

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

@@ -24,6 +24,7 @@
   "DEF":
   [
     "ipconfigUSE_DNS_CACHE={USE_CACHE}",
-    "ipconfigUSE_NBNS=1"
+    "ipconfigUSE_NBNS=1",
+    "ipconfigNETWORK_MTU=586"
   ]
 }

test/cbmc/proofs/DNS_ParseDNSReply/Configurations.json

@@ -1,16 +1,18 @@
 {
   "ENTRY": "DNS_ParseDNSReply",
-  "TEST_PAYLOAD_SIZE": 2,
-  "TEST_IPV4_PACKET_SIZE": 29,
-  "TEST_IPV6_PACKET_SIZE": 49,
+  "TEST_MAX_TEST_UNWIND_LOOP": 6,
+  "TEST_MIN_TEST_DNS_HEADER": 12,
+  "TEST_MIN_IPV4_UDP_PACKET_SIZE": 42,
+  "TEST_MIN_IPV6_UDP_PACKET_SIZE": 62,
+  "TEST_IPV4_NETWORK_MTU": "__eval {TEST_MIN_IPV4_UDP_PACKET_SIZE} + {TEST_MIN_TEST_DNS_HEADER} + {TEST_MAX_TEST_UNWIND_LOOP}",
+  "TEST_IPV6_NETWORK_MTU": "__eval {TEST_MIN_IPV6_UDP_PACKET_SIZE} + {TEST_MIN_TEST_DNS_HEADER} + {TEST_MAX_TEST_UNWIND_LOOP}",
   "CBMCFLAGS":
   [
     "--unwind 1",
-    "--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}"
+    "--unwindset strlen.0:{TEST_MAX_TEST_UNWIND_LOOP}",
+    "--unwindset DNS_ParseDNSReply.0:{TEST_MAX_TEST_UNWIND_LOOP}",
+    "--unwindset DNS_ReadNameField.0:{TEST_MAX_TEST_UNWIND_LOOP}",
+    "--unwindset DNS_ReadNameField.1:{TEST_MAX_TEST_UNWIND_LOOP}"
   ],
   "OPT":
   [
@@ -25,21 +27,63 @@
   "DEF":
   [
     {
-      "IPv4":
+      "IPv4_FixedNetworkBufferSize":
       [
-        "TEST_PACKET_SIZE={TEST_IPV4_PACKET_SIZE}",
+        "TEST_MAX_PAYLOAD_SIZE={TEST_MAX_TEST_UNWIND_LOOP}",
         "ipconfigUSE_LLMNR=1",
         "ipconfigUSE_MDNS=1",
-        "IS_TESTING_IPV6=0"
+        "IS_TESTING_IPV6=0",
+        "IS_BUFFER_ALLOCATE_FIXED=1",
+        "ipconfigNETWORK_MTU={TEST_IPV4_NETWORK_MTU}",
+        "ipconfigUSE_TCP=0",
+        "ipconfigUSE_DHCP=0",
+        "ipconfigTCP_MSS=536",
+        "ipconfigDNS_CACHE_NAME_LENGTH={TEST_MAX_TEST_UNWIND_LOOP}"
       ]
     },
     {
-      "IPv6":
+      "IPv6_FixedNetworkBufferSize":
       [
-        "TEST_PACKET_SIZE={TEST_IPV6_PACKET_SIZE}",
+        "TEST_MAX_PAYLOAD_SIZE={TEST_MAX_TEST_UNWIND_LOOP}",
         "ipconfigUSE_LLMNR=1",
         "ipconfigUSE_MDNS=1",
-        "IS_TESTING_IPV6=1"
+        "IS_TESTING_IPV6=1",
+        "IS_BUFFER_ALLOCATE_FIXED=1",
+        "ipconfigNETWORK_MTU={TEST_IPV6_NETWORK_MTU}",
+        "ipconfigUSE_TCP=0",
+        "ipconfigUSE_DHCP=0",
+        "ipconfigTCP_MSS=536",
+        "ipconfigDNS_CACHE_NAME_LENGTH={TEST_MAX_TEST_UNWIND_LOOP}"
+      ]
+    },
+    {
+      "IPv4_DynamicNetworkBufferSize":
+      [
+        "TEST_MAX_PAYLOAD_SIZE={TEST_MAX_TEST_UNWIND_LOOP}",
+        "ipconfigUSE_LLMNR=1",
+        "ipconfigUSE_MDNS=1",
+        "IS_TESTING_IPV6=0",
+        "IS_BUFFER_ALLOCATE_FIXED=0",
+        "ipconfigNETWORK_MTU={TEST_IPV4_NETWORK_MTU}",
+        "ipconfigUSE_TCP=0",
+        "ipconfigUSE_DHCP=0",
+        "ipconfigTCP_MSS=536",
+        "ipconfigDNS_CACHE_NAME_LENGTH={TEST_MAX_TEST_UNWIND_LOOP}"
+      ]
+    },
+    {
+      "IPv6_DynamicNetworkBufferSize":
+      [
+        "TEST_MAX_PAYLOAD_SIZE={TEST_MAX_TEST_UNWIND_LOOP}",
+        "ipconfigUSE_LLMNR=1",
+        "ipconfigUSE_MDNS=1",
+        "IS_TESTING_IPV6=1",
+        "IS_BUFFER_ALLOCATE_FIXED=0",
+        "ipconfigNETWORK_MTU={TEST_IPV6_NETWORK_MTU}",
+        "ipconfigUSE_TCP=0",
+        "ipconfigUSE_DHCP=0",
+        "ipconfigTCP_MSS=536",
+        "ipconfigDNS_CACHE_NAME_LENGTH={TEST_MAX_TEST_UNWIND_LOOP}"
       ]
     }
   ],

test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c

@@ -10,14 +10,16 @@
 
 /* FreeRTOS+TCP includes. */
 #include "FreeRTOS_IP.h"
+#include "FreeRTOS_IP_Private.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"
+
+const BaseType_t xBufferAllocFixedSize = IS_BUFFER_ALLOCATE_FIXED;
 
 /****************************************************************
 * Signature of function under test
@@ -60,12 +62,18 @@ NetworkBufferDescriptor_t * pxUDPPayloadBuffer_to_NetworkBuffer( const void * pv
 
 uint32_t ulChar2u32( const uint8_t * pucPtr )
 {
+    uint32_t ret;
+
     __CPROVER_assert( __CPROVER_r_ok( pucPtr, 4 ), "must be 4 bytes legal address to read" );
+    return ret;
 }
 
 uint16_t usChar2u16( const uint8_t * pucPtr )
 {
+    uint16_t ret;
+
     __CPROVER_assert( __CPROVER_r_ok( pucPtr, 2 ), "must be 2 bytes legal address to read" );
+    return ret;
 }
 
 const char * FreeRTOS_inet_ntop( BaseType_t xAddressFamily,
@@ -131,11 +139,14 @@ NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const Networ
 {
     NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
 
-    if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) )
+    if( pxNetworkBuffer != NULL )
     {
         pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xNewLength );
-        __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer );
+        __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
         pxNetworkBuffer->xDataLength = xNewLength;
+
+        pxNetworkBuffer->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL );
     }
 
     return pxNetworkBuffer;
@@ -176,23 +187,31 @@ void harness()
     uint8_t * pPayloadBuffer;
     size_t uxPayloadBufferLength;
 
-    __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 <= TEST_PACKET_SIZE );
+    __CPROVER_assume( uxBufferLength <= ipconfigNETWORK_MTU );
+    __CPROVER_assume( pxNetworkEndPoint_Temp != NULL );
 
     lIsIPv6Packet = IS_TESTING_IPV6;
 
-    xNetworkBuffer.pucEthernetBuffer = safeMalloc( uxBufferLength );
-    xNetworkBuffer.xDataLength = uxBufferLength;
-    xNetworkBuffer.pxEndPoint = pxNetworkEndPoint_Temp;
+    if( xBufferAllocFixedSize != pdFALSE )
+    {
+        /* When xBufferAllocFixedSize is true, buffers in all network descriptors
+         * is big enough to allow all Ethernet packet. */
+        xNetworkBuffer.pucEthernetBuffer = safeMalloc( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER );
+        xNetworkBuffer.xDataLength = uxBufferLength;
+        xNetworkBuffer.pxEndPoint = pxNetworkEndPoint_Temp;
+    }
+    else
+    {
+        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. */
+        __CPROVER_assume( uxBufferLength >= ulIpv6UdpOffset ); /* 62 is total size of IPv6 UDP header, including ethernet, IPv6, UDP headers. */
         pPayloadBuffer = xNetworkBuffer.pucEthernetBuffer + ulIpv6UdpOffset;
         uxPayloadBufferLength = uxBufferLength - ulIpv6UdpOffset;
     }

test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c

@@ -47,8 +47,7 @@ void prvTCPReturnPacket( FreeRTOS_Socket_t * pxSocket,
                          uint32_t ulLen,
                          BaseType_t xReleaseAfterSend )
 {
-    __CPROVER_assert( pxSocket != NULL, "pxSocket should not be NULL" );
-    __CPROVER_assert( pxDescriptor != NULL, "pxDescriptor should not be NULL" );
+    __CPROVER_assert( pxSocket != NULL || pxDescriptor != NULL, "Either pxSocket or pxDescriptor must be non-NULL" );
     __CPROVER_assert( pxDescriptor->pucEthernetBuffer != NULL, "pucEthernetBuffer should not be NULL" );
 }
 
@@ -57,11 +56,14 @@ int32_t prvTCPPrepareSend( FreeRTOS_Socket_t * pxSocket,
                            NetworkBufferDescriptor_t ** ppxNetworkBuffer,
                            UBaseType_t uxOptionsLength )
 {
+    int32_t ret = nondet_int32();
+
     __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
     __CPROVER_assert( *ppxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" );
     __CPROVER_assert( __CPROVER_r_ok( ( *ppxNetworkBuffer )->pucEthernetBuffer, ( *ppxNetworkBuffer )->xDataLength ), "Data in *ppxNetworkBuffer must be readable" );
 
-    return nondet_int32();
+    __CPROVER_assume( ret >= 0 && ret <= ipconfigNETWORK_MTU );
+    return ret;
 }
 
 /* prvTCPHandleState is proven separately. */
@@ -137,6 +139,7 @@ FreeRTOS_Socket_t * pxTCPSocketLookup( uint32_t ulLocalIP,
     {
         /* This test case is for IPv4. */
         __CPROVER_assume( xRetSocket->bits.bIsIPv6 == pdFALSE );
+        __CPROVER_assume( xRetSocket->u.xTCP.ucPeerWinScaleFactor <= tcpTCP_OPT_WSOPT_MAXIMUM_VALUE );
     }
 
     return xRetSocket;
@@ -151,7 +154,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 +177,12 @@ size_t uxIPHeaderSizeSocket( const FreeRTOS_Socket_t * pxSocket )
 void harness()
 {
     NetworkBufferDescriptor_t * pxNetworkBuffer;
+    size_t tcpPacketSize;
+
+    __CPROVER_assume( tcpPacketSize >= ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv4_HEADER + sizeof( TCPHeader_t ) ) );
+
+    pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( tcpPacketSize, 0 );
 
-    pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( sizeof( TCPPacket_t ), 0 );
 
     /* To avoid asserting on the network buffer being NULL. */
     __CPROVER_assume( pxNetworkBuffer != NULL );