Fix integer wrap around when IPv6 payload length is malformed

Author: tony-josi-aws

source/FreeRTOS_IPv6_Utils.c

@@ -92,7 +92,7 @@ BaseType_t prvChecksumIPv6Checks( uint8_t * pucEthernetBuffer,
     {
         uxExtensionHeaderLength = usGetExtensionHeaderLength( pucEthernetBuffer, uxBufferLength, &pxSet->ucProtocol );
 
-        if( uxExtensionHeaderLength >= uxBufferLength )
+        if( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + uxExtensionHeaderLength >= uxBufferLength )
         {
             /* Error detected when parsing extension header. */
             pxSet->usChecksum = ipINVALID_LENGTH;
@@ -108,7 +108,16 @@ BaseType_t prvChecksumIPv6Checks( uint8_t * pucEthernetBuffer,
             pxSet->pxProtocolHeaders = ( ( ProtocolHeaders_t * ) &( pucEthernetBuffer[ ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + uxExtensionHeaderLength ] ) );
             pxSet->usPayloadLength = FreeRTOS_ntohs( pxSet->pxIPPacket_IPv6->usPayloadLength );
             /* For IPv6, the number of bytes in the protocol is indicated. */
-            pxSet->usProtocolBytes = ( uint16_t ) ( pxSet->usPayloadLength - uxExtensionHeaderLength );
+            if( pxSet->usPayloadLength < uxExtensionHeaderLength )
+            {
+                /* Invalid payload length - extension headers exceed payload. */
+                pxSet->usChecksum = ipINVALID_LENGTH;
+                xReturn = 4;
+            }
+            else
+            {
+                pxSet->usProtocolBytes = ( uint16_t ) ( pxSet->usPayloadLength - uxExtensionHeaderLength );
+            }
 
             uxNeeded = ( size_t ) pxSet->usPayloadLength;
             uxNeeded += ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER;

test/cbmc/proofs/prvChecksumIPv6Checks/prvChecksumIPv6Checks_harness.c

@@ -21,19 +21,27 @@ void harness()
     size_t uxBufferSize;
     uint8_t * pucEthernetBuffer;
     struct xPacketSummary xSet;
+    BaseType_t xReturn;
 
     /* We must have ethernet header to get frame type. */
     __CPROVER_assume( uxBufferSize >= sizeof( IPPacket_IPv6_t ) && uxBufferSize <= ipconfigNETWORK_MTU );
 
     /* Ethernet buffer is not possible to be NULL. */
     pucEthernetBuffer = ( uint8_t * ) safeMalloc( uxBufferSize );
     __CPROVER_assume( pucEthernetBuffer != NULL );
+    __CPROVER_havoc_object( pucEthernetBuffer );
 
     /* This is set before calling prvChecksumIPv6Checks. */
     xSet.pxIPPacket = ( const IPPacket_t * ) pucEthernetBuffer;
     xSet.pxIPPacket_IPv6 = ( const IPHeader_IPv6_t * ) ( pucEthernetBuffer + ipSIZE_OF_ETH_HEADER );
 
-    prvChecksumIPv6Checks( pucEthernetBuffer,
+    xReturn = prvChecksumIPv6Checks( pucEthernetBuffer,
                            uxBufferSize,
                            &xSet );
+
+    if( xReturn == 0 )
+    {
+        __CPROVER_assert( ( xSet.usProtocolBytes <= FreeRTOS_ntohs( xSet.pxIPPacket_IPv6->usPayloadLength ) ), "xSet.usProtocolBytes shouldn't be greater than IPv6 usPayloadLength" );
+    }
+
 }

test/unit-test/FreeRTOS_IPv6_Utils/FreeRTOS_IPv6_Utils_utest.c

@@ -131,7 +131,7 @@ void test_prvChecksumIPv6Checks_IncompleteIPv6Packet( void )
     BaseType_t usReturn;
     uint8_t pucEthernetBuffer[ ipconfigTCPv6_MSS ];
     IPHeader_IPv6_t * pxIPv6Packet;
-    size_t uxBufferLength = ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER;
+    size_t uxBufferLength = ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + 4;
     struct xPacketSummary xSet;
 
     memset( pucEthernetBuffer, 0, ipconfigTCPv6_MSS );
@@ -205,6 +205,46 @@ void test_prvChecksumIPv6Checks_LargeExtensionHeader( void )
     TEST_ASSERT_EQUAL( 3, usReturn );
 }
 
+/**
+ * @brief Prepare a packet with large extension header length.
+ *         - ipIPv6_EXT_HEADER_ROUTING_HEADER
+ *         - ipIPv6_EXT_HEADER_HOP_BY_HOP
+ *         - ipPROTOCOL_TCP
+ */
+void test_prvChecksumIPv6Checks_IncorrectPayloadLength( void )
+{
+    BaseType_t usReturn;
+    struct xPacketSummary xSet;
+    NetworkBufferDescriptor_t * pxNetworkBuffer = prvInitializeNetworkDescriptorWithExtensionHeader( ipPROTOCOL_TCP );
+    IPHeader_IPv6_t * pxIPv6Header = ( IPHeader_IPv6_t * ) &( pxNetworkBuffer->pucEthernetBuffer[ ipSIZE_OF_ETH_HEADER ] );
+    size_t uxIndex = ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER;
+
+    /* Modify the extension header */
+    pxIPv6Header->ucNextHeader = ipIPv6_EXT_HEADER_HOP_BY_HOP;
+    pxNetworkBuffer->pucEthernetBuffer[ uxIndex ] = ipIPv6_EXT_HEADER_ROUTING_HEADER;
+    pxNetworkBuffer->pucEthernetBuffer[ uxIndex + 1 ] = 5U; /* Extension header length is set to 200*8 + 8, which is larger than buffer size. */
+    uxIndex += 8;
+    pxNetworkBuffer->pucEthernetBuffer[ uxIndex ] = ipPROTOCOL_TCP;
+    pxNetworkBuffer->pucEthernetBuffer[ uxIndex + 1 ] = 0;
+    uxIndex += 8;
+
+    xSet.pxIPPacket_IPv6 = ( ( const IPHeader_IPv6_t * ) pxNetworkBuffer->pucEthernetBuffer );
+    IPHeader_IPv6_t * pxIPPacket_IPv6 = (IPHeader_IPv6_t * ) pxNetworkBuffer->pucEthernetBuffer;
+
+    /* Incorrect payload length */
+    pxIPPacket_IPv6->usPayloadLength = FreeRTOS_ntohs(20);
+
+    xGetExtensionOrder_ExpectAndReturn( ipIPv6_EXT_HEADER_HOP_BY_HOP, 0U, 1 );
+    xGetExtensionOrder_ExpectAndReturn( ipIPv6_EXT_HEADER_HOP_BY_HOP, ipIPv6_EXT_HEADER_ROUTING_HEADER, 1 );
+    xGetExtensionOrder_ExpectAndReturn( ipIPv6_EXT_HEADER_ROUTING_HEADER, ipPROTOCOL_TCP, 2 );
+    xGetExtensionOrder_ExpectAndReturn( ipIPv6_EXT_HEADER_ROUTING_HEADER, ipPROTOCOL_TCP, 2 );
+
+    usReturn = prvChecksumIPv6Checks( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength, &xSet );
+
+    TEST_ASSERT_EQUAL( 4, usReturn );
+}
+
+
 /**
  * @brief Prepare a packet have extension with following order.
  *         - ipIPv6_EXT_HEADER_ROUTING_HEADER