Fix possible network buffer leak DHCP v4 and v6 state machines

source/FreeRTOS_DHCP.c

@@ -224,6 +224,13 @@
                     {
                         FreeRTOS_printf( ( "vDHCPProcess: FreeRTOS_recvfrom returns %d\n", ( int ) lBytes ) );
                     }
+                    else if( lBytes >= 0 )
+                    {
+                        vReleaseSinglePacketFromUDPSocket( EP_DHCPData.xDHCPSocket );
+                    }
+                    else
+                    {
+                    }
 
                     break;
                 }

source/FreeRTOS_DHCPv6.c

@@ -436,6 +436,13 @@ void vDHCPv6Process( BaseType_t xReset,
                 {
                     FreeRTOS_printf( ( "vDHCPProcess: FreeRTOS_recvfrom returns %d\n", ( int ) lBytes ) );
                 }
+                else if( lBytes == 0 )
+                {
+                    vReleaseSinglePacketFromUDPSocket( EP_DHCPData.xDHCPSocket );
+                }
+                else
+                {
+                }
 
                 break;
             }
@@ -450,6 +457,8 @@ void vDHCPv6Process( BaseType_t xReset,
             {
                 xDoProcess = xDHCPv6Process_PassReplyToEndPoint( pxEndPoint );
             }
+
+            FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload );
         }
     }
 

source/FreeRTOS_IP_Utils.c

@@ -1825,6 +1825,27 @@ uint32_t FreeRTOS_round_down( uint32_t a,
 }
 /*-----------------------------------------------------------*/
 
+/**
+ * @brief Release single UDP packet from a given socket
+ * @param[in] xSocket UDP Socket from which the packet should be released.
+ */
+void vReleaseSinglePacketFromUDPSocket( const ConstSocket_t xSocket )
+{
+    uint8_t * pucUDPPayload = NULL;
+    int32_t lBytes;
+
+    /* Passing the address of a pointer (pucUDPPayload) because FREERTOS_ZERO_COPY is used. */
+    lBytes = FreeRTOS_recvfrom( xSocket, &pucUDPPayload, 0U, FREERTOS_ZERO_COPY, NULL, NULL );
+
+    ( void ) lBytes;
+
+    if( pucUDPPayload != NULL )
+    {
+        FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload );
+    }
+}
+/*-----------------------------------------------------------*/
+
 /**
  * @brief Convert character array (of size 4) to equivalent 32-bit value.
  * @param[in] pucPtr The character array.

source/include/FreeRTOS_IP_Utils.h

@@ -109,6 +109,10 @@ void vPreCheckConfigs( void );
  */
 void prvProcessNetworkDownEvent( struct xNetworkInterface * pxInterface );
 
+/**
+ * @brief Release single UDP packet from a given socket
+ */
+void vReleaseSinglePacketFromUDPSocket( const ConstSocket_t xSocket );
 
 /* *INDENT-OFF* */
 #ifdef __cplusplus

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_utest.c

@@ -16,6 +16,7 @@
 #include "mock_NetworkBufferManagement.h"
 #include "mock_FreeRTOS_DHCP_mock.h"
 #include "mock_FreeRTOS_IP_Common.h"
+#include "mock_FreeRTOS_IP_Utils.h"
 
 #include "FreeRTOS_DHCP.h"
 
@@ -343,6 +344,7 @@ void test_vDHCPProcess_ResetAndIncorrectStateWithSocketAlreadyCreated( void )
         FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
         /* Ignore the buffer argument though. */
         FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+        vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
         /* Make random number generation pass. */
         xApplicationGetRandomNumber_ExpectAndReturn( &( pxEndPoint->xDHCPData.ulTransactionId ), pdTRUE );
         /* See if the timer is reloaded. */
@@ -365,6 +367,76 @@ void test_vDHCPProcess_ResetAndIncorrectStateWithSocketAlreadyCreated( void )
     }
 }
 
