Adjust proof tooling to support CBMC v6

.github/workflows/ci.yml

@@ -406,7 +406,7 @@ jobs:
       - name: Set up CBMC runner
         uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main
         with:
-          cbmc_version: "5.95.1"
+          cbmc_version: "6.1.1"
 
       - env:
           stepName: Install Dependencies

source/FreeRTOS_DHCP.c

@@ -81,7 +81,7 @@
 /**
  * @brief The number of end-points that are making use of the UDP-socket.
  */
-    static BaseType_t xDHCPSocketUserCount = 0;
+    _static BaseType_t xDHCPSocketUserCount = 0;
 
 /*
  * Generate a DHCP discover message and send it on the DHCP socket.
@@ -881,7 +881,7 @@
             configASSERT( xSocketValid( xDHCPv4Socket ) == pdTRUE );
 
             /* MISRA Ref 11.4.1 [Socket error and integer to pointer conversion] */
-/* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-114 */
+            /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-114 */
             /* coverity[misra_c_2012_rule_11_4_violation] */
             if( xSocketValid( xDHCPv4Socket ) == pdTRUE )
             {

source/FreeRTOS_DHCPv6.c

@@ -85,11 +85,11 @@
       ( ( ( uint32_t ) 1U ) << DHCPv6_Option_Server_Identifier ) )
 
 /** @brief The UDP socket which is shared by all end-points that need DHCPv6. */
-static Socket_t xDHCPv6Socket;
+_static Socket_t xDHCPv6Socket;
 
 /** @brief A reference count makes sure that the UDP socket will be deleted when it
  * is not used anymore. */
