Fix DHCP v4/v6 race condition and memory leak

source/FreeRTOS_DHCP.c

@@ -209,14 +209,21 @@
             uint8_t * pucUDPPayload = NULL;
             const DHCPMessage_IPv4_t * pxDHCPMessage;
             int32_t lBytes;
+            struct freertos_sockaddr xSourceAddress;
+            BaseType_t xFristIter = pdTRUE;
+
+            memset( &xSourceAddress, 0, sizeof( xSourceAddress ) );
 
             while( EP_DHCPData.xDHCPSocket != NULL )
             {
                 BaseType_t xRecvFlags = FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK;
                 NetworkEndPoint_t * pxIterator = NULL;
+                struct freertos_sockaddr xSourceAddressCurrent;
+                socklen_t xSourceAddressCurrentLength = 0;
+                pucUDPPayload = NULL;
 
                 /* Peek the next UDP message. */
-                lBytes = FreeRTOS_recvfrom( EP_DHCPData.xDHCPSocket, &( pucUDPPayload ), 0, xRecvFlags, NULL, NULL );
+                lBytes = FreeRTOS_recvfrom( EP_DHCPData.xDHCPSocket, &( pucUDPPayload ), 0, xRecvFlags, &xSourceAddressCurrent, &xSourceAddressCurrentLength );
 
                 if( lBytes < ( ( int32_t ) sizeof( DHCPMessage_IPv4_t ) ) )
                 {
@@ -225,9 +232,20 @@
                         FreeRTOS_printf( ( "vDHCPProcess: FreeRTOS_recvfrom returns %d\n", ( int ) lBytes ) );
                     }
 
+                    if( ( lBytes >= 0 ) && ( pucUDPPayload != NULL ) )
+                    {
+                        FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload );
+                    }
+
                     break;
                 }
 
+                if( xFristIter == pdTRUE )
+                {
+                    memcpy( &xSourceAddress, &xSourceAddressCurrent, xSourceAddressCurrentLength );
+                    xFristIter = pdFALSE;
+                }
+
                 /* Map a DHCP structure onto the received data. */
                 /* MISRA Ref 11.3.1 [Misaligned access] */
                 /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
@@ -239,10 +257,12 @@
                 {
                     pxIterator = pxNetworkEndPoints;
 
-                    /* Find the end-point with given transaction ID. */
+                    /* Find the end-point with given transaction ID and verify DHCP server address. */
                     while( pxIterator != NULL )
                     {
-                        if( pxDHCPMessage->ulTransactionID == FreeRTOS_htonl( pxIterator->xDHCPData.ulTransactionId ) )
+                        if( ( pxDHCPMessage->ulTransactionID == FreeRTOS_htonl( pxIterator->xDHCPData.ulTransactionId ) ) &&
+                            ( ( xSourceAddress.sin_address.ulIP_IPv4 == xSourceAddressCurrent.sin_address.ulIP_IPv4 ) &&
+                              ( xSourceAddress.sin_port == xSourceAddressCurrent.sin_port ) ) )
                         {
                             break;
                         }

source/FreeRTOS_DHCPv6.c

@@ -421,14 +421,21 @@ void vDHCPv6Process( BaseType_t xReset,
 
         BaseType_t lBytes;
         size_t uxLength;
+        struct freertos_sockaddr xSourceAddress;
+        BaseType_t xFristIter = pdTRUE;
+
+        memset( &xSourceAddress, 0, sizeof( xSourceAddress ) );
 
         for( ; ; )
         {
             BaseType_t xResult;
             BaseType_t xRecvFlags = ( BaseType_t ) FREERTOS_ZERO_COPY;
+            struct freertos_sockaddr xSourceAddressCurrent;
+            socklen_t xSourceAddressCurrentLength = 0;
+            pucUDPPayload = NULL;
 
             /* Get the next UDP message. */
-            lBytes = FreeRTOS_recvfrom( EP_DHCPData.xDHCPSocket, &( pucUDPPayload ), 0, xRecvFlags, NULL, NULL );
+            lBytes = FreeRTOS_recvfrom( EP_DHCPData.xDHCPSocket, &( pucUDPPayload ), 0, xRecvFlags, &xSourceAddressCurrent, &xSourceAddressCurrentLength );
 
             if( lBytes <= 0 )
             {
@@ -437,19 +444,39 @@ void vDHCPv6Process( BaseType_t xReset,
                     FreeRTOS_printf( ( "vDHCPProcess: FreeRTOS_recvfrom returns %d\n", ( int ) lBytes ) );
                 }
 
+                if( ( lBytes == 0 ) && ( pucUDPPayload != NULL ) )
+                {
+                    FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload );
+                }
+
                 break;
             }
 
-            uxLength = ( size_t ) lBytes;
+            if( xFristIter == pdTRUE )
+            {
+                memcpy( &xSourceAddress, &xSourceAddressCurrent, sizeof( xSourceAddress ) );
+                xFristIter = pdFALSE;
+            }
+
+            /* Verify DHCPv6 server address. */
+            if( ( memcmp( &( xSourceAddress.sin_address.xIP_IPv6.ucBytes ),        \
+                          &( xSourceAddressCurrent.sin_address.xIP_IPv6.ucBytes ), \
+                          sizeof( xSourceAddressCurrent.sin_address.xIP_IPv6.ucBytes ) ) == 0 ) &&
+                ( xSourceAddress.sin_port == xSourceAddressCurrent.sin_port ) )
+            {
+                uxLength = ( size_t ) lBytes;
 
-            xResult = prvDHCPv6Analyse( pxEndPoint, pucUDPPayload, uxLength, &( xDHCPMessage ) );
+                xResult = prvDHCPv6Analyse( pxEndPoint, pucUDPPayload, uxLength, &( xDHCPMessage ) );
 
-            FreeRTOS_printf( ( "prvDHCPv6Analyse: %s\n", ( xResult == pdPASS ) ? "Pass" : "Fail" ) );
+                FreeRTOS_printf( ( "prvDHCPv6Analyse: %s\n", ( xResult == pdPASS ) ? "Pass" : "Fail" ) );
 
-            if( xResult == pdPASS )
-            {
-                xDoProcess = xDHCPv6Process_PassReplyToEndPoint( pxEndPoint );
+                if( xResult == pdPASS )
+                {
+                    xDoProcess = xDHCPv6Process_PassReplyToEndPoint( pxEndPoint );
+                }
             }
+
+            FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload );
         }
     }
 

test/cbmc/proofs/DHCPv6/DHCPv6Process/DHCPv6Process_harness.c

@@ -153,6 +153,16 @@ int32_t FreeRTOS_recvfrom( Socket_t xSocket,
     return retVal;
 }
 
+/* For the purpose of this proof we stub the
+ * implementation of FreeRTOS_ReleaseUDPPayloadBuffer here, but make sure that
+ * the pvBuffer is not NULL, its not verified here if the pointer is a valid
+ * payload buffer as its proved in other proofs */
+void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer )
+{
+    __CPROVER_assert( pvBuffer != NULL,
+                      "FreeRTOS precondition: pvBuffer != NULL" );
+}
+
 void harness()
 {
     BaseType_t xReset;

test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json

@@ -5,6 +5,7 @@
     "CBMCFLAGS":
     [
       "--unwind {LOOP_UNWIND_COUNT}",
+      "--unwindset memcmp.0:17",
       "--nondet-static --flush"
     ],
     "OPT":

test/unit-test/FreeRTOS_DHCP/FreeRTOS_DHCP_stubs.c

@@ -41,6 +41,8 @@ static int32_t ulGenericLength;
 static NetworkBufferDescriptor_t * pxGlobalNetworkBuffer[ 10 ];
 static uint8_t GlobalBufferCounter = 0;
 
+struct freertos_sockaddr xSourceAddress, xSourceAddress2;
+
 static uint8_t pucUDPBuffer[ xSizeofUDPBuffer ];
 
 static uint8_t DHCP_header[] =
@@ -346,6 +348,16 @@ static int32_t FreeRTOS_recvfrom_ResetAndIncorrectStateWithSocketAlreadyCreated_
         *( ( uint8_t ** ) pvBuffer ) = pucUDPBuffer;
     }
 