+/* Verify the control flow when FreeRTOS_recvfrom with DHCP socket returns timeout. */
+void test_vDHCPProcess_RecvFromReturnsTimeout( void )
+{
+    struct xSOCKET xTestSocket;
+    NetworkEndPoint_t xEndPoint = { 0 }, * pxEndPoint = &xEndPoint;
+
+    /* This should remain unchanged. */
+    xDHCPv4Socket = &xTestSocket;
+    xDHCPSocketUserCount = 1;
+    pxEndPoint->xDHCPData.xDHCPSocket = &xTestSocket;
+    /* Put any state. */
+    pxEndPoint->xDHCPData.eDHCPState = eSendDHCPRequest;
+    pxEndPoint->xDHCPData.eExpectedState = eSendDHCPRequest;
+    /* This should be reset to 0. */
+    pxEndPoint->xDHCPData.xUseBroadcast = 1;
+    /* This should be reset as well */
+    pxEndPoint->xDHCPData.ulOfferedIPAddress = 0xAAAAAAAA;
+    /* And this too. */
+    pxEndPoint->xDHCPData.ulDHCPServerAddress = 0xABABABAB;
+    /* And this should be updated. */
+    pxEndPoint->xDHCPData.xDHCPTxPeriod = 0;
+
+    /* Expect these arguments. */
+    FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, -pdFREERTOS_ERRNO_EAGAIN );
+    /* Ignore the buffer argument though. */
+    FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+
+    /* Make random number generation pass. */
+    xApplicationGetRandomNumber_ExpectAndReturn( &( pxEndPoint->xDHCPData.ulTransactionId ), pdTRUE );
+    /* See if the timer is reloaded. */
+    vDHCP_RATimerReload_Expect( &xEndPoint, dhcpINITIAL_TIMER_PERIOD );
+
+    vDHCPProcess( pdTRUE, pxEndPoint );
+}
+
+/* Verify the control flow when FreeRTOS_recvfrom with DHCP socket returns IO error/any other error. */
+void test_vDHCPProcess_RecvFromReturnsIOError( void )
+{
+    struct xSOCKET xTestSocket;
+    NetworkEndPoint_t xEndPoint = { 0 }, * pxEndPoint = &xEndPoint;
+
+    /* This should remain unchanged. */
+    xDHCPv4Socket = &xTestSocket;
+    xDHCPSocketUserCount = 1;
+    pxEndPoint->xDHCPData.xDHCPSocket = &xTestSocket;
+    /* Put any state. */
+    pxEndPoint->xDHCPData.eDHCPState = eSendDHCPRequest;
+    pxEndPoint->xDHCPData.eExpectedState = eSendDHCPRequest;
+    /* This should be reset to 0. */
+    pxEndPoint->xDHCPData.xUseBroadcast = 1;
+    /* This should be reset as well */
+    pxEndPoint->xDHCPData.ulOfferedIPAddress = 0xAAAAAAAA;
+    /* And this too. */
+    pxEndPoint->xDHCPData.ulDHCPServerAddress = 0xABABABAB;
+    /* And this should be updated. */
+    pxEndPoint->xDHCPData.xDHCPTxPeriod = 0;
+
+    /* Expect these arguments. */
+    FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, -pdFREERTOS_ERRNO_EIO );
+    /* Ignore the buffer argument though. */
+    FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+
+    /* Make random number generation pass. */
+    xApplicationGetRandomNumber_ExpectAndReturn( &( pxEndPoint->xDHCPData.ulTransactionId ), pdTRUE );
+    /* See if the timer is reloaded. */
+    vDHCP_RATimerReload_Expect( &xEndPoint, dhcpINITIAL_TIMER_PERIOD );
+
+    vDHCPProcess( pdTRUE, pxEndPoint );
+}
+
 void test_vDHCPProcess_CorrectStateDHCPHookFailsDHCPSocketNULL( void )
 {
     NetworkEndPoint_t xEndPoint = { 0 }, * pxEndPoint = &xEndPoint;
@@ -422,6 +494,7 @@ void test_vDHCPProcess_CorrectStateDHCPHookFailsDHCPSocketNonNULL( void )
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
     /* Make sure that the user indicates anything else than the desired options. */
     eStubExpectedDHCPPhase = eDHCPPhasePreDiscover;
     pxStubExpectedEndPoint = pxEndPoint;
@@ -469,6 +542,7 @@ void test_vDHCPProcess_CorrectStateDHCPHookDefaultReturn( void )
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
     /* Make sure that the user indicates anything else than the desired options. */
     eStubExpectedDHCPPhase = eDHCPPhasePreDiscover;
     pxStubExpectedEndPoint = pxEndPoint;
@@ -513,6 +587,7 @@ void test_vDHCPProcess_CorrectStateDHCPHookContinueReturnDHCPSocketNotNULLButGNW
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
     /* Make sure that the user indicates anything else than the desired options. */
     eStubExpectedDHCPPhase = eDHCPPhasePreDiscover;
     pxStubExpectedEndPoint = pxEndPoint;
@@ -551,6 +626,7 @@ void test_vDHCPProcess_CorrectStateDHCPHookContinueReturnDHCPSocketNotNULLButHos
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
     /* Make sure that the user indicates anything else than the desired options. */
     eStubExpectedDHCPPhase = eDHCPPhasePreDiscover;
     pxStubExpectedEndPoint = pxEndPoint;
@@ -623,6 +699,7 @@ void test_vDHCPProcess_CorrectStateDHCPHookContinueReturnSendFailsNoBroadcast( v
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
     /* Make sure that the user indicates anything else than the desired options. */
     eStubExpectedDHCPPhase = eDHCPPhasePreDiscover;
     pxStubExpectedEndPoint = pxEndPoint;
@@ -671,6 +748,7 @@ void test_vDHCPProcess_CorrectStateDHCPHookContinueReturnSendFailsNoBroadcast_NU
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
     /* Make sure that the user indicates anything else than the desired options. */
     eStubExpectedDHCPPhase = eDHCPPhasePreDiscover;
     pxStubExpectedEndPoint = pxEndPoint;
@@ -720,6 +798,7 @@ void test_vDHCPProcess_CorrectStateDHCPHookContinueReturnSendFailsUseBroadCast(
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
     /* Make sure that the user indicates anything else than the desired options. */
     eStubExpectedDHCPPhase = eDHCPPhasePreDiscover;
     pxStubExpectedEndPoint = pxEndPoint;
@@ -770,6 +849,7 @@ void test_vDHCPProcess_CorrectStateDHCPHookContinueReturnSendSucceedsUseBroadCas
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
     /* Make sure that the user indicates anything else than the desired options. */
     eStubExpectedDHCPPhase = eDHCPPhasePreDiscover;
     pxStubExpectedEndPoint = pxEndPoint;
@@ -821,6 +901,7 @@ void test_vDHCPProcess_CorrectStateDHCPHookContinueReturnSendSucceedsUseBroadCas
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
     /* Make sure that the user indicates anything else than the desired options. */
     eStubExpectedDHCPPhase = eDHCPPhasePreDiscover;
     pxStubExpectedEndPoint = pxEndPoint;
@@ -868,6 +949,7 @@ void test_vDHCPProcess_eSendDHCPRequestCorrectStateGNWFails( void )
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
     /* Get the hostname. */
     pcApplicationHostnameHook_ExpectAndReturn( pcHostName );
     /* Return NULL network buffer. */
@@ -900,6 +982,7 @@ void test_vDHCPProcess_eSendDHCPRequestCorrectStateGNWSucceedsSendFails( void )
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
     /* Get the hostname. */
     pcApplicationHostnameHook_ExpectAndReturn( pcHostName );
     /* Returning a proper network buffer. */
@@ -938,6 +1021,7 @@ void test_vDHCPProcess_eSendDHCPRequestCorrectStateGNWSucceedsSendSucceeds( void
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
     /* Get the hostname. */
     pcApplicationHostnameHook_ExpectAndReturn( pcHostName );
     /* Returning a proper network buffer. */
@@ -980,6 +1064,7 @@ void test_vDHCPProcess_eWaitingOfferRecvfromFailsNoTimeout( void )
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
 
     /* Make sure that there is no timeout. The expression is: xTaskGetTickCount() - pxEndPoint->xDHCPData.xDHCPTxTime ) > pxEndPoint->xDHCPData.xDHCPTxPeriod  */
     /* Return a value which makes the difference just equal to the period. */
@@ -1016,6 +1101,7 @@ void test_vDHCPProcess_eWaitingOfferRecvfromFailsTimeoutGiveUp( void ) /* prvClo
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
 
     /* Make sure that there is timeout. The expression is: xTaskGetTickCount() - pxEndPoint->xDHCPData.xDHCPTxTime ) > pxEndPoint->xDHCPData.xDHCPTxPeriod  */
     /* Return a value which makes the difference greater than the period. */
@@ -1068,6 +1154,7 @@ void test_vDHCPProcess_eWaitingOfferRecvfromFailsTimeoutDontGiveUpRNGFail( void
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
 
     /* Make sure that there is timeout. The expression is: xTaskGetTickCount() - pxEndPoint->xDHCPData.xDHCPTxTime ) > pxEndPoint->xDHCPData.xDHCPTxPeriod  */
     /* Return a value which makes the difference greater than the period. */
@@ -1111,6 +1198,7 @@ void test_vDHCPProcess_eWaitingOfferRecvfromFailsTimeoutDontGiveUpRNGPassUseBroa
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
 
     /* Make sure that there is timeout. The expression is: xTaskGetTickCount() - pxEndPoint->xDHCPData.xDHCPTxTime ) > pxEndPoint->xDHCPData.xDHCPTxPeriod  */
     /* Return a value which makes the difference greater than the period. */
@@ -1164,6 +1252,7 @@ void test_vDHCPProcess_eWaitingOfferRecvfromFailsTimeoutDontGiveUpRNGPassNoBroad
     FreeRTOS_recvfrom_ExpectAndReturn( xDHCPv4Socket, NULL, 0UL, FREERTOS_ZERO_COPY + FREERTOS_MSG_PEEK, NULL, NULL, 0 );
     /* Ignore the buffer argument though. */
     FreeRTOS_recvfrom_IgnoreArg_pvBuffer();
+    vReleaseSinglePacketFromUDPSocket_Expect( xDHCPv4Socket );
 
     /* Make sure that there is timeout. The expression is: xTaskGetTickCount() - pxEndPoint->xDHCPData.xDHCPTxTime ) > pxEndPoint->xDHCPData.xDHCPTxPeriod  */
     /* Return a value which makes the difference greater than the period. */

test/unit-test/FreeRTOS_DHCP/ut.cmake

@@ -17,6 +17,7 @@ list(APPEND mock_list
             "${CMAKE_BINARY_DIR}/Annexed_TCP/FreeRTOS_Routing.h"
             "${CMAKE_BINARY_DIR}/Annexed_TCP/FreeRTOS_IP_Private.h"
             "${CMAKE_BINARY_DIR}/Annexed_TCP/FreeRTOS_IP_Common.h"
+            "${CMAKE_BINARY_DIR}/Annexed_TCP/FreeRTOS_IP_Utils.h"
             "${CMAKE_BINARY_DIR}/Annexed_TCP/FreeRTOS_IP_Timers.h"
             "${CMAKE_BINARY_DIR}/Annexed_TCP/NetworkBufferManagement.h"
             "${MODULE_ROOT_DIR}/test/unit-test/${project_name}/FreeRTOS_DHCP_mock.h"