-static BaseType_t xDHCPv6SocketUserCount;
+_static BaseType_t xDHCPv6SocketUserCount;
 
 static BaseType_t prvIsOptionLengthValid( uint16_t usOption,
                                           size_t uxOptionLength,
@@ -151,7 +151,7 @@ static BaseType_t prvDHCPv6_handleOption( struct xNetworkEndPoint * pxEndPoint,
 /**
  * @brief DHCP IPv6 message object
  */
-static DHCPMessage_IPv6_t xDHCPMessage;
+_static DHCPMessage_IPv6_t xDHCPMessage;
 
 /**
  * @brief Get the DHCP state from a given endpoint.
@@ -1492,6 +1492,7 @@ static BaseType_t prvDHCPv6Analyse( struct xNetworkEndPoint * pxEndPoint,
             xSet.uxOptionLength = ( size_t ) usBitConfig_read_16( &xMessage );
             xSet.uxStart = xMessage.uxIndex;
 
+            /* ulOptionsReceived has only 32-bits, it's not allowed to shift more than 32-bits on it. */
             if( xMessage.xHasError != pdFALSE )
             {
                 FreeRTOS_printf( ( "prvDHCPv6Analyse: bad input\n" ) );
@@ -1500,7 +1501,12 @@ static BaseType_t prvDHCPv6Analyse( struct xNetworkEndPoint * pxEndPoint,
             }
             else
             {
-                ulOptionsReceived |= ( ( ( uint32_t ) 1U ) << usOption );
+                if( usOption < 32 )
+                {
+                    /* Store the option by bit-map only if it's less than 32. */
+                    ulOptionsReceived |= ( ( ( uint32_t ) 1U ) << usOption );
+                }
+
                 xReady = prvDHCPv6_handleOption( pxEndPoint, usOption, &( xSet ), pxDHCPMessage, &( xMessage ) );
             }
 

source/FreeRTOS_DNS_Parser.c

@@ -1093,7 +1093,7 @@
                     /* Define the ASCII value of the capital "A". */
                     const uint8_t ucCharA = ( uint8_t ) 0x41U;
 
-                    ucByte = ( uint8_t ) ( ( ( pucSource[ 0 ] - ucCharA ) << 4 ) |
+                    ucByte = ( uint8_t ) ( ( ( ( pucSource[ 0 ] - ucCharA ) & 0x0F ) << 4 ) |
                                            ( pucSource[ 1 ] - ucCharA ) );
 
                     /* Make sure there are no trailing spaces in the name. */

source/FreeRTOS_IP_Utils.c

@@ -1694,6 +1694,81 @@ size_t FreeRTOS_min_size_t( size_t a,
 }
 /*-----------------------------------------------------------*/
 
+/**
+ * @brief Performs a safe addition of two 32-bit integers, preventing overflow and underflow.
+ * @param[in] a the first value.
+ * @param[in] b the second value.
+ * @return The result of a + b if no overflow/underflow occurs, or INT32_MAX/INT32_MIN if overflow/underflow would occur.
+ */
+int32_t FreeRTOS_add_int32( int32_t a,
+                            int32_t b )
+{
+    int32_t ret;
+
+    if( ( a > 0 ) && ( b > ipINT32_MAX_VALUE - a ) )
+    {
+        ret = ipINT32_MAX_VALUE; /* Positive overflow */
+    }
+    else if( ( a < 0 ) && ( b < ipINT32_MIN_VALUE - a ) )
+    {
+        ret = ipINT32_MIN_VALUE; /* Negative underflow */
+    }
+    else
+    {
+        ret = a + b;
+    }
+
+    return ret;
+}
+/*-----------------------------------------------------------*/
+
+/**
+ * @brief Performs a safe multiplication of two 32-bit integers, preventing overflow and underflow.
+ * @param[in] a the first value.
+ * @param[in] b the second value.
+ * @return The result of a * b if no overflow occurs, or ipINT32_MAX_VALUE if an overflow would occur.
+ */
+int32_t FreeRTOS_multiply_int32( int32_t a,
+                                 int32_t b )
+{
+    int32_t ret;
+
+    /* Check for overflow/underflow */
+    if( a > 0 )
+    {
+        if( ( b > 0 ) && ( a > ipINT32_MAX_VALUE / b ) )
+        {
+            ret = ipINT32_MAX_VALUE; /* Positive overflow */
+        }
+        else if( ( b < 0 ) && ( b < ipINT32_MIN_VALUE / a ) )
+        {
+            ret = ipINT32_MIN_VALUE; /* Negative underflow */
+        }
+        else
+        {
+            ret = a * b;
+        }
+    }
+    else
+    {
+        if( ( b > 0 ) && ( a < ipINT32_MIN_VALUE / b ) )
+        {
+            ret = ipINT32_MIN_VALUE; /* Negative underflow */
+        }
+        else if( ( b < 0 ) && ( a < ipINT32_MAX_VALUE / b ) )
+        {
+            ret = ipINT32_MAX_VALUE; /* Positive overflow */
+        }
+        else
+        {
+            ret = a * b;
+        }
+    }
+
+    return ret;
+}
+/*-----------------------------------------------------------*/
+
 /**
  * @brief Round-up a number to a multiple of 'd'.
  * @param[in] a the first value.

source/FreeRTOS_TCP_Reception.c

@@ -99,7 +99,7 @@
         size_t uxTCPHeaderOffset = ipSIZE_OF_ETH_HEADER + uxIPHeaderSizePacket( pxNetworkBuffer );
 
         /* MISRA Ref 11.3.1 [Misaligned access] */
-/* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
+        /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
         /* coverity[misra_c_2012_rule_11_3_violation] */
         const ProtocolHeaders_t * pxProtocolHeaders = ( ( ProtocolHeaders_t * )
                                                         &( pxNetworkBuffer->pucEthernetBuffer[ uxTCPHeaderOffset ] ) );
@@ -237,7 +237,17 @@
                     /* Option is only valid in SYN phase. */
                     if( xHasSYNFlag != 0 )
                     {
-                        pxSocket->u.xTCP.ucPeerWinScaleFactor = pucPtr[ 2 ];
+                        /* From RFC7323 - section 2.3, we should limit the WSopt not larger than 14. */
+                        if( pucPtr[ 2 ] > tcpTCP_OPT_WSOPT_MAXIMUM_VALUE )
+                        {
+                            FreeRTOS_debug_printf( ( "The WSopt(%u) from SYN packet is larger than maximum value.", pucPtr[ 2 ] ) );
+                            pxSocket->u.xTCP.ucPeerWinScaleFactor = tcpTCP_OPT_WSOPT_MAXIMUM_VALUE;
+                        }
+                        else
+                        {
+                            pxSocket->u.xTCP.ucPeerWinScaleFactor = pucPtr[ 2 ];
+                        }
+
                         pxSocket->u.xTCP.bits.bWinScaling = pdTRUE_UNSIGNED;
                     }
 
@@ -430,7 +440,7 @@
         /* Map the ethernet buffer onto the ProtocolHeader_t struct for easy access to the fields. */
 
         /* MISRA Ref 11.3.1 [Misaligned access] */
-/* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
+        /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
         /* coverity[misra_c_2012_rule_11_3_violation] */
         const ProtocolHeaders_t * pxProtocolHeaders = ( ( ProtocolHeaders_t * )
                                                         &( pxNetworkBuffer->pucEthernetBuffer[ ( size_t ) ipSIZE_OF_ETH_HEADER + uxIPHeaderSizePacket( pxNetworkBuffer ) ] ) );

source/FreeRTOS_TCP_WIN.c

@@ -1901,18 +1901,33 @@
                                                      const TCPSegment_t * pxSegment )
         {
             int32_t mS = ( int32_t ) ulTimerGetAge( &( pxSegment->xTransmitTimer ) );
+            int32_t lSum = 0;
+            int32_t lWeight = 0;
+            int32_t lDivisor = 0;
+
+            mS = mS < 0 ? ipINT32_MAX_VALUE : mS;
 
             if( pxWindow->lSRTT >= mS )
             {
                 /* RTT becomes smaller: adapt slowly. */
-                pxWindow->lSRTT = ( ( winSRTT_DECREMENT_NEW * mS ) + ( winSRTT_DECREMENT_CURRENT * pxWindow->lSRTT ) ) / ( winSRTT_DECREMENT_NEW + winSRTT_DECREMENT_CURRENT );
+                lWeight = winSRTT_DECREMENT_CURRENT;
+                lDivisor = winSRTT_DECREMENT_NEW + winSRTT_DECREMENT_CURRENT;
+                mS = FreeRTOS_multiply_int32( mS,
+                                              winSRTT_DECREMENT_NEW );
             }
             else
             {
                 /* RTT becomes larger: adapt quicker */
-                pxWindow->lSRTT = ( ( winSRTT_INCREMENT_NEW * mS ) + ( winSRTT_INCREMENT_CURRENT * pxWindow->lSRTT ) ) / ( winSRTT_INCREMENT_NEW + winSRTT_INCREMENT_CURRENT );
+                lWeight = winSRTT_INCREMENT_CURRENT;
+                lDivisor = winSRTT_INCREMENT_NEW + winSRTT_INCREMENT_CURRENT;
+                mS = FreeRTOS_multiply_int32( mS,
+                                              winSRTT_INCREMENT_NEW );
             }
 
+            lSum = FreeRTOS_multiply_int32( pxWindow->lSRTT, lWeight );
+            lSum = FreeRTOS_add_int32( lSum, mS );
+            pxWindow->lSRTT = lSum / lDivisor;
+
             /* Cap to the minimum of 50ms. */
             if( pxWindow->lSRTT < winSRTT_CAP_mS )
             {
@@ -1946,7 +1961,7 @@
             const ListItem_t * pxIterator;
 
             /* MISRA Ref 11.3.1 [Misaligned access] */
-/* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
+            /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
             /* coverity[misra_c_2012_rule_11_3_violation] */
             const ListItem_t * pxEnd = ( ( const ListItem_t * ) &( pxWindow->xTxSegments.xListEnd ) );
             BaseType_t xDoUnlink;

source/include/FreeRTOS_IP.h

@@ -60,6 +60,11 @@
 #define ipSIZE_OF_UDP_HEADER     8U
 #define ipSIZE_OF_TCP_HEADER     20U
 
+/* The maximum of int32 value. */
+#define ipINT32_MAX_VALUE        ( ( int32_t ) 0x7FFFFFFF )
+
+/* The minimum of int32 value. */
+#define ipINT32_MIN_VALUE        ( ( int32_t ) 0x80000000 )
 
 /*
  * Generate a randomized TCP Initial Sequence Number per RFC.
@@ -270,6 +275,11 @@ uint32_t FreeRTOS_min_uint32( uint32_t a,
 size_t FreeRTOS_min_size_t( size_t a,
                             size_t b );
 
+int32_t FreeRTOS_add_int32( int32_t a,
+                            int32_t b );
+int32_t FreeRTOS_multiply_int32( int32_t a,
+                                 int32_t b );
+
 uint32_t FreeRTOS_round_up( uint32_t a,
                             uint32_t d );
 uint32_t FreeRTOS_round_down( uint32_t a,

source/include/FreeRTOS_TCP_IP.h

@@ -96,25 +96,26 @@ typedef enum eTCP_STATE
 /*
  * A few values of the TCP options:
  */
-#define tcpTCP_OPT_END               0U                  /**< End of TCP options list. */
-#define tcpTCP_OPT_NOOP              1U                  /**< "No-operation" TCP option. */
-#define tcpTCP_OPT_MSS               2U                  /**< Maximum segment size TCP option. */
-#define tcpTCP_OPT_WSOPT             3U                  /**< TCP Window Scale Option (3-byte long). */
-#define tcpTCP_OPT_SACK_P            4U                  /**< Advertise that SACK is permitted. */
-#define tcpTCP_OPT_SACK_A            5U                  /**< SACK option with first/last. */
-#define tcpTCP_OPT_TIMESTAMP         8U                  /**< Time-stamp option. */
+#define tcpTCP_OPT_END                    0U             /**< End of TCP options list. */
+#define tcpTCP_OPT_NOOP                   1U             /**< "No-operation" TCP option. */
+#define tcpTCP_OPT_MSS                    2U             /**< Maximum segment size TCP option. */
+#define tcpTCP_OPT_WSOPT                  3U             /**< TCP Window Scale Option (3-byte long). */
+#define tcpTCP_OPT_SACK_P                 4U             /**< Advertise that SACK is permitted. */
+#define tcpTCP_OPT_SACK_A                 5U             /**< SACK option with first/last. */
+#define tcpTCP_OPT_TIMESTAMP              8U             /**< Time-stamp option. */
 
 
-#define tcpTCP_OPT_MSS_LEN           4U                  /**< Length of TCP MSS option. */
-#define tcpTCP_OPT_WSOPT_LEN         3U                  /**< Length of TCP WSOPT option. */
+#define tcpTCP_OPT_MSS_LEN                4U             /**< Length of TCP MSS option. */
+#define tcpTCP_OPT_WSOPT_LEN              3U             /**< Length of TCP WSOPT option. */
+#define tcpTCP_OPT_WSOPT_MAXIMUM_VALUE    ( 14U )        /**< Maximum value of TCP WSOPT option. */
 
-#define tcpTCP_OPT_TIMESTAMP_LEN     10                  /**< fixed length of the time-stamp option. */
+#define tcpTCP_OPT_TIMESTAMP_LEN          10             /**< fixed length of the time-stamp option. */
 
 /** @brief
  * Minimum segment length as outlined by RFC 791 section 3.1.
  * Minimum segment length ( 536 ) = Minimum MTU ( 576 ) - IP Header ( 20 ) - TCP Header ( 20 ).
  */
-#define tcpMINIMUM_SEGMENT_LENGTH    536U
+#define tcpMINIMUM_SEGMENT_LENGTH         536U
 
 /** @brief
  * The macro tcpNOW_CONNECTED() is use to determine if the connection makes a

test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c

@@ -12,6 +12,7 @@ void harness()
 {
     uint32_t ulIPAddress;
     MACAddress_t xMACAddress;
+    struct xNetworkEndPoint * pxEndPoint = NULL;
 
     /*
      * For this proof, its assumed that the endpoints and interfaces are correctly
@@ -38,13 +39,5 @@ void harness()
         pxNetworkEndPoints->pxNext = NULL;
     }
 
-    NetworkInterface_t ** ppxInterface = ( NetworkInterface_t ** ) malloc( sizeof( NetworkInterface_t * ) );
-
-    if( ppxInterface )
-    {
-        *ppxInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
-        __CPROVER_assume( *ppxInterface != NULL );
-    }
-
-    eARPGetCacheEntry( &ulIPAddress, &xMACAddress, ppxInterface );
+    eARPGetCacheEntry( &ulIPAddress, &xMACAddress, &pxEndPoint );
 }

test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c

@@ -100,6 +100,7 @@ void harness()
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
     pxNetworkEndPoints->pxNetworkInterface->pxNext = NULL;
 
     pxNetworkEndPoints->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub;

test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c

@@ -80,6 +80,7 @@ void harness()
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
     pxNetworkEndPoints->pxNetworkInterface->pxNext = NULL;
 
     pxNetworkEndPoints->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub;

test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c

@@ -32,8 +32,6 @@ void __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvReadSackOption( const uint
 * Proof of prvReadSackOption function contract
 ****************************************************************/
 
-
-
 void harness()
 {
     /* pucPtr points into a buffer */
@@ -97,6 +95,8 @@ void harness()
     /* Assuming quite a bit more about the initialization of pxSocket */
     __CPROVER_assume( pucPtr != NULL );
     __CPROVER_assume( pxSocket != NULL );
+    /* lSRTT is guaranteed to be always greater than or equal to minimum value. */
+    __CPROVER_assume( pxSocket->u.xTCP.xTCPWindow.lSRTT >= ipconfigTCP_SRTT_MINIMUM_VALUE_MS );
 
     __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvReadSackOption( pucPtr, uxIndex, pxSocket );
 

test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c

@@ -49,6 +49,7 @@
 /* Static members defined in FreeRTOS_DHCP.c */
 extern DHCPData_t xDHCPData;
 extern Socket_t xDHCPv4Socket;
+extern BaseType_t xDHCPSocketUserCount;
 void prvCreateDHCPSocket( NetworkEndPoint_t * pxEndPoint );
 
 uint32_t uxSocketCloseCnt = 0;
@@ -182,6 +183,9 @@ void harness()
     BaseType_t xReset;
     eDHCPState_t eExpectedState;
 
+    /* The only possibility of making xDHCPSocketUserCount overflow is having more than BaseType_t endpoints, which is assumed not possible here. */
+    __CPROVER_assume( xDHCPSocketUserCount >= 0 && xDHCPSocketUserCount <= ENDPOINT_DNS_ADDRESS_COUNT );
+
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
 

test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json

@@ -33,6 +33,7 @@
     "BUFFER_SIZE={BUFFER_SIZE}",
     "ipconfigDHCP_REGISTER_HOSTNAME=1",
     "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL=1",
-    "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}"
+    "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}",
+    "ENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}"
   ]
 }