Fix integer wrap around with IPv6 payload length field processing

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" );
+    }
+
 }