+    if( pxSourceAddress != NULL )
+    {
+        memcpy( pxSourceAddress, &xSourceAddress, sizeof( xSourceAddress ) );
+    }
+
+    if( pxSourceAddressLength != NULL )
+    {
+        *pxSourceAddressLength = sizeof( xSourceAddress );
+    }
+
     memset( pucUDPBuffer, 0, xSizeofUDPBuffer );
     /* Put in correct DHCP cookie. */
     ( ( struct xDHCPMessage_IPv4 * ) pucUDPBuffer )->ulDHCPCookie = dhcpCOOKIE;
@@ -355,6 +367,55 @@ static int32_t FreeRTOS_recvfrom_ResetAndIncorrectStateWithSocketAlreadyCreated_
     return xSizeofUDPBuffer;
 }
 
+static int32_t FreeRTOS_recvfrom_LoopedCall( const ConstSocket_t xSocket,
+                                             void * pvBuffer,
+                                             size_t uxBufferLength,
+                                             BaseType_t xFlags,
+                                             struct freertos_sockaddr * pxSourceAddress,
+                                             socklen_t * pxSourceAddressLength,
+                                             int callbacks )
+{
+    NetworkEndPoint_t * pxIterator = pxNetworkEndPoints;
+    size_t xSizeRetBufferSize = xSizeofUDPBuffer;
+
+    if( callbacks == 2 )
+    {
+        pxNetworkEndPoints->xDHCPData.eDHCPState = eInitialWait;
+    }
+    else if( callbacks == 4 )
+    {
+        xSizeRetBufferSize = 200;
+    }
+
+    if( ( xFlags & FREERTOS_ZERO_COPY ) != 0 )
+    {
+        *( ( uint8_t ** ) pvBuffer ) = pucUDPBuffer;
+    }
+
+    if( pxSourceAddress != NULL )
+    {
+        if( callbacks == 2 )
+        {
+            xSourceAddress2.sin_port = 6060;
+        }
+
+        memcpy( pxSourceAddress, &xSourceAddress2, sizeof( xSourceAddress2 ) );
+    }
+
+    if( pxSourceAddressLength != NULL )
+    {
+        *pxSourceAddressLength = sizeof( xSourceAddress2 );
+    }
+
+    memset( pucUDPBuffer, 0, xSizeofUDPBuffer );
+    /* Put in correct DHCP cookie. */
+    ( ( struct xDHCPMessage_IPv4 * ) pucUDPBuffer )->ulDHCPCookie = dhcpCOOKIE;
+    ( ( struct xDHCPMessage_IPv4 * ) pucUDPBuffer )->ucOpcode = dhcpREPLY_OPCODE;
+    ( ( struct xDHCPMessage_IPv4 * ) pucUDPBuffer )->ulTransactionID = FreeRTOS_htonl( 0x01ABCDEF );
+
+    return xSizeRetBufferSize;
+}
+
 static int32_t FreeRTOS_recvfrom_ResetAndIncorrectStateWithSocketAlreadyCreated_validUDPmessage_TwoFlagOptions_nullbytes( const ConstSocket_t xSocket,
                                                                                                                           void * pvBuffer,
                                                                                                                           size_t uxBufferLength,