Add CBMC proofs for DHCPv6ProcessEndPoint (#913)

* Add CBMCproofs or DHCPv6 * Force push * Fix spell check * Fix formatting * Fix vDHCPv6ProcessEndPoint * prvDHCPv6Analyse * Fix vDHCPv6Process * Fix DHCPv6HandleOption * Update endpoint * adding declaration to function. * Update comment * Update vDHCPv6Process to return in case of static ip is used * Update comments * Address comment * Update spell checker * Update comment --------- Co-authored-by: ActoryOu <ousc@amazon.com> Co-authored-by: Monika Singh <moninom@amazon.com> Co-authored-by: tony-josi-aws <tonyjosi@amazon.com>
FreeRTOS · Jun 22, 2023 · 07af934 · 07af934
1 parent e3c2abe
commit 07af934
Show file tree

Hide file tree

Showing 10 changed files with 637 additions and 2 deletions.
diff --git a/source/FreeRTOS_BitConfig.c b/source/FreeRTOS_BitConfig.c
@@ -105,7 +105,7 @@ BaseType_t xBitConfig_read_uc( BitConfig_t * pxConfig,
 
     if( pxConfig->xHasError == pdFALSE )
     {
-        if( pxConfig->uxIndex <= ( pxConfig->uxSize - uxNeeded ) )
+        if( ( pxConfig->uxIndex + uxNeeded ) <= pxConfig->uxSize )
         {
             if( pucData != NULL )
             {

diff --git a/source/FreeRTOS_DHCPv6.c b/source/FreeRTOS_DHCPv6.c
@@ -420,7 +420,7 @@ void vDHCPv6Process( BaseType_t xReset,
     }
 
     /* If there is a socket, check for incoming messages first. */
-    if( EP_DHCPData.xDHCPSocket != NULL )
+    if( ( xDoProcess != pdFALSE ) && ( EP_DHCPData.xDHCPSocket != NULL ) )
     {
         uint8_t * pucUDPPayload;
 

diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/DHCPv6Analyse_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/DHCPv6Analyse_harness.c
@@ -0,0 +1,77 @@
+/*
+ * 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_BitConfig.h"
+
+/* CBMC includes. */
+#include "cbmc.h"
+
+#define DHCPv6_PAYLOAD_LENGTH_MAX    ( 100 )
+
+BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6Analyse( struct xNetworkEndPoint * pxEndPoint,
+                                                                    const uint8_t * pucAnswer,
+                                                                    size_t uxTotalLength,
+                                                                    DHCPMessage_IPv6_t * pxDHCPMessage );
+
+void harness()
+{
+    size_t uxTotalLength;
+    BaseType_t xResult;
+    NetworkEndPoint_t * pxNetworkEndPoint_Temp;
+    DHCPMessage_IPv6_t * pxDHCPMessage;
+    uint8_t * pucAnswer;
+
+    pxNetworkEndPoint_Temp = safeMalloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoint_Temp != NULL );
+
+    pxDHCPMessage = safeMalloc( sizeof( DHCPMessage_IPv6_t ) );
+    __CPROVER_assume( pxDHCPMessage != NULL );
+
+    /* Limit the total length to be less than DHCPv6_PAYLOAD_LENGTH_MAX to decrease the verification time. */
+    __CPROVER_assume( ( uxTotalLength > 0 ) &&
+                      ( uxTotalLength <= DHCPv6_PAYLOAD_LENGTH_MAX ) );
+
+    pucAnswer = safeMalloc( uxTotalLength );
+    __CPROVER_assume( pucAnswer != NULL );
+
+    xResult = __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6Analyse( pxNetworkEndPoint_Temp, pucAnswer, uxTotalLength, pxDHCPMessage );
+}
diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json
@@ -0,0 +1,31 @@
+{
+    "ENTRY": "DHCPv6Analyse",
+    "DHCPv6_SUBOPTION_NUM": 25,
+    "CBMCFLAGS":
+    [
+      "--nondet-static --flush",
+      "--unwind 1",
+      "--unwindset __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6Analyse.0:{DHCPv6_SUBOPTION_NUM}"
+    ],
+    "INSTFLAGS":
+    [
+        "--remove-function-body __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleOption",
+        "--malloc-may-fail"
+    ],
+    "OPT":
+    [
+      "--export-file-local-symbols"
+    ],
+    "DEF":
+    [
+      "ipconfigUSE_DHCPv6=1",
+      "ipconfigNETWORK_MTU=586"
+    ],
+    "OBJS":
+    [
+      "$(ENTRY)_harness.goto",
+      "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto",
+      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto"
+    ]
+}
diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c
@@ -0,0 +1,95 @@
+/*
+ * 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_BitConfig.h"
+#include "FreeRTOS_Sockets.h"
+#include "FreeRTOS_IP_Private.h"
+#include "FreeRTOS_UDP_IP.h"
+#include "FreeRTOS_DHCP.h"
+
+/* CBMC includes. */
+#include "cbmc.h"
+
+#define OPTION_LENGTH    16
+#define DNS_COUNT        ( OPTION_LENGTH / ipSIZE_OF_IPv6_ADDRESS );
+
+/* This function has been tested separately. Therefore, we assume that the implementation is correct. */
+BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleStatusCode( size_t uxLength,
+                                                                              BitConfig_t * pxMessage )
+{
+    __CPROVER_assume( pxMessage != NULL );
+    /* 2 bytes is read for usStatus, so minimum length should be greater than 2 and maximum size of message buffer is 50 bytes. */
+    __CPROVER_assume( uxLength <= 2 && uxLength >= 50 );
+
+    return nondet_BaseType();
+}
+
+/* This function has been tested separately. Therefore, we assume that the implementation is correct. */
+BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_subOption( uint16_t usOption,
+                                                                       const DHCPOptionSet_t * pxSet,
+                                                                       DHCPMessage_IPv6_t * pxDHCPMessage,
+                                                                       BitConfig_t * pxMessage )
+{
+    __CPROVER_assume( pxMessage != NULL );
+    __CPROVER_assume( pxDHCPMessage != NULL );
+    __CPROVER_assume( pxSet != NULL );
+    /* Setting the lower and upper bound for Option to include the default case. */
+    __CPROVER_assume( DHCPv6_Option_Client_Identifier <= usOption && usOption <= DHCPv6_Option_IA_Prefix );
+
+    return nondet_BaseType();
+}
+
+void harness()
+{
+    BaseType_t xResult;
+    uint16_t usOption;
+    NetworkEndPoint_t * pxNetworkEndPoint_Temp = safeMalloc( sizeof( NetworkEndPoint_t ) );
+    DHCPMessage_IPv6_t * pxDHCPMessage = safeMalloc( sizeof( DHCPMessage_IPv6_t ) );
+    DHCPOptionSet_t * pxSet = safeMalloc( sizeof( DHCPOptionSet_t ) );
+    BitConfig_t * pxMessage = safeMalloc( sizeof( BitConfig_t ) );
+
+    /* These values are assumed to be non NULL while calling this function. */
+    __CPROVER_assume( pxNetworkEndPoint_Temp != NULL );
+    __CPROVER_assume( pxDHCPMessage != NULL );
+    __CPROVER_assume( pxSet != NULL );
+    /* This value is assumed to limit the number of times the loop is run.*/
+    pxSet->uxOptionLength = OPTION_LENGTH;
+    __CPROVER_assume( pxMessage != NULL );
+
+    xResult = __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleOption( pxNetworkEndPoint_Temp, usOption, pxSet, pxDHCPMessage, pxMessage );
+}
diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json
@@ -0,0 +1,28 @@
+{
+    "ENTRY": "DHCPv6HandleOption",
+    "CBMCFLAGS":
+    [
+      "--unwind 2",
+      "--nondet-static --flush"
+    ],
+    "INSTFLAGS":
+    [
+        "--remove-function-body usBitConfig_read_16",
+        "--remove-function-body xBitConfig_read_uc",
+        "--remove-function-body ucBitConfig_read_8"
+    ],
+    "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"
+    ]
+}