From e945a87e4aca2ade6056f3f2e8f003a5ea605c17 Mon Sep 17 00:00:00 2001 From: kar-rahul-aws Date: Fri, 9 Jun 2023 09:27:11 +0000 Subject: [PATCH 01/10] Add cbmc proof --- ...HCPv6Process_PassReplyToEndPoint_harness.c | 92 +++++++++++++++++++ .../Process_PassReplyToEndPoint/Makefile.json | 26 ++++++ .../DHCPv6/SendDHCPMessage/Makefile.json | 37 ++++++++ .../SendDHCPMessage/SendDHCPMessage_harness.c | 68 ++++++++++++++ 4 files changed, 223 insertions(+) create mode 100644 test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c create mode 100644 test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json create mode 100644 test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json create mode 100644 test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c diff --git a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c new file mode 100644 index 000000000..6bfa7740b --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c @@ -0,0 +1,92 @@ +/* + * 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 + +/* 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 xDHCPMessage; + +/**************************************************************** +* Signature of function under test +****************************************************************/ + +BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6Process_PassReplyToEndPoint( NetworkEndPoint_t * pxEndPoint ) +{ + return nondet_BaseType(); +} + +void harness() +{ + + BaseType_t xResult; + + pxNetworkEndPoints = safeMalloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoints != NULL ); + + if( nondet_bool() ) + { + pxNetworkEndPoints->pxNext = safeMalloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL ); + 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( &xDHCPMessage ); + + /* vDHCPv6ProcessEndPoint is checked separately. */ + + xResult = __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6Process_PassReplyToEndPoint( pxNetworkEndPoint_Temp ); +} diff --git a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json new file mode 100644 index 000000000..46cc9662a --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json @@ -0,0 +1,26 @@ +{ + "ENTRY": "DHCPv6Process_PassReplyToEndPoint", + "CBMCFLAGS": + [ + "--nondet-static", + "--unwind 1" + ], + "INSTFLAGS": + [ + "--remove-function-body vDHCPv6ProcessEndPoint" + ], + "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" + ] +} \ No newline at end of file diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json new file mode 100644 index 000000000..08cb3e73a --- /dev/null +++ b/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" + ] +} \ No newline at end of file diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c new file mode 100644 index 000000000..15a99869a --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c @@ -0,0 +1,68 @@ +/* + * 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 + +/* 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" + + +/**************************************************************** +* Signature of function under test +****************************************************************/ + +void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( NetworkEndPoint_t * pxEndPoint ); + + +void harness() +{ + NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( 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 ) ); + __CPROVER_assume( pxNetworkEndPoint_Temp->pxDHCPMessage != NULL ); + + __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( pxNetworkEndPoint_Temp ); +} From 917630a92c9ba55379ce492d208d805f5e8e3961 Mon Sep 17 00:00:00 2001 From: kar-rahul-aws Date: Fri, 9 Jun 2023 09:40:34 +0000 Subject: [PATCH 02/10] Force push --- .../DHCPv6Process_PassReplyToEndPoint_harness.c | 1 - 1 file changed, 1 deletion(-) mode change 100644 => 100755 test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c diff --git a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c old mode 100644 new mode 100755 index 6bfa7740b..41240a8f3 --- a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c +++ b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c @@ -59,7 +59,6 @@ BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6Process_PassReplyToEndP void harness() { - BaseType_t xResult; pxNetworkEndPoints = safeMalloc( sizeof( NetworkEndPoint_t ) ); From d0c97b92964c853e2fd81efcaef52da3a518bf92 Mon Sep 17 00:00:00 2001 From: kar-rahul-aws Date: Fri, 9 Jun 2023 09:56:29 +0000 Subject: [PATCH 03/10] Fix formatting --- .../cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c | 1 + 1 file changed, 1 insertion(+) diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c index 15a99869a..831c2c292 100644 --- a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c +++ b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c @@ -57,6 +57,7 @@ void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( NetworkEndPoint_ void harness() { NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); /* The application provides the random number and time hook in a memory safe manner. */ From 6a5c2d32ec4482f291935c5261f2b6d5eb9a23e7 Mon Sep 17 00:00:00 2001 From: kar-rahul-aws Date: Fri, 9 Jun 2023 10:54:31 +0000 Subject: [PATCH 04/10] Fix build error --- .../proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) mode change 100644 => 100755 test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c old mode 100644 new mode 100755 index 831c2c292..a18b4b429 --- a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c +++ b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c @@ -56,7 +56,7 @@ void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( NetworkEndPoint_ void harness() { - NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( sizeof( NetworkEndPoint_t ) ); + NetworkEndPoint_t * pxNetworkEndPoint_Temp = safeMalloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); From 159e232b20b3112f533aa3dd9732a089e7deb152 Mon Sep 17 00:00:00 2001 From: kar-rahul-aws <118818625+kar-rahul-aws@users.noreply.github.com> Date: Tue, 13 Jun 2023 08:50:43 +0530 Subject: [PATCH 05/10] Formatting fix Co-authored-by: ActoryOu --- .../proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json index 46cc9662a..a76a572a2 100644 --- a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json +++ b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json @@ -7,7 +7,7 @@ ], "INSTFLAGS": [ - "--remove-function-body vDHCPv6ProcessEndPoint" + "--remove-function-body vDHCPv6ProcessEndPoint" ], "OPT": [ From 4733120fb21914e217db42314e4439c21e58811b Mon Sep 17 00:00:00 2001 From: kar-rahul-aws <118818625+kar-rahul-aws@users.noreply.github.com> Date: Tue, 13 Jun 2023 08:51:01 +0530 Subject: [PATCH 06/10] Formatting suggestion fix Co-authored-by: ActoryOu --- .../proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json index a76a572a2..6cfa36cd4 100644 --- a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json +++ b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json @@ -2,8 +2,8 @@ "ENTRY": "DHCPv6Process_PassReplyToEndPoint", "CBMCFLAGS": [ - "--nondet-static", - "--unwind 1" + "--nondet-static", + "--unwind 1" ], "INSTFLAGS": [ From d377efa5ef6f73dbf6f070a06fbf58b50a5306c2 Mon Sep 17 00:00:00 2001 From: kar-rahul-aws <118818625+kar-rahul-aws@users.noreply.github.com> Date: Tue, 13 Jun 2023 08:51:56 +0530 Subject: [PATCH 07/10] Removing unnecessary comment Co-authored-by: ActoryOu --- .../proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c | 3 --- 1 file changed, 3 deletions(-) diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c index a18b4b429..734a4b742 100755 --- a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c +++ b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c @@ -47,9 +47,6 @@ #include "cbmc.h" -/**************************************************************** -* Signature of function under test -****************************************************************/ void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( NetworkEndPoint_t * pxEndPoint ); From a6c2fab35f0a095263da55d818a43fde48df0a38 Mon Sep 17 00:00:00 2001 From: kar-rahul-aws <118818625+kar-rahul-aws@users.noreply.github.com> Date: Tue, 13 Jun 2023 08:52:11 +0530 Subject: [PATCH 08/10] Removing unnecessary comment Co-authored-by: ActoryOu --- .../DHCPv6Process_PassReplyToEndPoint_harness.c | 3 --- 1 file changed, 3 deletions(-) diff --git a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c index 41240a8f3..df9a1f82b 100755 --- a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c +++ b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c @@ -48,9 +48,6 @@ /* Extern variables. */ extern DHCPMessage_IPv6_t xDHCPMessage; -/**************************************************************** -* Signature of function under test -****************************************************************/ BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6Process_PassReplyToEndPoint( NetworkEndPoint_t * pxEndPoint ) { From 6492b7e5cf11e43182e9466bf23d26b17f3da400 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Fri, 16 Jun 2023 18:05:01 +0530 Subject: [PATCH 09/10] add CBMC proof for xDHCPv6Process_PassReplyToEndPoint --- source/FreeRTOS_DHCPv6.c | 2 +- ...HCPv6Process_PassReplyToEndPoint_harness.c | 29 +++++++++++++++---- .../Process_PassReplyToEndPoint/Makefile.json | 10 +++---- 3 files changed, 29 insertions(+), 12 deletions(-) mode change 100755 => 100644 test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c diff --git a/source/FreeRTOS_DHCPv6.c b/source/FreeRTOS_DHCPv6.c index 4f1198cf6..a31de5d4b 100644 --- a/source/FreeRTOS_DHCPv6.c +++ b/source/FreeRTOS_DHCPv6.c @@ -334,7 +334,7 @@ static BaseType_t xDHCPv6Process_PassReplyToEndPoint( struct xNetworkEndPoint * if( pxIterator != NULL ) { - if( pxIterator->pxDHCPMessage->xServerID.usDUIDType != 0U ) + if( ( pxIterator->pxDHCPMessage->xServerID.usDUIDType != 0U ) && ( pxIterator->pxDHCPMessage->xServerID.uxLength <= DHCPv6_MAX_CLIENT_SERVER_ID_LENGTH ) ) { /* Check if the ID-type, the length and the contents are equal. */ if( ( xDHCPMessage.xServerID.usDUIDType != pxIterator->pxDHCPMessage->xServerID.usDUIDType ) || diff --git a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c old mode 100755 new mode 100644 index df9a1f82b..664e7a4bc --- a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c +++ b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c @@ -46,12 +46,21 @@ #include "cbmc.h" /* Extern variables. */ -extern DHCPMessage_IPv6_t xDHCPMessage; +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 __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6Process_PassReplyToEndPoint( NetworkEndPoint_t * pxEndPoint ) +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 ) { - return nondet_BaseType(); + __CPROVER_assert( pxEndPoint != NULL, "pxEndPoint != NULL" ); + __CPROVER_assert( pxDHCPMessage != NULL, "pxDHCPMessage != NULL" ); } void harness() @@ -60,11 +69,13 @@ void harness() 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 @@ -80,9 +91,15 @@ void harness() __CPROVER_assume( pxNetworkEndPoint_Temp->pxDHCPMessage != NULL ); /* Randomize DHCPMsg as input for different scenarios. */ - __CPROVER_havoc_object( &xDHCPMessage ); + __CPROVER_havoc_object( &__CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPMessage ); /* vDHCPv6ProcessEndPoint is checked separately. */ - - xResult = __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6Process_PassReplyToEndPoint( pxNetworkEndPoint_Temp ); + 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 ); + } } diff --git a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json index 6cfa36cd4..ef683e778 100644 --- a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json +++ b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/Makefile.json @@ -1,13 +1,13 @@ { "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" - ], - "INSTFLAGS": - [ - "--remove-function-body vDHCPv6ProcessEndPoint" + "--unwind 1", + "--unwindset memcmp.0:{MAX_CLIENT_SERVER_ID_LENGTH_UNWIND}", + "--unwindset __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6Process_PassReplyToEndPoint.0:3" ], "OPT": [ From ffe3eb6b3f0190f4cee9c95371e9651a745aac21 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Fri, 16 Jun 2023 19:06:25 +0530 Subject: [PATCH 10/10] fix unit tests, coverage, refactor --- source/FreeRTOS_DHCPv6.c | 16 +++++-- .../SendDHCPMessage/SendDHCPMessage_harness.c | 3 ++ .../FreeRTOS_DHCPv6/FreeRTOS_DHCPv6_utest.c | 44 +++++++++++++++++++ 3 files changed, 59 insertions(+), 4 deletions(-) mode change 100755 => 100644 test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c diff --git a/source/FreeRTOS_DHCPv6.c b/source/FreeRTOS_DHCPv6.c index a31de5d4b..a1db93318 100644 --- a/source/FreeRTOS_DHCPv6.c +++ b/source/FreeRTOS_DHCPv6.c @@ -334,16 +334,24 @@ static BaseType_t xDHCPv6Process_PassReplyToEndPoint( struct xNetworkEndPoint * if( pxIterator != NULL ) { - if( ( pxIterator->pxDHCPMessage->xServerID.usDUIDType != 0U ) && ( pxIterator->pxDHCPMessage->xServerID.uxLength <= DHCPv6_MAX_CLIENT_SERVER_ID_LENGTH ) ) + 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 ) diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c old mode 100755 new mode 100644 index 734a4b742..fc2886720 --- a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c +++ b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c @@ -60,6 +60,9 @@ void harness() /* 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 ); diff --git a/test/unit-test/FreeRTOS_DHCPv6/FreeRTOS_DHCPv6_utest.c b/test/unit-test/FreeRTOS_DHCPv6/FreeRTOS_DHCPv6_utest.c index 1e030bc2b..4f0cb9d26 100644 --- a/test/unit-test/FreeRTOS_DHCPv6/FreeRTOS_DHCPv6_utest.c +++ b/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. */