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

* [Draft] CBMC: replace any missing functions by assert-false (#1147)

* CBMC: replace any missing functions by assert-false

---------

Co-authored-by: ActoryOu <[email protected]>

* Adjust proof tooling to support CBMC v6 (#1180)

* Adjust proof tooling to support CBMC v6

With CBMC v6, unwinding assertions as well as other checks are enabled
by default.

* Fix CBMC issues

* Fix spelling & formatting

* Fix build-check

* Add unit test cases for FreeRTOS_multiply_int32 and FreeRTOS_add_int32

* Tony's comment

* Bump CBMC version to very latest release

* Replace Synopsys link with blackduck one to solve link error.

* Move the comment to the right place

---------

Co-authored-by: Tony Josi <[email protected]>
Co-authored-by: ActoryOu <[email protected]>
Co-authored-by: ActoryOu <[email protected]>

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

* Fix CI

* Add Network Down event in EMACHandler Task (#1173)

* Add Network Down event in EMACHandler Task

* Update links in ReadMe (#1174)

---------

Co-authored-by: Michael Tautschnig <[email protected]>
Co-authored-by: ActoryOu <[email protected]>
Co-authored-by: ActoryOu <[email protected]>
Co-authored-by: Rahul Kar <[email protected]>

Author: 4 people

.github/.cSpellWords.txt

@@ -89,6 +89,7 @@ BLXNS
 bmcr
 BMSR
 BPDG
+BPIALL
 brgintclr
 brginten
 brgintstat
@@ -920,6 +921,7 @@ Picovolts
 PIDEVAD
 pidr
 PIDR
+PINSEL
 PIOA
 PKHBT
 pkhtb
@@ -1263,6 +1265,7 @@ STLIDMPUSR
 STLIMPUOR
 STLNVICACTVOR
 STLNVICPENDOR
+Storex
 strbt
 STRBT
 strexb

.github/workflows/ci.yml

@@ -128,7 +128,7 @@ jobs:
           path: ./
 
   formatting:
-    runs-on: ubuntu-20.04
+    runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
       - name: Check formatting
@@ -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.3.1"
 
       - env:
           stepName: Install Dependencies

README.md

@@ -5,12 +5,12 @@ This library has undergone static code analysis and checks for compliance with t
 
 ## Getting started
 The easiest way to use version 4.0.0 and later of FreeRTOS-Plus-TCP is to refer the Getting started Guide (found [here](https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/GettingStarted.md))
-Another way is to start with the pre-configured IPv4 Windows Simulator demo (found in [this directory](https://github.com/FreeRTOS/FreeRTOS/tree/main/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Minimal_Windows_Simulator)) or IPv6 Multi-endpoint Windows Simulator demo (found in [this directory](https://github.com/FreeRTOS/FreeRTOS/tree/main/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_IPv6_Demo/IPv6_Multi_WinSim_demo)). That way you will have the correct FreeRTOS source files included, and the correct include paths configured.  Once a demo application is building and executing you can remove the demo application files, and start to add in your own application source files.  See the [FreeRTOS Kernel Quick Start Guide](https://www.freertos.org/FreeRTOS-quick-start-guide.html) for detailed instructions and other useful links.
+Another way is to start with the pre-configured IPv4 Windows Simulator demo (found in [this directory](https://github.com/FreeRTOS/FreeRTOS/tree/main/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Minimal_Windows_Simulator)) or IPv6 Multi-endpoint Windows Simulator demo (found in [this directory](https://github.com/FreeRTOS/FreeRTOS/tree/main/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_IPv6_Demo/IPv6_Multi_WinSim_demo)). That way you will have the correct FreeRTOS source files included, and the correct include paths configured.  Once a demo application is building and executing you can remove the demo application files, and start to add in your own application source files.  See the [FreeRTOS Kernel Quick Start Guide](https://www.freertos.org/Documentation/01-FreeRTOS-quick-start/01-Beginners-guide/02-Quick-start-guide) for detailed instructions and other useful links.
 
-Additionally, for FreeRTOS-Plus-TCP source code organization refer to the [Documentation](http://www.FreeRTOS.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_Networking_Tutorial.html), and [API Reference](https://freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/FreeRTOS_TCP_API_Functions.html).
+Additionally, for FreeRTOS-Plus-TCP source code organization refer to the [Documentation](http://www.FreeRTOS.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_Networking_Tutorial.html), and [API Reference](https://freertos.org/Documentation/03-Libraries/02-FreeRTOS-plus/02-FreeRTOS-plus-TCP/09-API-reference/01-FreeRTOS-plus-TCP-APIs).
 
 ### Getting help
-If you have any questions or need assistance troubleshooting your FreeRTOS project, we have an active community that can help on the [FreeRTOS Community Support Forum](https://forums.freertos.org). Please also refer to [FAQ](http://www.freertos.org/FAQHelp.html) for frequently asked questions.
+If you have any questions or need assistance troubleshooting your FreeRTOS project, we have an active community that can help on the [FreeRTOS Community Support Forum](https://forums.freertos.org). Please also refer to [FAQ](https://www.freertos.org/Why-FreeRTOS/FAQs) for frequently asked questions.
 
 Also see the [Submitting a bugs/feature request](https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/.github/CONTRIBUTING.md#submitting-a-bugsfeature-request) section of CONTRIBUTING.md for more details.
 
@@ -86,7 +86,7 @@ git submodule update --checkout --init --recursive tools/CMock test/FreeRTOS-Ker
 ```
 
 ## Porting
-The porting guide is available on [this page](http://www.FreeRTOS.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/FreeRTOS_TCP_Porting.html).
+The porting guide is available on [this page](https://www.freertos.org/Documentation/03-Libraries/02-FreeRTOS-plus/02-FreeRTOS-plus-TCP/10-Porting/01-FreeRTOS_TCP_Porting).
 
 ## Repository structure
 This repository contains the FreeRTOS-Plus-TCP repository and a number of supplementary libraries for testing/PR Checks.

readme.txt

@@ -7,7 +7,7 @@ A description of the source code organisation is available on:
 http://www.FreeRTOS.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_Networking_Tutorial.html
 
 The porting guide is available on:
-http://www.FreeRTOS.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/FreeRTOS_TCP_Porting.html
+https://www.freertos.org/Documentation/03-Libraries/02-FreeRTOS-plus/02-FreeRTOS-plus-TCP/10-Porting/01-FreeRTOS_TCP_Porting
 
 License information is available on:
 http://www.FreeRTOS.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/FreeRTOS_Plus_TCP_License.html

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.
@@ -1500,7 +1500,13 @@ static BaseType_t prvDHCPv6Analyse( struct xNetworkEndPoint * pxEndPoint,
             }
             else
             {
-                ulOptionsReceived |= ( ( ( uint32_t ) 1U ) << usOption );
+                /* ulOptionsReceived has only 32-bits, it's not allowed to shift more than 32-bits on it. */
+                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_Cache.c

@@ -448,10 +448,9 @@
         /* Add or update the item. */
         if( strlen( pcName ) < ( size_t ) ipconfigDNS_CACHE_NAME_LENGTH )
         {
-            ( void ) strncpy( xDNSCache[ uxFreeEntry ].pcName, pcName, ipconfigDNS_CACHE_NAME_LENGTH );
+            ( void ) strncpy( xDNSCache[ uxFreeEntry ].pcName, pcName, strlen( pcName ) );
             ( void ) memcpy( &( xDNSCache[ uxFreeEntry ].xAddresses[ 0 ] ), pxIP, sizeof( *pxIP ) );
 
-
             xDNSCache[ uxFreeEntry ].ulTTL = ulTTL;
             xDNSCache[ uxFreeEntry ].ulTimeWhenAddedInSeconds = ulCurrentTimeSeconds;
             #if ( ipconfigDNS_CACHE_ADDRESSES_PER_ENTRY > 1 )

source/FreeRTOS_DNS_Parser.c

@@ -484,31 +484,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,
@@ -537,7 +536,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 ) )
@@ -1093,7 +1102,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. */
@@ -1208,7 +1217,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/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 ) ] ) );