[DHCPv6] Add CBMC test for xDHCPv6Process_PassReplyToEndPoint & prvSendDHCPMessage

source/FreeRTOS_DHCPv6.c

@@ -337,13 +337,21 @@ static BaseType_t xDHCPv6Process_PassReplyToEndPoint( struct xNetworkEndPoint *
  if( pxIterator->pxDHCPMessage->xServerID.usDUIDType != 0U )
  {
  /* Check if the ID-type, the length and the contents are equal. */
- if( ( xDHCPMessage.xServerID.usDUIDType != pxIterator->pxDHCPMessage->xServerID.usDUIDType ) ||
- ( xDHCPMessage.xServerID.uxLength != pxIterator->pxDHCPMessage->xServerID.uxLength ) ||
- ( memcmp( xDHCPMessage.xServerID.pucID, pxIterator->pxDHCPMessage->xServerID.pucID, pxIterator->pxDHCPMessage->xServerID.uxLength ) != 0 ) )
+ if( pxIterator->pxDHCPMessage->xServerID.uxLength > DHCPv6_MAX_CLIENT_SERVER_ID_LENGTH )
+ {
+ FreeRTOS_printf( ( "DHCPv6 invalid uxLength.\n" ) );
+ ulCompareResult = pdFAIL;
+ }
+ else if( ( xDHCPMessage.xServerID.usDUIDType != pxIterator->pxDHCPMessage->xServerID.usDUIDType ) ||
+ ( xDHCPMessage.xServerID.uxLength != pxIterator->pxDHCPMessage->xServerID.uxLength ) ||
+ ( memcmp( xDHCPMessage.xServerID.pucID, pxIterator->pxDHCPMessage->xServerID.pucID, pxIterator->pxDHCPMessage->xServerID.uxLength ) != 0 ) )
  {
  FreeRTOS_printf( ( "DHCPv6 reply contains an unknown ID.\n" ) );
  ulCompareResult = pdFAIL;
  }
+ else
+ {
+ }
  }
 
  if( ulCompareResult == pdPASS )

test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c

@@ -0,0 +1,105 @@
+/*
+ * FreeRTOS memory safety proofs with CBMC.
+ * Copyright (C) 2022 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person
+ * obtaining a copy of this software and associated documentation
+ * files (the "Software"), to deal in the Software without
+ * restriction, including without limitation the rights to use, copy,
+ * modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be
+ * included in all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+ * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+ * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
+ * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
+ * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ *
+ * http://aws.amazon.com/freertos
+ * http://www.FreeRTOS.org
+ */
+
+
+/* Standard includes. */
+#include <stdint.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "task.h"
+#include "semphr.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_Sockets.h"
+#include "FreeRTOS_IP_Private.h"
+#include "FreeRTOS_UDP_IP.h"
+#include "FreeRTOS_DHCP.h"
+
+/* CBMC includes. */
+#include "cbmc.h"
+
+/* Extern variables. */
+extern DHCPMessage_IPv6_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPMessage;
+
+void __CPROVER_file_local_FreeRTOS_DHCPv6_c_vDHCPv6ProcessEndPoint( BaseType_t xReset,
+ NetworkEndPoint_t * pxEndPoint,
+ DHCPMessage_IPv6_t * pxDHCPMessage );
+
+BaseType_t xDHCPv6Process_PassReplyToEndPoint( struct xNetworkEndPoint * pxEndPoint );
+
+/* vDHCPv6ProcessEndPoint proved to be memory safe else where */
+static void __CPROVER_file_local_FreeRTOS_DHCPv6_c_vDHCPv6ProcessEndPoint( BaseType_t xReset,
+ NetworkEndPoint_t * pxEndPoint,
+ DHCPMessage_IPv6_t * pxDHCPMessage )
+{
+ __CPROVER_assert( pxEndPoint != NULL, "pxEndPoint != NULL" );
+ __CPROVER_assert( pxDHCPMessage != NULL, "pxDHCPMessage != NULL" );
+}
+
+void harness()
+{
+ BaseType_t xResult;
+
+ pxNetworkEndPoints = safeMalloc( sizeof( NetworkEndPoint_t ) );
+ __CPROVER_assume( pxNetworkEndPoints != NULL );
+ pxNetworkEndPoints->pxDHCPMessage = &__CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPMessage;
+
+ if( nondet_bool() )
+ {
+ pxNetworkEndPoints->pxNext = safeMalloc( sizeof( NetworkEndPoint_t ) );
+ __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+ pxNetworkEndPoints->pxNext->pxDHCPMessage = &__CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPMessage;
+ pxNetworkEndPoints->pxNext->pxNext = NULL;
+ }
+ else
+ {
+ pxNetworkEndPoints->pxNext = NULL;
+ }
+
+ NetworkEndPoint_t * pxNetworkEndPoint_Temp = safeMalloc( sizeof( NetworkEndPoint_t ) );
+ __CPROVER_assume( pxNetworkEndPoint_Temp != NULL );
+ pxNetworkEndPoint_Temp->pxNext = NULL;
+
+ pxNetworkEndPoint_Temp->pxDHCPMessage = safeMalloc( sizeof( DHCPMessage_IPv6_t ) );
+ __CPROVER_assume( pxNetworkEndPoint_Temp->pxDHCPMessage != NULL );
+
+ /* Randomize DHCPMsg as input for different scenarios. */
+ __CPROVER_havoc_object( &__CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPMessage );
+
+ /* vDHCPv6ProcessEndPoint is checked separately. */
+ if( nondet_bool() )
+ {
+ xResult = __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6Process_PassReplyToEndPoint( pxNetworkEndPoint_Temp );
+ }
+ else
+ {
+ xResult = __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6Process_PassReplyToEndPoint( pxNetworkEndPoints );
+ }
+}

test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json

@@ -0,0 +1,26 @@
+{
+ "ENTRY": "DHCPv6Process_PassReplyToEndPoint",
+ "MAX_CLIENT_SERVER_ID_LENGTH": 128,
+ "MAX_CLIENT_SERVER_ID_LENGTH_UNWIND": "__eval {MAX_CLIENT_SERVER_ID_LENGTH} + 1",
+ "CBMCFLAGS":
+ [
+ "--nondet-static",
+ "--unwind 1",
+ "--unwindset memcmp.0:{MAX_CLIENT_SERVER_ID_LENGTH_UNWIND}",
+ "--unwindset __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6Process_PassReplyToEndPoint.0:3"
+ ],
+ "OPT":
+ [
+ "--export-file-local-symbols"
+ ],
+ "DEF":
+ [
+ "ipconfigUSE_DHCPv6=1"
+ ],
+ "OBJS":
+ [
+ "$(ENTRY)_harness.goto",
+ "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto"
+ ]
+}

test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json

@@ -0,0 +1,37 @@
+{
+ "ENTRY": "SendDHCPMessage",
+ "CBMCFLAGS":
+ [
+ "--nondet-static"
+ ],
+ "INSTFLAGS":
+ [
+ "--remove-function-body xApplicationGetRandomNumber",
+ "--remove-function-body ulApplicationTimeHook",
+ "--remove-function-body xBitConfig_init",
+ "--remove-function-body vBitConfig_write_8",
+ "--remove-function-body vBitConfig_write_uc",
+ "--remove-function-body vBitConfig_write_16",
+ "--remove-function-body vBitConfig_write_32",
+ "--remove-function-body pucBitConfig_peek_last_index_uc",
+ "--remove-function-body FreeRTOS_inet_pton6",
+ "--remove-function-body FreeRTOS_sendto",
+ "--remove-function-body vBitConfig_release"
+ ],
+ "OPT":
+ [
+ "--export-file-local-symbols"
+ ],
+ "DEF":
+ [
+ "ipconfigUSE_DHCPv6=1"
+ ],
+ "OBJS":
+ [
+ "$(ENTRY)_harness.goto",
+ "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Sockets.goto",
+ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto",
+ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto"
+ ]
+}

test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c

@@ -0,0 +1,69 @@
+/*
+ * FreeRTOS memory safety proofs with CBMC.
+ * Copyright (C) 2022 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person
+ * obtaining a copy of this software and associated documentation
+ * files (the "Software"), to deal in the Software without
+ * restriction, including without limitation the rights to use, copy,
+ * modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be
+ * included in all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+ * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+ * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
+ * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
+ * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ *
+ * http://aws.amazon.com/freertos
+ * http://www.FreeRTOS.org
+ */
+
+/* Standard includes. */
+#include <stdint.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "task.h"
+#include "semphr.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_Sockets.h"
+#include "FreeRTOS_IP_Private.h"
+#include "FreeRTOS_UDP_IP.h"
+#include "FreeRTOS_DHCP.h"
+#include "FreeRTOS_DHCPv6.h"
+#include "FreeRTOS_ARP.h"
+
+/* CBMC includes. */
+#include "cbmc.h"
+
+
+
+void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( NetworkEndPoint_t * pxEndPoint );
+
+
+void harness()
+{
+ NetworkEndPoint_t * pxNetworkEndPoint_Temp = safeMalloc( sizeof( NetworkEndPoint_t ) );
+
+ __CPROVER_assume( pxNetworkEndPoint_Temp != NULL );
+
+ /* The application provides the random number and time hook in a memory safe manner. */
+
+ pxNetworkEndPoint_Temp->pxDHCPMessage = safeMalloc( sizeof( DHCPMessage_IPv6_t ) );
+
+ /* All calls to prvSendDHCPMessage are after asserts to make sure pxDHCPMessage
+ * is never NULL. [xDHCPv6ProcessEndPoint_HandleState(): configASSERT( pxDHCPMessage != NULL );] */
+ __CPROVER_assume( pxNetworkEndPoint_Temp->pxDHCPMessage != NULL );
+
+ __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( pxNetworkEndPoint_Temp );
+}

test/unit-test/FreeRTOS_DHCPv6/FreeRTOS_DHCPv6_utest.c

@@ -2420,6 +2420,50 @@ void test_vDHCPv6Process_xDHCPv6Process_PassReplyToEndPoint_DifferentServerLengt
  TEST_ASSERT_EQUAL( eWaitingAcknowledge, xEndPoint.xDHCPData.eDHCPState );
 }
 
