From 5ce74cf40483b4436de49f65e5753d88173635f4 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 9 May 2024 12:43:37 +0530 Subject: [PATCH] Add back deleted files --- .../DHCPv6/SendDHCPMessage/Makefile.json | 28 ++++++++ .../SendDHCPMessage/SendDHCPMessage_harness.c | 69 +++++++++++++++++++ .../proofs/ProcessDHCPReplies/Makefile.json | 56 +++++++++++++++ .../ProcessDHCPReplies_harness.c | 43 ++++++++++++ 4 files changed, 196 insertions(+) create mode 100644 test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json create mode 100644 test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c create mode 100644 test/cbmc/proofs/ProcessDHCPReplies/Makefile.json create mode 100644 test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json new file mode 100644 index 000000000..524738820 --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json @@ -0,0 +1,28 @@ +{ + "ENTRY": "SendDHCPMessage", + "CBMCFLAGS": + [ + "--nondet-static" + ], + "INSTFLAGS": + [ + "--generate-function-body 'xApplicationGetRandomNumber|ulApplicationTimeHook|xBitConfig_init|vBitConfig_write_8|vBitConfig_write_16|vBitConfig_write_32|FreeRTOS_inet_pton6|FreeRTOS_sendto|vBitConfig_release'", + "--generate-function-body-options nondet-return" + ], + "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..05f24cb27 --- /dev/null +++ b/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 + +/* 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 ); +} diff --git a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json new file mode 100644 index 000000000..4bdca6f7c --- /dev/null +++ b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json @@ -0,0 +1,56 @@ +# The proof depends on one parameter: +# BUFFER_SIZE is the size of the buffer being parsed +# The buffer size must be bounded because we must bound the number of +# iterations loops iterating over the buffer. + +{ + "ENTRY": "ProcessDHCPReplies", + +################################################################ +# Buffer header: sizeof(DHCPMessage_t) = 241 +# Buffer header: sizeof(DHCPMessage_IPv4_t) = 240 + "BUFFER_HEADER": 240, + "ENDPOINT_DNS_ADDRESS_COUNT": 5, + +################################################################ +# Buffer size +# Reasonable sizes are BUFFER_SIZE > BUFFER_HEADER +# Sizes smaller than this causes CBMC to fail in simplify_byte_extract + "BUFFER_SIZE": 252, + +################################################################ +# Buffer payload + "BUFFER_PAYLOAD": "__eval 1 if {BUFFER_SIZE} <= {BUFFER_HEADER} else {BUFFER_SIZE} - {BUFFER_HEADER} + 1", + "ENDPOINT_DNS_ADDRESS_COUNT_UNWIND": "__eval {ENDPOINT_DNS_ADDRESS_COUNT} + 1", + +################################################################ + + "CBMCFLAGS": [ + # "--nondet-static", + "--unwind 1", + "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}", + "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.1:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}", + "--unwindset memcmp.0:7,__CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}" + ], + "OPT": + [ + "--export-file-local-symbols" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCP.goto", + "$(FREERTOS_PLUS_TCP)/source/portable/BufferManagement/BufferAllocation_2.goto", + "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/event_groups.goto", + "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto" + ], + + "DEF": + [ + "CBMC_DHCPMESSAGE_HEADER_SIZE={BUFFER_HEADER}", + "CBMC_FREERTOS_RECVFROM_BUFFER_BOUND={BUFFER_SIZE}", + "ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}" + ] +} diff --git a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c new file mode 100644 index 000000000..f43404c28 --- /dev/null +++ b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c @@ -0,0 +1,43 @@ +/* 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_ARP.h" + + +/**************************************************************** +* Signature of function under test +****************************************************************/ + +BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType, + NetworkEndPoint_t * pxEndPoint ); + +/**************************************************************** +* The proof for FreeRTOS_gethostbyname. +****************************************************************/ + +void harness() +{ + /* Omitting model of an unconstrained xDHCPData because xDHCPData is */ + /* the source of uninitialized data only on line 647 to set a */ + /* transaction id is an outgoing message */ + + BaseType_t xExpectedMessageType; + + NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + + __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); + pxNetworkEndPoint_Temp->pxNext = NULL; + + __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( xExpectedMessageType, pxNetworkEndPoint_Temp ); +}