Intial version with UTs fixed

Author: tony-josi-aws

source/FreeRTOS_ND.c

@@ -147,7 +147,7 @@
                                              MACAddress_t * const pxMACAddress,
                                              NetworkEndPoint_t ** ppxEndPoint )
     {
-        eARPLookupResult_t eReturn;
+        eARPLookupResult_t eReturn = eARPCacheMiss;
 
         /* Mostly used multi-cast address is ff02::. */
         if( xIsIPv6AllowedMulticast( pxAddressToLookup ) != pdFALSE )
@@ -157,14 +157,20 @@
             if( ppxEndPoint != NULL )
             {
                 *ppxEndPoint = pxFindLocalEndpoint();
-            }
 
-            eReturn = eARPCacheHit;
+                if (*ppxEndPoint != NULL)
+                {
+                    eReturn = eARPCacheHit;
+                }
+                else
+                {
+                    /* No link-local endpoint configured, eARPCacheHit */
+                }
+            }
         }
         else
         {
-            /* Not a multicast IP address. */
-            eReturn = eARPCacheMiss;
+            /* Not a multicast IP address, eARPCacheHit */
         }
 
         return eReturn;
@@ -955,6 +961,23 @@
  */
     eFrameProcessingResult_t prvProcessICMPMessage_IPv6( NetworkBufferDescriptor_t * const pxNetworkBuffer )
     {
+        /*
+            ICMPv6 messages have the following general format:
+
+            0                   1                   2                   3
+            0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1
+            +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
+            |     Type      |     Code      |          Checksum             |
+            +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
+            |                                                               |
+            +                         Message Body                          +
+            |                                                               |
+
+            The packet should contain atleast 4 bytes of general fields
+
+        */
+        if( pxNetworkBuffer->xDataLength >= ( size_t ) ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + ipICMPv6_GENERAL_FIELD_SIZE ) )
+        {
         /* MISRA Ref 11.3.1 [Misaligned access] */
         /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
         /* coverity[misra_c_2012_rule_11_3_violation] */
@@ -1029,6 +1052,14 @@
 
                                /* Find the total length of the IP packet. */
                                uxDataLength = ipNUMERIC_CAST( size_t, FreeRTOS_ntohs( pxICMPPacket->xIPHeader.usPayloadLength ) );
+                               
+                                uxNeededSize = ( size_t ) ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + uxDataLength );
+                                if( uxNeededSize > pxNetworkBuffer->xDataLength )
+                                {
+                                    FreeRTOS_printf( ( "Too small\n" ) );
+                                    break;
+                                }
+                               
                                uxDataLength = uxDataLength - sizeof( *pxICMPEchoHeader );
 
                                /* Find the first byte of the data within the ICMP packet. */
@@ -1105,6 +1136,16 @@
                    break;
 
                 case ipICMP_NEIGHBOR_ADVERTISEMENT_IPv6:
+                    {
+                        size_t uxICMPSize;
+                        uxICMPSize = sizeof( ICMPHeader_IPv6_t );
+                        uxNeededSize = ( size_t ) ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + uxICMPSize );
+
+                        if( uxNeededSize > pxNetworkBuffer->xDataLength )
+                        {
+                            FreeRTOS_printf( ( "Too small\n" ) );
+                            break;
+                        }
                     /* MISRA Ref 11.3.1 [Misaligned access] */
                     /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
                     /* coverity[misra_c_2012_rule_11_3_violation] */
@@ -1126,14 +1167,15 @@
                     {
                         prvCheckWaitingBuffer( &( pxICMPHeader_IPv6->xIPv6Address ) );
                     }
-
+                    }
                     break;
 
                 case ipICMP_ROUTER_SOLICITATION_IPv6:
                     break;
 
                     #if ( ipconfigUSE_RA != 0 )
                         case ipICMP_ROUTER_ADVERTISEMENT_IPv6:
+                            /* Size check is done inside vReceiveRA */
                             vReceiveRA( pxNetworkBuffer );
                             break;
                     #endif /* ( ipconfigUSE_RA != 0 ) */
@@ -1143,7 +1185,12 @@
                     break;
             } /* switch( pxICMPHeader_IPv6->ucTypeOfMessage ) */
         }     /* if( pxEndPoint->bits.bIPv6 != pdFALSE_UNSIGNED ) */
-
+        }
+        else
+        {
+            /* Malformed ICMPv6 packet, release the network buffer (performed
+            in prvProcessEthernetPacket)*/
+        }
         return eReleaseBuffer;
     }
 /*-----------------------------------------------------------*/

source/include/FreeRTOS_IPv6_Private.h

@@ -132,6 +132,8 @@
 struct xNetworkEndPoint;
 struct xNetworkInterface;
 
+#define ipICMPv6_GENERAL_FIELD_SIZE             (4U)
+
 #include "pack_struct_start.h"
 struct xIP_HEADER_IPv6
 {

test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c

@@ -137,7 +137,9 @@ void harness()
     uint16_t usEthernetBufferSize;
     NetworkBufferDescriptor_t * pxLocalARPWaitingNetworkBuffer;
 
-    __CPROVER_assume( ( ulLen >= sizeof( ICMPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) );
+    /* Following assumption is to make sure ulLen doesnt go 
+     * beyond CBMC_MAX_OBJECT_SIZE */
+    __CPROVER_assume( ulLen < ( CBMC_MAX_OBJECT_SIZE - ipBUFFER_PADDING ) );
 
     pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ulLen, 0 );