+/**
+ * @brief The server ID length in reply message is invalid.
+ */
+void test_vDHCPv6Process_xDHCPv6Process_PassReplyToEndPoint_DifferentServerLength_HigherThanThreshold()
+{
+ NetworkEndPoint_t xEndPoint;
+ DHCPMessage_IPv6_t xDHCPMessage;
+ struct xSOCKET xLocalDHCPv6Socket;
+
+ memset( &xEndPoint, 0, sizeof( NetworkEndPoint_t ) );
+ memset( &xLocalDHCPv6Socket, 0, sizeof( struct xSOCKET ) );
+ memset( &xDHCPMessage, 0, sizeof( DHCPMessage_IPv6_t ) );
+
+ pxNetworkEndPoints = &xEndPoint;
+
+ memcpy( xEndPoint.xMACAddress.ucBytes, ucDefaultMACAddress, sizeof( ucDefaultMACAddress ) );
+ memcpy( xEndPoint.ipv6_settings.xPrefix.ucBytes, &xDefaultNetPrefix.ucBytes, sizeof( IPv6_Address_t ) );
+ xEndPoint.ipv6_settings.uxPrefixLength = 64;
+ xEndPoint.bits.bIPv6 = pdTRUE;
+ xEndPoint.bits.bWantDHCP = pdTRUE;
+
+ xEndPoint.xDHCPData.eDHCPState = eWaitingAcknowledge;
+ xEndPoint.xDHCPData.eExpectedState = eWaitingAcknowledge;
+ xEndPoint.xDHCPData.ulTransactionId = TEST_DHCPV6_TRANSACTION_ID;
+ xEndPoint.xDHCPData.xDHCPSocket = &xLocalDHCPv6Socket;
+ memcpy( xEndPoint.xDHCPData.ucClientDUID, ucTestDHCPv6OptionClientID, sizeof( ucTestDHCPv6OptionClientID ) );
+
+ xEndPoint.pxDHCPMessage = &xDHCPMessage;
+ xDHCPMessage.xServerID.usDUIDType = 1U;
+ xDHCPMessage.xServerID.uxLength = 150U;
+ memcpy( xDHCPMessage.xServerID.pucID, ucTestDHCPv6OptionServerID, sizeof( ucTestDHCPv6OptionServerID ) );
+
+ FreeRTOS_recvfrom_IgnoreAndReturn( 100 );
+ FreeRTOS_recvfrom_IgnoreAndReturn( 0 );
+ xTaskGetTickCount_IgnoreAndReturn( 0 );
+
+ prvPrepareReplyDifferentServerLength();
+
+ vDHCPv6Process( pdFALSE, &xEndPoint );
+
+ TEST_ASSERT_EQUAL( eWaitingAcknowledge, xEndPoint.xDHCPData.eDHCPState );
+}
+
+
 /**
  * @brief The server DUID in reply message is different from advertise.
  */