diff options
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/proofs')
106 files changed, 5046 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/.gitignore b/FreeRTOS-Plus/Test/CBMC/proofs/.gitignore new file mode 100644 index 000000000..3498c4b3b --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/.gitignore @@ -0,0 +1,10 @@ +# These files are generated by make_type_header_files.py +*_datastructure.h + +Makefile +Makefile.common +cbmc-batch.yaml +**/*.txt +**/*.goto + +!CMakeLists.txt diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c new file mode 100644 index 000000000..523783564 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c @@ -0,0 +1,22 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "list.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +//We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. +//This is the mock to mimic the correct expected bahvior. If this allocation fails, this might invalidate the proof. +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + NetworkBufferDescriptor_t *pxNetworkBuffer = (NetworkBufferDescriptor_t *) malloc(sizeof(NetworkBufferDescriptor_t)); + pxNetworkBuffer->pucEthernetBuffer = malloc(xRequestedSizeBytes); + pxNetworkBuffer->xDataLength = xRequestedSizeBytes; + return pxNetworkBuffer; +} + +void harness() +{ + vARPAgeCache(); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json new file mode 100644 index 000000000..83c351d70 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json @@ -0,0 +1,18 @@ +{ + "ENTRY": "ARPAgeCache", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPAgeCache.0:7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/README.md new file mode 100644 index 000000000..3352f8096 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/README.md @@ -0,0 +1,2 @@ +Assuming that xNetworkInterfaceOutput is memory safe, +this harness proves the memory safety of the vARPAgeCache function. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c new file mode 100644 index 000000000..3ec9500cc --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c @@ -0,0 +1,28 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + /* + * The assumption made here is that the buffer pointed by pucEthernerBuffer + * is at least allocated to sizeof(ARPPacket_t) size but eventually a even larger buffer. + * This is not checked inside vARPGenerateRequestPacket. + */ + uint8_t ucBUFFER_SIZE; + __CPROVER_assume( ucBUFFER_SIZE >= sizeof(ARPPacket_t) && ucBUFFER_SIZE < 2 * sizeof(ARPPacket_t) ); + void *xBuffer = malloc(ucBUFFER_SIZE); + + NetworkBufferDescriptor_t xNetworkBuffer2; + xNetworkBuffer2.pucEthernetBuffer = xBuffer; + xNetworkBuffer2.xDataLength = ucBUFFER_SIZE; + + /* vARPGenerateRequestPacket asserts buffer has room for a packet */ + __CPROVER_assume( xNetworkBuffer2.xDataLength >= sizeof(ARPPacket_t) ); + vARPGenerateRequestPacket( &xNetworkBuffer2 ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json new file mode 100644 index 000000000..65c352489 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json @@ -0,0 +1,15 @@ +{ + "ENTRY": "ARPGenerateRequestPacket", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md new file mode 100644 index 000000000..f8fdcc97d --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md @@ -0,0 +1,3 @@ +Given that the pointer target of xNetworkDescriptor.pucEthernetBuffer is allocated +to the size claimed in xNetworkDescriptor.xDataLength, +this harness proves the memory safety of ARPGenerateRequestPacket.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c new file mode 100644 index 000000000..bf188efa1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c @@ -0,0 +1,17 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + + +void harness() +{ + uint32_t ulIPAddress; + MACAddress_t xMACAddress; + + eARPGetCacheEntry( &ulIPAddress, &xMACAddress ); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json new file mode 100644 index 000000000..ecc95a87f --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json @@ -0,0 +1,41 @@ +{ + "ENTRY": "ARPGetCacheEntry", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvCacheLookup.0:7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + { + "ARPGetCacheEntry_default":[ + "ipconfigARP_STORES_REMOTE_ADDRESSES=0", + "ipconfigUSE_LLMNR=0" + ] + }, + { + "ARPGetCacheEntry_LLMNR": [ + "ipconfigARP_STORES_REMOTE_ADDRESSES=0", + "ipconfigUSE_LLMNR=1" + ] + }, + { + "ARPGetCacheEntry_STORE_REMOTE": [ + "ipconfigARP_STORES_REMOTE_ADDRESSES=1", + "ipconfigUSE_LLMNR=0" + ] + }, + { + "ARPGetCacheEntry_REMOTE_LLMNR": [ + "ipconfigARP_STORES_REMOTE_ADDRESSES=1", + "ipconfigUSE_LLMNR=1" + ] + } + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md new file mode 100644 index 000000000..03e987ebd --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md @@ -0,0 +1,4 @@ +The combined proofs in the subdirectories prove that ARPGetCacheEntry +is memory safe for all possible combinations of ipconfigARP_STORES_REMOTE_ADDRESSES +and ipconfigUSE_LLMNR. These are the only configuration +parameters used inside the ARPGetCacheEntry. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c new file mode 100644 index 000000000..442b1df6b --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c @@ -0,0 +1,14 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +void harness(){ + MACAddress_t xMACAddress; + uint32_t ulIPAddress; + eARPGetCacheEntryByMac( &xMACAddress, &ulIPAddress ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json new file mode 100644 index 000000000..0f589a8e2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json @@ -0,0 +1,17 @@ +{ + "ENTRY": "ARPGetCacheEntryByMac", + "CBMCFLAGS": + [ + "--unwind 7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + "ipconfigUSE_ARP_REVERSED_LOOKUP=1", "ipconfigARP_CACHE_ENTRIES=6" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md new file mode 100644 index 000000000..77c17e2e9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md @@ -0,0 +1,4 @@ +ARPGetCacheEntryByMac is memory safe, +if it is enabled. + +ARPGetCacheEntryByMac does not use multiple configurations internally. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c new file mode 100644 index 000000000..f2d8e61ae --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c @@ -0,0 +1,15 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + ARPPacket_t xARPFrame; + + eARPProcessPacket( &xARPFrame ); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json new file mode 100644 index 000000000..48d5d83c9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json @@ -0,0 +1,19 @@ +{ + "ENTRY": "ARPProcessPacket", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + {"disableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=0"]}, + {"enableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=1"]} + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md new file mode 100644 index 000000000..0197851b1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md @@ -0,0 +1,4 @@ +The proofs in the subdirectories show that +ARPProcessPacket is memory safe independent +of the configuration value of +ipconfigARP_USE_CLASH_DETECTION.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c new file mode 100644 index 000000000..6664d3cd0 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c @@ -0,0 +1,15 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + MACAddress_t xMACAddress; + uint32_t ulIPAddress; + vARPRefreshCacheEntry( &xMACAddress, ulIPAddress ); + vARPRefreshCacheEntry( NULL, ulIPAddress ); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json new file mode 100644 index 000000000..6cde60a51 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json @@ -0,0 +1,19 @@ +{ + "ENTRY": "ARPRefreshCacheEntry", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + {"NOT_STORE_REMOTE":["ipconfigARP_STORES_REMOTE_ADDRESSES=0"]}, + {"STORE_REMOTE":["ipconfigARP_STORES_REMOTE_ADDRESSES=1"]} + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md new file mode 100644 index 000000000..0f84300cf --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md @@ -0,0 +1,4 @@ +The proofs in this directory guarantee together that +ARPRefreshCacheEntry is memory safe independent +of the configuration value of +ipconfigARP_STORES_REMOTE_ADDRESSES. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c new file mode 100644 index 000000000..fd02b10a2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c @@ -0,0 +1,13 @@ +// /* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_ARP.h" + + +void harness() +{ + vARPSendGratuitous(); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json new file mode 100644 index 000000000..1f9616ef8 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json @@ -0,0 +1,18 @@ +{ + "ENTRY": "ARPSendGratuitous", + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md new file mode 100644 index 000000000..5bb155221 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md @@ -0,0 +1,6 @@ +Abstracting xQueueGenericSend away +and including tasks.c and FreeRTOS_IP.c: +The ARPSendGratutious function is memory safe, +if xQueueGenericSend is memory safe. + +queue.c is not compiled into the proof binary.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c new file mode 100644 index 000000000..957720133 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c @@ -0,0 +1,13 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + FreeRTOS_ClearARP(); +} + diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json new file mode 100644 index 000000000..332106c4e --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json @@ -0,0 +1,15 @@ +{ + "ENTRY": "ClearARP", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md new file mode 100644 index 000000000..2447722c9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md @@ -0,0 +1,2 @@ +This proof demonstrates the memory safety of the ClearARP function in the FreeRTOS_ARP.c file. +No restrictions are made.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json new file mode 100644 index 000000000..13792bb68 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json @@ -0,0 +1,57 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 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 +# + +{ + "ENTRY": "OutputARPRequest", + "CBMCFLAGS": + [ + "--unwind 20" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + #That is the minimal required size for an ARPPacket_t plus offset in the buffer. + "MINIMUM_PACKET_BYTES": 50, + "DEF": + [ + { + "CBMC_PROOF_ASSUMPTION_HOLDS_Packet_bytes": [ + "CBMC_PROOF_ASSUMPTION_HOLDS=1", + "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}" + ] + }, + { + "CBMC_PROOF_ASSUMPTION_HOLDS_no_packet_bytes": ["CBMC_PROOF_ASSUMPTION_HOLDS=1"] + }, + { + "CBMC_PROOF_ASSUMPTION_DOES_NOT_HOLD": ["CBMC_PROOF_ASSUMPTION_HOLDS=0"] + } + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c new file mode 100644 index 000000000..472f6b1e1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c @@ -0,0 +1,76 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 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 + */ + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + + +ARPPacket_t xARPPacket; +NetworkBufferDescriptor_t xNetworkBuffer; + +/* STUB! + * We assume that the pxGetNetworkBufferWithDescriptor function is + * implemented correctly and returns a valid data structure. + * This is the mock to mimic the expected behavior. + * If this allocation fails, this might invalidate the proof. + * FreeRTOS_OutputARPRequest calls pxGetNetworkBufferWithDescriptor + * to get a NetworkBufferDescriptor. Then it calls vARPGenerateRequestPacket + * passing this buffer along in the function call. vARPGenerateRequestPacket + * casts the pointer xNetworkBuffer.pucEthernetBuffer into an ARPPacket_t pointer + * and writes a complete ARPPacket to it. Therefore the buffer has to be at least of the size + * of an ARPPacket to gurantee memory safety. + */ +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + #ifdef CBMC_PROOF_ASSUMPTION_HOLDS + #ifdef ipconfigETHERNET_MINIMUM_PACKET_BYTES + xNetworkBuffer.pucEthernetBuffer = malloc(ipconfigETHERNET_MINIMUM_PACKET_BYTES); + #else + xNetworkBuffer.pucEthernetBuffer = malloc(xRequestedSizeBytes); + #endif + #else + uint32_t malloc_size; + __CPROVER_assert(!__CPROVER_overflow_mult(2, xRequestedSizeBytes)); + __CPROVER_assume(malloc_size > 0 && malloc_size < 2 * xRequestedSizeBytes); + xNetworkBuffer.pucEthernetBuffer = malloc(malloc_size); + #endif + xNetworkBuffer.xDataLength = xRequestedSizeBytes; + return &xNetworkBuffer; +} + + +void harness() +{ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md new file mode 100644 index 000000000..8a868dda1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md @@ -0,0 +1,29 @@ +This is the memory safety proof for FreeRTOS_OutputARPRequest. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* xNetworkInterfaceOutput + +This proof checks FreeRTOS_OutputARPRequest in multiple configuration: + +* The config_CBMC_PROOF_ASSUMPTION_HOLDS_no_packet_bytes proof + guarantees that for a buffer allocated to xDataLength, + the code executed by the FreeRTOS_OutputARPRequest function + call of FreeRTOS_ARP.c is memory safe. +* If the ipconfigETHERNET_MINIMUM_PACKET_BYTES is set and the + buffer allocated by pxGetNetworkBufferWithDescriptor allocates + a buffer of at least ipconfigETHERNET_MINIMUM_PACKET_BYTES, + the config_CBMC_PROOF_ASSUMPTION_HOLDS_Packet_bytes proof + guarantees that the code executed by the + FreeRTOS_OutputARPRequest function call + of FreeRTOS_ARP.c is memory safe. +* The third configuration in the subdirectory + config_CBMC_PROOF_ASSUMPTION_DOES_NOT_HOLD demonstrates + that the code is not memory safe, if the allocation + code violates our assumption. +* All proofs mock the pxGetNetworkBufferWithDescriptor + function for modelling the assumptions about the + buffer management layer. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c new file mode 100644 index 000000000..4975d66ee --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c @@ -0,0 +1,14 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOSIPConfig.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + FreeRTOS_PrintARPCache(); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json new file mode 100644 index 000000000..6588b10d9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json @@ -0,0 +1,17 @@ +{ + "ENTRY": "FreeRTOS_PrintARPCache", + "CBMCFLAGS": + [ + "--unwind 7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + "ipconfigARP_CACHE_ENTRIES=6" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md new file mode 100644 index 000000000..2c44908cd --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md @@ -0,0 +1,4 @@ +FreeRTOS_PrintARPCache_harness.c is memory safe, +assuming vLoggingPrintf is correct and memory safe. + +FreeRTOS_PrintARPCache does not use multiple configurations. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json new file mode 100644 index 000000000..ed1a2aca8 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json @@ -0,0 +1,47 @@ +{ + "ENTRY": "OutputARPRequest", + "MINIMUM_PACKET_BYTES": 50, + "CBMCFLAGS": + [ + "--unwind {MINIMUM_PACKET_BYTES}", + "--unwindset xNetworkBuffersInitialise.0:3,xNetworkBuffersInitialise.1:3,vListInsert.0:3,pxGetNetworkBufferWithDescriptor.0:3,pxGetNetworkBufferWithDescriptor.1:3,vNetworkInterfaceAllocateRAMToBuffers.0:3" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement/BufferAllocation_1.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Source/queue.goto" + ], + "DEF": + [ + { + "minimal_configuration": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=0" + ] + }, + { + "minimal_configuration_minimal_packet_size": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}" + ] + }, + { + "minimal_configuration_linked_rx_messages": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=1" + ] + } + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c new file mode 100644 index 000000000..3dae34a34 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c @@ -0,0 +1,71 @@ +/* This harness is linked against + * libraries/freertos_plus/standard/freertos_plus_tcp/source/portable/BufferManagement/BufferAllocation_1.goto + */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#if( ipconfigUSE_LLMNR == 1 ) + #include "FreeRTOS_DNS.h" +#endif /* ipconfigUSE_LLMNR */ +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" + +void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] ){ + for(int x = 0; x < ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS; x++){ + NetworkBufferDescriptor_t *current = &pxNetworkBuffers[x]; + #ifdef ipconfigETHERNET_MINIMUM_PACKET_BYTES + current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t) + (ipconfigETHERNET_MINIMUM_PACKET_BYTES- sizeof(ARPPacket_t))); + #else + current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t)); + #endif + current->xDataLength = sizeof(ARPPacket_t); + } +} + +/* The code expects that the Semaphore creation relying on pvPortMalloc + is successful. This is checked by an assert statement, that gets + triggered when the allocation fails. Nevertheless, the code is perfectly + guarded against a failing Semaphore allocation. To make the assert pass, + it is assumed for now, that pvPortMalloc doesn't fail. Using a model allowing + failures of the allocation might be possible + after removing the assert in l.105 of BufferAllocation_1.c, from a memory + safety point of view. */ +void *pvPortMalloc( size_t xWantedSize ){ + return malloc(xWantedSize); +} + +/* + * This function is implemented by a third party. + * After looking through a couple of samples in the demos folder, it seems + * like the only shared contract is that you want to add the if statement + * for releasing the buffer to the end. Apart from that, it is up to the vendor, + * how to write this code out to the network. + */ +BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor, BaseType_t bReleaseAfterSend ){ + if( bReleaseAfterSend != pdFALSE ) + { + vReleaseNetworkBufferAndDescriptor( pxDescriptor ); + } +} + +void harness() +{ + BaseType_t xRes = xNetworkBuffersInitialise(); + if(xRes == pdPASS){ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); + } +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md new file mode 100644 index 000000000..ea5eac78d --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md @@ -0,0 +1,27 @@ +This is the memory safety proof for ```FreeRTOS_OutputARPRequest``` +method combined with the BufferAllocation_1.c allocation strategy. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* vPortEnterCritical +* vPortExitCritical +* vPortGenerateSimulatedInterrupt +* vAssertCalled +* xTaskGetSchedulerState +* pvTaskIncrementMutexHeldCount +* xTaskRemoveFromEventList +* xTaskPriorityDisinherit + +This proof checks ```FreeRTOS_OutputARPRequest``` in multiple configurations. +All assume the memory safety of vNetworkInterfaceAllocateRAMToBuffers. +* The ```config_minimal_configuration``` proof sets + ```ipconfigUSE_LINKED_RX_MESSAGES=0```. +* The ```config_minimal_configuration_linked_rx_messages``` proof sets + ```ipconfigUSE_LINKED_RX_MESSAGES=1```. +* The ```minimal_configuration_minimal_packet_size``` proof sets + ```ipconfigETHERNET_MINIMUM_PACKET_BYTES``` to 50. + +All harnesses include the queue.c file, but test only for the happy path. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json new file mode 100644 index 000000000..fb5dd4be2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json @@ -0,0 +1,48 @@ +{ + "ENTRY": "OutputARPRequest", + "MINIMUM_PACKET_BYTES": 50, + "CBMCFLAGS": + [ + "--unwind {MINIMUM_PACKET_BYTES}", + "--unwindset xNetworkBuffersInitialise.0:3,xNetworkBuffersInitialise.1:3,vListInsert.0:3,pxGetNetworkBufferWithDescriptor.0:3,pxGetNetworkBufferWithDescriptor.1:3,vNetworkInterfaceAllocateRAMToBuffers.0:3" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement/BufferAllocation_2.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Source/queue.goto" + ], + "DEF": + [ + { + "minimal_configuration": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=0" + ] + }, + { + "minimal_configuration_minimal_packet_size": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}", + "ipconfigUSE_TCP=1" + ] + }, + { + "minimal_configuration_linked_rx_messages": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=1" + ] + } + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c new file mode 100644 index 000000000..c047a2760 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c @@ -0,0 +1,54 @@ +/* This harness is linked against + * libraries/freertos_plus/standard/freertos_plus_tcp/source/portable/BufferManagement/BufferAllocation_2.goto + */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#if( ipconfigUSE_LLMNR == 1 ) + #include "FreeRTOS_DNS.h" +#endif /* ipconfigUSE_LLMNR */ +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" + +void *pvPortMalloc( size_t xWantedSize ){ + return malloc(xWantedSize); +} + + +void vPortFree( void *pv ){ + free(pv); +} + +/* + * This function function writes a buffer to the network. We stub it + * out here, and assume it has no side effects relevant to memory safety. + */ +BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor, BaseType_t bReleaseAfterSend ){ + if( bReleaseAfterSend != pdFALSE ) + { + vReleaseNetworkBufferAndDescriptor( pxDescriptor ); + } +} + +void harness() +{ + BaseType_t xRes = xNetworkBuffersInitialise(); + if(xRes == pdPASS){ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); + } +} + diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md new file mode 100644 index 000000000..5d509a7e8 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md @@ -0,0 +1,49 @@ +This is the memory safety proof for FreeRTOS_OutputARPRequest +method combined with the BufferAllocation_2.c allocation strategy. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* vPortEnterCritical +* vPortExitCritical +* vPortGenerateSimulatedInterrupt +* vAssertCalled +* xTaskGetSchedulerState +* pvTaskIncrementMutexHeldCount +* xTaskRemoveFromEventList +* xTaskPriorityDisinherit + +* pvPortMalloc +* pvPortFree +* xNetworkInterfaceOutput +* vNetworkInterfaceAllocateRAMToBuffers + +This proof disables the tracing library in the header. + +This proof checks FreeRTOS_OutputARPRequest in multiple configuration: + +* The proof in the directory config_minimal_configuration guarantees + that the implementation and interaction between + FreeRTOS_OutputARPRequest and + FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c + are memory save. This proof depends entirely of the implementation + correctness of vNetworkInterfaceAllocateRAMToBuffers. +* The proof in directory minimal_configuration_minimal_packet_size + guarantees that using + FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c + along with the ipconfigETHERNET_MINIMUM_PACKET_BYTES is memory save + as long as TCP is enabled ( ipconfigUSE_TCP 1 ) and + ipconfigETHERNET_MINIMUM_PACKET_BYTES < sizeof( TCPPacket_t ). +* The directory minimal_configuration_minimal_packet_size_no_tcp + reminds that ipconfigETHERNET_MINIMUM_PACKET_BYTES must not be used + if TCP is disabled ( ipconfigUSE_TCP 1 ) along with the + FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c + allocator. +* The proof in directory + config_minimal_configuration_linked_rx_messages guarantees that the + ipconfigUSE_LINKED_RX_MESSAGES define does not interfere with the + memory safety claim. + +All harnesses include the queue.c file, but test only for the happy path. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.c b/FreeRTOS-Plus/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.c new file mode 100644 index 000000000..3fe245f80 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.c @@ -0,0 +1,47 @@ +#include "FreeRTOS.h" +#include "task.h" +#include "tasksStubs.h" + +#ifndef TASK_STUB_COUNTER + #define TASK_STUB_COUNTER 0; +#endif + +/* 5 is a magic number, but we need some number here as a default value. + This value is used to bound any loop depending on xTaskCheckForTimeOut + as a loop bound. It should be overwritten in the Makefile.json adapting + to the performance requirements of the harness. */ +#ifndef TASK_STUB_COUNTER_LIMIT + #define TASK_STUB_COUNTER_LIMIT 5; +#endif + + +static BaseType_t xCounter = TASK_STUB_COUNTER; +static BaseType_t xCounterLimit = TASK_STUB_COUNTER_LIMIT; + +BaseType_t xTaskGetSchedulerState( void ) +{ + return xState; +} + +/* This function is another method apart from overwritting the defines to init the max + loop bound. */ +void vInitTaskCheckForTimeOut(BaseType_t maxCounter, BaseType_t maxCounter_limit) +{ + xCounter = maxCounter; + xCounterLimit = maxCounter_limit; +} + +/* This is mostly called in a loop. For CBMC, we have to bound the loop + to a max limits of calls. Therefore this Stub models a nondet timeout in + max TASK_STUB_COUNTER_LIMIT iterations.*/ +BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait ) { + ++xCounter; + if(xCounter == xCounterLimit) + { + return pdTRUE; + } + else + { + return nondet_basetype(); + } +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CMakeLists.txt b/FreeRTOS-Plus/Test/CBMC/proofs/CMakeLists.txt new file mode 100644 index 000000000..aaa2e3c8a --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CMakeLists.txt @@ -0,0 +1,40 @@ +list(APPEND cbmc_compile_options + -m32 +) + +list(APPEND cbmc_compile_definitions + CBMC + WINVER=0x400 + _CONSOLE + _CRT_SECURE_NO_WARNINGS + _DEBUG + _WIN32_WINNT=0x0500 + __PRETTY_FUNCTION__=__FUNCTION__ + __free_rtos__ +) + +list(APPEND cbmc_compile_includes + ${CMAKE_SOURCE_DIR}/Source/include + ${CMAKE_SOURCE_DIR}/Source/portable/MSVC-MingW + ${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement + ${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include + ${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/Compiler/MSVC + ${cbmc_dir}/include + ${cbmc_dir}/windows +) + +# Remove --flag for a specific proof with list(REMOVE_ITEM cbmc_flags --flag) +list(APPEND cbmc_flags + --32 + --bounds-check + --pointer-check + --div-by-zero-check + --float-overflow-check + --nan-check + --nondet-static + --pointer-overflow-check + --signed-overflow-check + --undefined-shift-check + --unsigned-overflow-check +) + diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c new file mode 100644 index 000000000..fd0900c5e --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c @@ -0,0 +1,100 @@ +/* Standard includes. */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.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 "NetworkInterface.h" +#include "NetworkBufferManagement.h" +#include "FreeRTOS_ARP.h" + +#include "cbmc.h" + +/**************************************************************** + * Signature of function under test + ****************************************************************/ + +void prvCheckOptions( FreeRTOS_Socket_t * pxSocket, + const NetworkBufferDescriptor_t * pxNetworkBuffer ); + +/**************************************************************** + * Declare the buffer size external to the harness so it can be + * accessed by the preconditions of prvSingleStepTCPHeaderOptions, and + * give the buffer size an unconstrained value in the harness itself. + ****************************************************************/ +size_t buffer_size; + +/**************************************************************** + * Function contract proved correct by CheckOptionsOuter + ****************************************************************/ + +size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr, + size_t uxTotalLength, + FreeRTOS_Socket_t * const pxSocket, + BaseType_t xHasSYNFlag ) +{ + /* CBMC model of pointers limits the size of the buffer */ + + /* Preconditions */ + __CPROVER_assert( buffer_size < CBMC_MAX_OBJECT_SIZE, + "prvSingleStepTCPHeaderOptions: buffer_size < CBMC_MAX_OBJECT_SIZE" ); + __CPROVER_assert( 8 <= buffer_size, + "prvSingleStepTCPHeaderOptions: 8 <= buffer_size" ); + __CPROVER_assert( pucPtr != NULL, + "prvSingleStepTCPHeaderOptions: pucPtr != NULL" ); + __CPROVER_assert( uxTotalLength <= buffer_size, + "prvSingleStepTCPHeaderOptions: uxTotalLength <= buffer_size" ); + __CPROVER_assert( pxSocket != NULL, + "prvSingleStepTCPHeaderOptions: pxSocket != NULL" ); + + /* Postconditions */ + size_t index; + __CPROVER_assume( index == 1 || index <= uxTotalLength ); + + return index; +} + +/**************************************************************** + * Proof of CheckOptions + ****************************************************************/ + +void harness() +{ + /* Give buffer_size an unconstrained value */ + size_t buf_size; + + buffer_size = buf_size; + + /* pxSocket can be any socket */ + FreeRTOS_Socket_t pxSocket; + + /* pxNetworkBuffer can be any buffer descriptor with any buffer */ + NetworkBufferDescriptor_t pxNetworkBuffer; + pxNetworkBuffer.pucEthernetBuffer = malloc( buffer_size ); + pxNetworkBuffer.xDataLength = buffer_size; + + /**************************************************************** + * Specification and proof of CheckOptions + ****************************************************************/ + + /* CBMC model of pointers limits the size of the buffer */ + __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); + + /* Bound required to bound iteration over the buffer */ + __CPROVER_assume( buffer_size <= BUFFER_SIZE ); + + /* Buffer must be big enough to hold pxTCPPacket and pxTCPHeader */ + __CPROVER_assume( buffer_size > 47 ); + + prvCheckOptions( &pxSocket, &pxNetworkBuffer ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/Makefile.json new file mode 100644 index 000000000..b6f82621a --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/Makefile.json @@ -0,0 +1,18 @@ +{ + "ENTRY": "CheckOptions", + "CBMCFLAGS": "--unwind 1 --unwindset prvCheckOptions.0:41", + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Stream_Buffer.goto", + "$(FREERTOS)/Source/tasks.goto", + "$(FREERTOS)/Source/list.goto" + ], + "BUFFER_SIZE": 100, + "DEF": + [ + "BUFFER_SIZE={BUFFER_SIZE}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c new file mode 100644 index 000000000..bca2b1792 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c @@ -0,0 +1,94 @@ +/* Standard includes. */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.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 "NetworkInterface.h" +#include "NetworkBufferManagement.h" +#include "FreeRTOS_ARP.h" + +#include "cbmc.h" + +/**************************************************************** + * Signature of function under test + ****************************************************************/ + +void prvReadSackOption( const uint8_t * const pucPtr, + size_t uxIndex, + FreeRTOS_Socket_t * const pxSocket ); + +/**************************************************************** + * Proof of prvReadSackOption function contract + ****************************************************************/ + +void harness() +{ + /* pucPtr points into a buffer */ + size_t buffer_size; + uint8_t * pucPtr = malloc( buffer_size ); + + /* uxIndex in an index into the buffer */ + size_t uxIndex; + + /* pxSocket can be any socket with some initialized values */ + FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); + + pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) ); + + vListInitialise( &pxSocket->u.xTCP.xTCPWindow.xWaitQueue ); + + if( nondet_bool() ) + { + TCPSegment_t * segment = malloc( sizeof( TCPSegment_t ) ); + listSET_LIST_ITEM_OWNER( &segment->xQueueItem, ( void * ) segment ); + vListInsertEnd( &pxSocket->u.xTCP.xTCPWindow.xWaitQueue, &segment->xQueueItem ); + } + + vListInitialise( &pxSocket->u.xTCP.xTCPWindow.xTxSegments ); + + if( nondet_bool() ) + { + TCPSegment_t * segment = malloc( sizeof( TCPSegment_t ) ); + vListInitialiseItem( &segment->xSegmentItem ); + listSET_LIST_ITEM_OWNER( &segment->xQueueItem, ( void * ) segment ); + vListInsertEnd( &pxSocket->u.xTCP.xTCPWindow.xTxSegments, &segment->xQueueItem ); + } + + vListInitialise( &pxSocket->u.xTCP.xTCPWindow.xPriorityQueue ); + + extern List_t xSegmentList; + vListInitialise( &xSegmentList ); + + /**************************************************************** + * Specification and proof of CheckOptions inner loop + ****************************************************************/ + + /* Preconditions */ + + /* CBMC model of pointers limits the size of the buffer */ + __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); + + /* Both preconditions are required to avoid integer overflow in the */ + /* pointer offset of the pointer pucPtr + uxIndex + 8 */ + __CPROVER_assume( uxIndex <= buffer_size ); + __CPROVER_assume( uxIndex + 8 <= buffer_size ); + + /* Assuming quite a bit more about the initialization of pxSocket */ + __CPROVER_assume( pucPtr != NULL ); + __CPROVER_assume( pxSocket != NULL ); + + prvReadSackOption( pucPtr, uxIndex, pxSocket ); + + /* No postconditions required */ +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/Makefile.json new file mode 100644 index 000000000..8730e4f99 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/Makefile.json @@ -0,0 +1,19 @@ +{ + "ENTRY": "CheckOptionsInner", + "CBMCFLAGS": [ + "--unwind 1", + "--unwindset prvTCPWindowTxCheckAck.1:2,prvTCPWindowFastRetransmit.2:2" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Stream_Buffer.goto", + "$(FREERTOS)/Source/tasks.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c new file mode 100644 index 000000000..b8833fc79 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c @@ -0,0 +1,100 @@ +/* Standard includes. */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.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 "NetworkInterface.h" +#include "NetworkBufferManagement.h" +#include "FreeRTOS_ARP.h" + +#include "cbmc.h" + +/**************************************************************** + * Signature of the function under test + ****************************************************************/ + +size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr, + size_t uxTotalLength, + FreeRTOS_Socket_t * const pxSocket, + BaseType_t xHasSYNFlag ); + +/**************************************************************** + * Declare the buffer size external to the harness so it can be + * accessed by the preconditions of prvReadSackOption, and give the + * buffer size an unconstrained value in the harness itself. + ****************************************************************/ + +size_t buffer_size; + +/**************************************************************** + * Function contract proved correct by CheckOptionsInner + ****************************************************************/ + +void prvReadSackOption( const uint8_t * const pucPtr, + size_t uxIndex, + FreeRTOS_Socket_t * const pxSocket ) +{ + /* Preconditions */ + __CPROVER_assert( buffer_size < CBMC_MAX_OBJECT_SIZE, + "prvReadSackOption: buffer_size < CBMC_MAX_OBJECT_SIZE" ); + __CPROVER_assert( uxIndex <= buffer_size, + "prvReadSackOption: uxIndex <= buffer_size" ); + __CPROVER_assert( uxIndex + 8 <= buffer_size, + "prvReadSackOption: uxIndex + 8 <= buffer_size" ); + __CPROVER_assert( pucPtr != NULL, + "prvReadSackOption: pucPtr != NULL" ); + __CPROVER_assert( pxSocket != NULL, + "prvReadSackOption: pxSocket != NULL" ); + + /* No postconditions required */ +} + +/**************************************************************** + * Proof of prvSingleStepTCPHeaderOptions function contract + ****************************************************************/ + +void harness() +{ + /* Give buffer_size an unconstrained value */ + size_t buf_size; + + buffer_size = buf_size; + + uint8_t * pucPtr = malloc( buffer_size ); + size_t uxTotalLength; + FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); + BaseType_t xHasSYNFlag; + + /**************************************************************** + * Specification and proof of CheckOptions outer loop + ****************************************************************/ + + /* CBMC model of pointers limits the size of the buffer */ + __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); + + /* Preconditions */ + __CPROVER_assume( 8 <= buffer_size ); /* ulFirst and ulLast */ + __CPROVER_assume( pucPtr != NULL ); + __CPROVER_assume( uxTotalLength <= buffer_size ); + __CPROVER_assume( pxSocket != NULL ); + + size_t index = prvSingleStepTCPHeaderOptions( pucPtr, + uxTotalLength, + pxSocket, + xHasSYNFlag ); + + /* Postconditions */ + __CPROVER_assert( index == 1 || index <= uxTotalLength, + "prvSingleStepTCPHeaderOptions: index <= uxTotalLength" ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/Makefile.json new file mode 100644 index 000000000..dfecf7886 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/Makefile.json @@ -0,0 +1,20 @@ +{ + "ENTRY": "CheckOptionsOuter", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvSingleStepTCPHeaderOptions.2:32" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Stream_Buffer.goto", + "$(FREERTOS)/Source/tasks.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c new file mode 100644 index 000000000..bbed7b243 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -0,0 +1,102 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 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_ARP.h" + +/* Static members defined in FreeRTOS_DHCP.c */ +extern DHCPData_t xDHCPData; +extern Socket_t xDHCPSocket; +void prvCreateDHCPSocket(); + +/* Static member defined in freertos_api.c */ +#ifdef CBMC_GETNETWORKBUFFER_FAILURE_BOUND + extern uint32_t GetNetworkBuffer_failure_count; +#endif + +/**************************************************************** + * The signature of the function under test. + ****************************************************************/ + +void vDHCPProcess( BaseType_t xReset ); + +/**************************************************************** + * Abstract prvProcessDHCPReplies proved memory safe in ProcessDHCPReplies. + ****************************************************************/ + +BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType ) +{ + return nondet_BaseType(); +} + +/**************************************************************** + * The proof of vDHCPProcess + ****************************************************************/ + +void harness() +{ + BaseType_t xReset; + + /**************************************************************** + * Initialize the counter used to bound the number of times + * GetNetworkBufferWithDescriptor can fail. + ****************************************************************/ + + #ifdef CBMC_GETNETWORKBUFFER_FAILURE_BOUND + GetNetworkBuffer_failure_count = 0; + #endif + + /**************************************************************** + * Assume a valid socket in most states of the DHCP state machine. + * + * The socket is created in the eWaitingSendFirstDiscover state. + * xReset==True resets the state to eWaitingSendFirstDiscover. + ****************************************************************/ + + if( !( ( xDHCPData.eDHCPState == eWaitingSendFirstDiscover ) || + ( xReset != pdFALSE ) ) ) + { + prvCreateDHCPSocket(); + __CPROVER_assume( xDHCPSocket != NULL ); + } + + vDHCPProcess( xReset ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/Makefile.json new file mode 100644 index 000000000..d96988754 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/Makefile.json @@ -0,0 +1,56 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 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 +# + +{ + "ENTRY": "DHCPProcess", + + # Minimal buffer size for maximum coverage, see harness for details. + "BUFFER_SIZE": 299, + + # The number of times GetNetworkBufferWithDescriptor can be allowed to fail + # (plus 1). + "FAILURE_BOUND": 2, + + "CBMCFLAGS": "--unwind 4 --unwindset strlen.0:11,memcmp.0:7,prvProcessDHCPReplies.0:8,prvCreatePartDHCPMessage.0:{FAILURE_BOUND} --nondet-static --flush", + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/cbmc.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + + "DEF": + [ + "BUFFER_SIZE={BUFFER_SIZE}", + "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL=1", + "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/README.md new file mode 100644 index 000000000..0de21e6b1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/README.md @@ -0,0 +1,28 @@ +This is the memory safety proof for DHCPProcess function, which is the +function that triggers the DHCP protocol. + +The main stubs in this proof deal with buffer management, which assume +that the buffer is large enough to accomodate a DHCP message plus a +few additional bytes for options (which is the last, variable-sized +field in a DHCP message). We have abstracted away sockets, concurrency +and third-party code. For more details, please check the comments on +the harness file. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* FreeRTOS_sendto +* FreeRTOS_setsockopt +* FreeRTOS_socket +* ulRand +* vARPSendGratuitous +* vApplicationIPNetworkEventHook +* vLoggingPrintf +* vPortEnterCritical +* vPortExitCritical +* vReleaseNetworkBufferAndDescriptor +* vSocketBind +* vSocketClose + diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/cbmc-viewer.json b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/cbmc-viewer.json new file mode 100644 index 000000000..1bc333788 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/cbmc-viewer.json @@ -0,0 +1,16 @@ +{ "expected-missing-functions": + [ + "vPortEnterCritical", + "vPortExitCritical", + "vSocketBind", + "vSocketClose", + "vTaskSetTimeOutState", + "xTaskGetTickCount", + "xTaskGetCurrentTaskHandle", + "xQueueGenericSend", + "xApplicationGetRandomNumber", + "vLoggingPrintf" + ], + "proof-name": "DHCPProcess", + "proof-root": "tools/cbmc/proofs" +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c new file mode 100644 index 000000000..cbde3397b --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c @@ -0,0 +1,49 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 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 + */ + +#include <stdint.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_DHCP.h" + +/* + * The harness test proceeds to call IsDHCPSocket with an unconstrained value + */ +void harness() +{ + Socket_t xSocket; + BaseType_t xResult; + + xResult = xIsDHCPSocket( xSocket ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/Makefile.json new file mode 100644 index 000000000..eac18fd55 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/Makefile.json @@ -0,0 +1,40 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 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 +# + +{ + "ENTRY": "IsDHCPSocket", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.goto" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/README.md new file mode 100644 index 000000000..ec2cc5e21 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/README.md @@ -0,0 +1 @@ +This is the memory safety proof for IsDCHPSocket. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c new file mode 100644 index 000000000..10a81ece8 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c @@ -0,0 +1,31 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" + +/* Function prvParseDNSReply is proven to be correct separately. +The proof can be found here: https://github.com/aws/amazon-freertos/tree/master/tools/cbmc/proofs/ParseDNSReply */ +uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer, + size_t xBufferLength, + BaseType_t xExpected ) {} + +struct xDNSMessage { + uint16_t usIdentifier; + uint16_t usFlags; + uint16_t usQuestions; + uint16_t usAnswers; + uint16_t usAuthorityRRs; + uint16_t usAdditionalRRs; +}; + +typedef struct xDNSMessage DNSMessage_t; + +void harness() { + NetworkBufferDescriptor_t xNetworkBuffer; + xNetworkBuffer.pucEthernetBuffer = malloc(sizeof(UDPPacket_t)+sizeof(DNSMessage_t)); + ulDNSHandlePacket(&xNetworkBuffer); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/Makefile.json new file mode 100644 index 000000000..6b2530527 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/Makefile.json @@ -0,0 +1,12 @@ +{ + "ENTRY": "DNShandlePacket", + "CBMCFLAGS": "--unwind 1", + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/DNSclear_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/DNSclear_harness.c new file mode 100644 index 000000000..0aa26dcb6 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/DNSclear_harness.c @@ -0,0 +1,16 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" + + +void harness() { + if( ipconfigUSE_DNS_CACHE != 0 ) { + FreeRTOS_dnsclear(); + } + +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/Makefile.json new file mode 100644 index 000000000..22f54b074 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/Makefile.json @@ -0,0 +1,20 @@ +{ + "ENTRY": "DNSclear", + ################################################################ + # This configuration flag uses DNS cache + "USE_CACHE":1, + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + "DEF": + [ + "ipconfigUSE_DNS_CACHE={USE_CACHE}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c new file mode 100644 index 000000000..d831b5709 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -0,0 +1,94 @@ +/* Standard includes. */ +#include <stdint.h> +#include <stdio.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_DNS.h" +#include "FreeRTOS_DHCP.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" + +#include "cbmc.h" + +/**************************************************************** + * We abstract: + * + * All kernel task scheduling functions since we are doing + * sequential verification and the sequential verification of these + * sequential primitives is done elsewhere. + * + * Many methods in the FreeRTOS TCP API in stubs/freertos_api.c + * + * prvParseDNSReply proved memory safe elsewhere + * + * prvCreateDNSMessage + * + * This proof assumes the length of pcHostName is bounded by + * MAX_HOSTNAME_LEN. We have to bound this length because we have to + * bound the iterations of strcmp. + ****************************************************************/ + +/**************************************************************** + * Abstract prvParseDNSReply proved memory save in ParseDNSReply. + * + * We stub out his function to fill the payload buffer with + * unconstrained data and return an unconstrained size. + * + * The function under test uses only the return value of this + * function. + ****************************************************************/ + +uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer, + size_t xBufferLength, + BaseType_t xExpected ) +{ + uint32_t size; + + __CPROVER_havoc_object( pucUDPPayloadBuffer ); + return size; +} + + +/**************************************************************** + * Abstract prvCreateDNSMessage + * + * This function writes a header, a hostname, and a constant amount of + * data into the payload buffer, and returns the amount of data + * written. This abstraction just fills the entire buffer with + * unconstrained data and returns and unconstrained length. + ****************************************************************/ + +size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer, + const char * pcHostName, + TickType_t uxIdentifier ) +{ + __CPROVER_havoc_object( pucUDPPayloadBuffer ); + size_t size; + return size; +} + +/**************************************************************** + * The proof for FreeRTOS_gethostbyname. + ****************************************************************/ + +void harness() +{ + size_t len; + + __CPROVER_assume( len <= MAX_HOSTNAME_LEN ); + char * pcHostName = safeMalloc( len ); + + __CPROVER_assume( len > 0 ); /* prvProcessDNSCache strcmp */ + __CPROVER_assume( pcHostName != NULL ); + pcHostName[ len - 1 ] = NULL; + FreeRTOS_gethostbyname( pcHostName ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/Makefile.json new file mode 100644 index 000000000..e0117e38e --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/Makefile.json @@ -0,0 +1,33 @@ +{ + "ENTRY": "DNSgetHostByName", + + ################################################################ + # This configuration sets callback to 0. + # It also sets MAX_HOSTNAME_LEN to 10 to bound strcmp. + # According to the specification MAX_HOST_NAME is upto 255. + + "callback": 0, + "MAX_HOSTNAME_LEN": 10, + "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", + + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvProcessDNSCache.0:5,prvGetHostByName.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.1:{HOSTNAME_UNWIND},strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},strcmp.0:{HOSTNAME_UNWIND},strcpy.0:{HOSTNAME_UNWIND}", + "--nondet-static" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/cbmc.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + + "DEF": + [ + "ipconfigDNS_USE_CALLBACKS={callback}", + "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/cbmc-viewer.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/cbmc-viewer.json new file mode 100644 index 000000000..82e9e2b4e --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/cbmc-viewer.json @@ -0,0 +1,9 @@ +{ "expected-missing-functions": + [ + "vLoggingPrintf", + "xApplicationGetRandomNumber", + "xTaskGetTickCount" + ], + "proof-name": "DNSgetHostByName", + "proof-root": "tools/cbmc/proofs" +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c new file mode 100644 index 000000000..b6e30c8f3 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -0,0 +1,110 @@ +/* Standard includes. */ +#include <stdint.h> +#include <stdio.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_DNS.h" +#include "FreeRTOS_DHCP.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" + +#include "cbmc.h" + +/**************************************************************** + * We abstract: + * + * All kernel task scheduling functions since we are doing + * sequential verification and the sequential verification of these + * sequential primitives is done elsewhere. + * + * Many methods in the FreeRTOS TCP API in stubs/freertos_api.c + * + * prvParseDNSReply proved memory safe elsewhere + * + * prvCreateDNSMessage + * + * This proof assumes the length of pcHostName is bounded by + * MAX_HOSTNAME_LEN. We have to bound this length because we have to + * bound the iterations of strcmp. + ****************************************************************/ + +/**************************************************************** + * Abstract prvParseDNSReply proved memory safe in ParseDNSReply. + * + * We stub out his function to fill the payload buffer with + * unconstrained data and return an unconstrained size. + * + * The function under test uses only the return value of this + * function. + ****************************************************************/ + +uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer, + size_t xBufferLength, + BaseType_t xExpected ) +{ + __CPROVER_assert(pucUDPPayloadBuffer != NULL, + "Precondition: pucUDPPayloadBuffer != NULL"); + + __CPROVER_havoc_object( pucUDPPayloadBuffer ); + return nondet_uint32(); +} + +/**************************************************************** + * Abstract prvCreateDNSMessage + * + * This function writes a header, a hostname, and a constant amount of + * data into the payload buffer, and returns the amount of data + * written. This abstraction just fills the entire buffer with + * unconstrained data and returns and unconstrained length. + ****************************************************************/ + +size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer, + const char * pcHostName, + TickType_t uxIdentifier ) +{ + __CPROVER_assert(pucUDPPayloadBuffer != NULL, + "Precondition: pucUDPPayloadBuffer != NULL"); + __CPROVER_assert(pcHostName != NULL, + "Precondition: pcHostName != NULL"); + + __CPROVER_havoc_object( pucUDPPayloadBuffer ); + return nondet_sizet(); +} + +/**************************************************************** + * A stub for a function callback. + ****************************************************************/ + +void func(const char * pcHostName, void * pvSearchID, uint32_t ulIPAddress) +{ +} + +/**************************************************************** + * The proof for FreeRTOS_gethostbyname_a. + ****************************************************************/ + +void harness() { + size_t len; + + __CPROVER_assume( len <= MAX_HOSTNAME_LEN ); + char * pcHostName = safeMalloc( len ); + + __CPROVER_assume( len > 0 ); /* prvProcessDNSCache strcmp */ + __CPROVER_assume( pcHostName != NULL ); + pcHostName[ len - 1 ] = NULL; + + FOnDNSEvent pCallback = func; + TickType_t xTimeout; + void *pvSearchID; + + FreeRTOS_gethostbyname_a(pcHostName, pCallback, pvSearchID, xTimeout); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/Makefile.json new file mode 100644 index 000000000..5a3051004 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/Makefile.json @@ -0,0 +1,30 @@ +{ + "ENTRY": "DNSgetHostByName_a", + ################################################################ + # This configuration flag sets callback to 1. It also sets MAX_HOSTNAME_LEN to 10 and MAX_REQ_SIZE to 50 for performance issues. + # According to the specification MAX_HOST_NAME is upto 255. + "callback": 1, + "MAX_HOSTNAME_LEN": 10, + "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvCreateDNSMessage.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.1:{HOSTNAME_UNWIND},prvGetHostByName.0:{HOSTNAME_UNWIND},prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},strcmp.0:{HOSTNAME_UNWIND},xTaskResumeAll.0:{HOSTNAME_UNWIND},xTaskResumeAll.1:{HOSTNAME_UNWIND},strcpy.0:{HOSTNAME_UNWIND}", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/cbmc.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto" + ], + "DEF": + [ + "ipconfigDNS_USE_CALLBACKS={callback}", + "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}", + # This value is defined only when ipconfigUSE_DNS_CACHE==1 + "ipconfigDNS_CACHE_NAME_LENGTH=254" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/cbmc-viewer.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/cbmc-viewer.json new file mode 100644 index 000000000..a526bee36 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/cbmc-viewer.json @@ -0,0 +1,13 @@ +{ "expected-missing-functions": + [ + "vLoggingPrintf", + "xApplicationGetRandomNumber", + "vListInsertEnd", + "vTaskSetTimeOutState", + "vTaskSuspendAll", + "xTaskGetTickCount", + "xTaskResumeAll" + ], + "proof-name": "DNSgetHostByName_a", + "proof-root": "tools/cbmc/proofs" +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c new file mode 100644 index 000000000..1e5832b20 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c @@ -0,0 +1,49 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" +#include "list.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" + + +/* This proof assumes the length of pcHostName is bounded by MAX_HOSTNAME_LEN. This also abstracts the concurrency. */ + +void vDNSInitialise(void); + +void vDNSSetCallBack(const char *pcHostName, void *pvSearchID, FOnDNSEvent pCallbackFunction, TickType_t xTimeout, TickType_t xIdentifier); + +void *safeMalloc(size_t xWantedSize) { /* Returns a NULL pointer if the wanted size is 0. */ + if(xWantedSize == 0) { + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +/* Abstraction of xTaskCheckForTimeOut from task pool. This also abstracts the concurrency. */ +BaseType_t xTaskCheckForTimeOut(TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait) { } + +/* Abstraction of xTaskResumeAll from task pool. This also abstracts the concurrency. */ +BaseType_t xTaskResumeAll(void) { } + +/* The function func mimics the callback function.*/ +void func(const char * pcHostName, void * pvSearchID, uint32_t ulIPAddress) {} + +void harness() { + vDNSInitialise(); /* We initialize the callbacklist in order to be able to check for functions that timed out. */ + size_t pvSearchID; + FOnDNSEvent pCallback = func; + TickType_t xTimeout; + TickType_t xIdentifier; + size_t len; + __CPROVER_assume(len >= 0 && len <= MAX_HOSTNAME_LEN); + char *pcHostName = safeMalloc(len); + if (len && pcHostName) { + pcHostName[len-1] = NULL; + } + vDNSSetCallBack( pcHostName, &pvSearchID, pCallback, xTimeout, xIdentifier); /* Add an item to be able to check the cancel function if the list is non-empty. */ + FreeRTOS_gethostbyname_cancel(&pvSearchID); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/Makefile.json new file mode 100644 index 000000000..02d95ab27 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/Makefile.json @@ -0,0 +1,29 @@ +{ + "ENTRY": "DNSgetHostByName_cancel", + ################################################################ + # This configuration flag sets callback to 1. It also sets MAX_HOSTNAME_LEN to 10 for performance issues. + # According to the specification MAX_HOST_NAME is upto 255. + "callback": 1, + "MAX_HOSTNAME_LEN": 10, + "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},vDNSCheckCallBack.0:2,strcpy.0:{HOSTNAME_UNWIND}", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto", + "$(FREERTOS)/Source/tasks.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": + [ + "ipconfigDNS_USE_CALLBACKS={callback}", + "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}", + # This value is defined only when ipconfigUSE_DNS_CACHE==1 + "ipconfigDNS_CACHE_NAME_LENGTH=254" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/DNSlookup_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/DNSlookup_harness.c new file mode 100644 index 000000000..5b725c4ca --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/DNSlookup_harness.c @@ -0,0 +1,32 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" +#include "list.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" + +/* This assumes that the length of the hostname is bounded by MAX_HOSTNAME_LEN. */ +void *safeMalloc(size_t xWantedSize) { + if(xWantedSize == 0) { + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +void harness() { + if(ipconfigUSE_DNS_CACHE != 0) { + size_t len; + __CPROVER_assume(len >= 0 && len <= MAX_HOSTNAME_LEN); + char *pcHostName = safeMalloc(len); /* malloc is replaced by safeMalloc */ + if (len && pcHostName) { + pcHostName[len-1] = NULL; + } + if (pcHostName) { /* guarding against NULL pointer */ + FreeRTOS_dnslookup(pcHostName); + } + } +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/Makefile.json new file mode 100644 index 000000000..2187bb914 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/Makefile.json @@ -0,0 +1,26 @@ +{ + "ENTRY": "DNSlookup", + ################################################################ + # This configuration uses DNS cache and the MAX_HOSTNAME_LEN is set to 255 according to the specification + "MAX_HOSTNAME_LEN": 255, + "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", + "USE_CACHE": 1, + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvProcessDNSCache.0:5,strcmp.0:{HOSTNAME_UNWIND}", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + "DEF": + [ + "ipconfigUSE_DNS_CACHE={USE_CACHE}", + "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}" + ], + "OPT" : "-m32" +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/Makefile.json new file mode 100644 index 000000000..083feb6e2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/Makefile.json @@ -0,0 +1,41 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 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 +# + +{ + "ENTRY": "SendEventToIPTask", + "CBMCFLAGS": [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto", + "$(FREERTOS)/Source/tasks.goto" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/README.md new file mode 100644 index 000000000..4682310df --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/README.md @@ -0,0 +1,13 @@ +This is the memory safety proof for xSendEventToIPTask, a function used +for sending different events to IP-Task. We have abstracted away queues. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* uxQueueMessagesWaiting +* xQueueGenericSend + +The coverage is imperfect (97%) because xSendEventToIPTask always +calls xSendEventStructToIPTask with xTimeout==0. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c new file mode 100644 index 000000000..9bdcbf7af --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c @@ -0,0 +1,44 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 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 + */ + +#include <stdint.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" + +// The harness test proceeds to call SendEventToIPTask with an unconstrained value +void harness() +{ + eIPEvent_t eEvent; + xSendEventToIPTask( eEvent ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/Makefile.template b/FreeRTOS-Plus/Test/CBMC/proofs/Makefile.template new file mode 100644 index 000000000..a029394c2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/Makefile.template @@ -0,0 +1,160 @@ +default: report + +# ____________________________________________________________________ +# CBMC binaries +# + +GOTO_CC = @GOTO_CC@ +GOTO_INSTRUMENT = goto-instrument +GOTO_ANALYZER = goto-analyzer +VIEWER = cbmc-viewer + +# ____________________________________________________________________ +# Variables +# +# Naming scheme: +# `````````````` +# FOO is the concatenation of the following: +# FOO2: Set of command line +# C_FOO: Value of $FOO common to all harnesses, set in this file +# O_FOO: Value of $FOO specific to the OS we're running on, set in the +# makefile for the operating system +# H_FOO: Value of $FOO specific to a particular harness, set in the +# makefile for that harness + +ENTRY = $(H_ENTRY) +OBJS = $(H_OBJS) + +INC = \ + $(INC2) \ + $(C_INC) $(O_INC) $(H_INC) \ + # empty + +CFLAGS = \ + $(CFLAGS2) \ + $(C_DEF) $(O_DEF) $(H_DEF) $(DEF) \ + $(C_OPT) $(O_OPT) $(H_OPT) $(OPT) \ + -m32 \ + # empty + +CBMCFLAGS = \ + $(CBMCFLAGS2) \ + $(C_CBMCFLAGS) $(O_CBMCFLAGS) $(H_CBMCFLAGS) \ + # empty + +INSTFLAGS = \ + $(INSTFLAGS2) \ + $(C_INSTFLAGS) $(O_INSTFLAGS) $(H_INSTFLAGS) \ + # empty + +# ____________________________________________________________________ +# Rules +# +# Rules for building a:FR object files. These are not harness-specific, +# and several harnesses might depend on a particular a:FR object, so +# define them all once here. + +@RULE_GOTO@ + $(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) @RULE_INPUT@ + +# ____________________________________________________________________ +# Rules +# +# Rules for patching + +patch: + cd $(PROOFS)/../patches && ./patch.py + +unpatch: + cd $(PROOFS)/../patches && ./unpatch.py + +# ____________________________________________________________________ +# Rules +# +# Rules for building the CBMC harness + +queue_datastructure.h: $(H_OBJS_EXCEPT_HARNESS) + python3 @TYPE_HEADER_SCRIPT@ --binary $(FREERTOS)/Source/queue.goto --c-file $(FREERTOS)/Source/queue.c + +$(ENTRY)_harness.goto: $(ENTRY)_harness.c $(H_GENERATE_HEADER) + $(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) @RULE_INPUT@ + +$(ENTRY)1.goto: $(OBJS) + $(GOTO_CC) @COMPILE_LINK@ @RULE_OUTPUT@ --function harness $(OBJS) + +$(ENTRY)2.goto: $(ENTRY)1.goto + $(GOTO_INSTRUMENT) --add-library @RULE_INPUT@ @RULE_OUTPUT@ \ + > $(ENTRY)2.txt 2>&1 + +$(ENTRY)3.goto: $(ENTRY)2.goto + $(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \ + > $(ENTRY)3.txt 2>&1 + +$(ENTRY)4.goto: $(ENTRY)3.goto + $(GOTO_INSTRUMENT) $(INSTFLAGS) --slice-global-inits @RULE_INPUT@ @RULE_OUTPUT@ \ + > $(ENTRY)4.txt 2>&1 +# ____________________________________________________________________ +# After running goto-instrument to remove function bodies the unused +# functions need to be dropped again. + +$(ENTRY)5.goto: $(ENTRY)4.goto + $(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \ + > $(ENTRY)5.txt 2>&1 + +$(ENTRY).goto: $(ENTRY)5.goto + @CP@ @RULE_INPUT@ @RULE_OUTPUT@ + +# ____________________________________________________________________ +# Rules +# +# Rules for running CBMC + +goto: + $(MAKE) patch + $(MAKE) $(ENTRY).goto + +cbmc.txt: $(ENTRY).goto + - cbmc $(CBMCFLAGS) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1 + +property.xml: $(ENTRY).goto + cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1 + +coverage.xml: $(ENTRY).goto + cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1 + +cbmc: cbmc.txt + +property: property.xml + +coverage: coverage.xml + +report: cbmc.txt property.xml coverage.xml + $(VIEWER) \ + --goto $(ENTRY).goto \ + --srcdir $(FREERTOS) \ + --blddir $(FREERTOS) \ + --htmldir html \ + --srcexclude "(.@FORWARD_SLASH@doc|.@FORWARD_SLASH@tests|.@FORWARD_SLASH@vendors)" \ + --result cbmc.txt \ + --property property.xml \ + --block coverage.xml + +# ____________________________________________________________________ +# Rules +# +# Rules for cleaning up + +clean: + @RM@ $(OBJS) $(ENTRY).goto + @RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt + @RM@ cbmc.txt property.xml coverage.xml TAGS TAGS-* + @RM@ *~ \#* + @RM@ queue_datastructure.h + + +veryclean: clean + @RM_RECURSIVE@ html + +distclean: veryclean + cd $(PROOFS)/../patches && ./unpatch.py + cd $(PROOFS) && ./make-remove-makefiles.py diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json new file mode 100644 index 000000000..1d49986d2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json @@ -0,0 +1,47 @@ +{ + "FREERTOS": [ " ../../../../FreeRTOS" ], + "PROOFS": [ "." ], + + "DEF ": [ + "WIN32", + "WINVER=0x400", + "_CONSOLE", + "_CRT_SECURE_NO_WARNINGS", + "_DEBUG", + "_WIN32_WINNT=0x0500", + "__PRETTY_FUNCTION__=__FUNCTION__", + "__free_rtos__", + + "CBMC", + "'configASSERT(X)=__CPROVER_assert(X,\"Assertion Error\")'", + "'configPRECONDITION(X)=__CPROVER_assume(X)'", + "'_static='", + "'_volatile='" + ], + + "INC ": [ + "$(FREERTOS)/Source/include", + "$(FREERTOS)/Source/portable/MSVC-MingW", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/Compiler/MSVC", + "$(FREERTOS)/../FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Minimal_Windows_Simulator/WinPCap", + "$(FREERTOS)/Demo/Common/include", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/include", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/patches", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/windows", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/windows2" + ], + + "CBMCFLAGS ": [ + "--object-bits 7", + "--32", + "--bounds-check", + "--pointer-check" + ], + + "FORWARD_SLASH": ["/"], + + "TYPE_HEADERS": [ + "$(FREERTOS)/Source/queue.c" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/MakefileLinux.json b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileLinux.json new file mode 100644 index 000000000..08442a2ab --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileLinux.json @@ -0,0 +1,36 @@ +{ + "GOTO_CC": [ + "goto-cc" + ], + "COMPILE_LINK": [ + "-o" + ], + "COMPILE_ONLY": [ + "-c", + "-o" + ], + "RULE_INPUT": [ + "$<" + ], + "RULE_OUTPUT": [ + "$@" + ], + "RULE_GOTO": [ + "%.goto : %.c" + ], + "INC": [ + "$(PROOFS)/../windows" + ], + "RM": [ + "$(RM)" + ], + "RM_RECURSIVE": [ + "$(RM) -r" + ], + "CP": [ + "cp" + ], + "TYPE_HEADER_SCRIPT": [ + "$(PROOFS)/make_type_header_files.py" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/MakefileWindows.json b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileWindows.json new file mode 100644 index 000000000..543dd6219 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileWindows.json @@ -0,0 +1,44 @@ +{ + "DEF": [ + "WIN32" + ], + "GOTO_CC": [ + "goto-cl" + ], + "COMPILE_LINK": [ + "/Fe" + ], + "COMPILE_ONLY": [ + "/c", + "/Fo" + ], + "RULE_INPUT": [ + "$**" + ], + "RULE_OUTPUT": [ + "$@" + ], + "RULE_GOTO": [ + ".c.goto:" + ], + "OPT": [ + "/wd4210", + "/wd4127", + "/wd4214", + "/wd4201", + "/wd4244", + "/wd4310" + ], + "RM": [ + "del" + ], + "RM_RECURSIVE": [ + "del /s" + ], + "CP": [ + "copy" + ], + "TYPE_HEADER_SCRIPT": [ + "$(PROOFS)\\make_type_header_files.py" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/Makefile.json new file mode 100644 index 000000000..f372c41da --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/Makefile.json @@ -0,0 +1,68 @@ +# The proof depends on one parameter: +# NETWORK_BUFFER_SIZE is the size of the network buffer being parsed +# The buffer size must be bounded because we must bound the number of +# iterations loops iterating over the buffer. + +{ + "ENTRY": "ParseDNSReply", + +################################################################ +# This is the network buffer size. +# Reasonable values are size > 12 = sizeof(xDNSMessage) + "NETWORK_BUFFER_SIZE": 40, + +################################################################ +# This is the size of the buffer into which the name is copied. +# Set to any positive value. +# In the source, NAME_SIZE=254 and NETWORK_BUFFER_SIZE >> NAME_SIZE +# In the proof, NAME_SIZE >= 4 required for good coverage. + "NAME_SIZE": "10", + +################################################################ +# Loop prvParseDNSReply.0: +# file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 915 + "PARSELOOP0": "prvParseDNSReply.0", + +# M = sizeof( DNSMessage_t ) = 12 +# U = sizeof( uint32_t) = 4 +# Loop bound is (NETWORK_BUFFER_SIZE - M) div (U+1) + 1 tight for SIZE >= M +# Loop bound is 1 for 0 <= SIZE < M + "PARSELOOP0_UNWIND": + "__eval 1 if {NETWORK_BUFFER_SIZE} < 12 else ({NETWORK_BUFFER_SIZE} - 12) / 5 + 1", + +################################################################ +# Loop prvParseDNSReply.1: +# file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 989 + "PARSELOOP1": "prvParseDNSReply.1", + +# A = sizeof( DNSAnswerRecord_t ) = 10 +# M = sizeof( DNSMessage_t ) = 12 +# U = sizeof( uint32_t) = 4 +# Loop bound is (NETWORK_BUFFER_SIZE - M - A) div (A+1) + A + 1 tight +# for SIZE >= M + A +# Loop bound is (NETWORK_BUFFER_SIZE - M) + 1 for M <= SIZE < M + A +# Loop bound is 1 for 0 <= SIZE < M + "PARSELOOP1_UNWIND": + "__eval 1 if {NETWORK_BUFFER_SIZE} < 12 else ({NETWORK_BUFFER_SIZE} - 11 if {NETWORK_BUFFER_SIZE} < 22 else ({NETWORK_BUFFER_SIZE} - 12 - 10) / 11 + 11)", + +################################################################ + + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset {PARSELOOP0}:{PARSELOOP0_UNWIND},{PARSELOOP1}:{PARSELOOP1_UNWIND},prvProcessDNSCache.0:5" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + + "DEF": + [ + "NETWORK_BUFFER_SIZE={NETWORK_BUFFER_SIZE}", + "NAME_SIZE={NAME_SIZE}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/ParseDNSReply_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/ParseDNSReply_harness.c new file mode 100644 index 000000000..3ae1256a0 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/ParseDNSReply_harness.c @@ -0,0 +1,130 @@ +/* Standard includes. */ +#include <stdint.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "list.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_DNS.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" +#include "IPTraceMacroDefaults.h" + +#include "cbmc.h" + +/**************************************************************** + * Signature of function under test + ****************************************************************/ + +uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer, + size_t uxBufferLength, + BaseType_t xExpected ); + +/**************************************************************** + * Abstraction of prvReadNameField proved in ReadNameField + ****************************************************************/ + +size_t prvReadNameField( const uint8_t *pucByte, + size_t uxRemainingBytes, + char *pcName, + size_t uxDestLen ) +{ + __CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, + "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE"); + __CPROVER_assert(NAME_SIZE < CBMC_MAX_OBJECT_SIZE, + "NAME_SIZE < CBMC_MAX_OBJECT_SIZE"); + __CPROVER_assert(NAME_SIZE >= 4, + "NAME_SIZE >= 4 required for good coverage."); + + + /* Preconditions */ + __CPROVER_assert(uxRemainingBytes < CBMC_MAX_OBJECT_SIZE, + "ReadNameField: uxRemainingBytes < CBMC_MAX_OBJECT_SIZE)"); + __CPROVER_assert(uxDestLen < CBMC_MAX_OBJECT_SIZE, + "ReadNameField: uxDestLen < CBMC_MAX_OBJECT_SIZE)"); + + __CPROVER_assert(uxRemainingBytes <= NETWORK_BUFFER_SIZE, + "ReadNameField: uxRemainingBytes <= NETWORK_BUFFER_SIZE)"); + + /* This precondition in the function contract for prvReadNameField + * fails because prvCheckOptions called prvReadNameField with the + * constant value 254. + __CPROVER_assert(uxDestLen <= NAME_SIZE, + "ReadNameField: uxDestLen <= NAME_SIZE)"); + */ + + __CPROVER_assert( pucByte != NULL , + "ReadNameField: pucByte != NULL )"); + __CPROVER_assert( pcName != NULL , + "ReadNameField: pcName != NULL )"); + + __CPROVER_assert(uxDestLen > 0, + "ReadNameField: uxDestLen > 0)"); + + /* Return value */ + size_t index; + + /* Postconditions */ + __CPROVER_assume( index <= uxDestLen+1 && index <= uxRemainingBytes ); + + return index; +} + +/**************************************************************** + * Abstraction of prvSkipNameField proved in SkipNameField + ****************************************************************/ + +size_t prvSkipNameField( const uint8_t *pucByte, size_t uxLength ) +{ + + __CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, + "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE"); + + + /* Preconditions */ + __CPROVER_assert(uxLength < CBMC_MAX_OBJECT_SIZE, + "SkipNameField: uxLength < CBMC_MAX_OBJECT_SIZE)"); + __CPROVER_assert(uxLength <= NETWORK_BUFFER_SIZE, + "SkipNameField: uxLength <= NETWORK_BUFFER_SIZE)"); + __CPROVER_assert(pucByte != NULL, + "SkipNameField: pucByte != NULL)"); + + /* Return value */ + size_t index; + + /* Postconditions */ + __CPROVER_assume(index <= uxLength); + + return index; +} + +/**************************************************************** + * Proof of prvParseDNSReply + ****************************************************************/ + +void harness() { + + size_t uxBufferLength; + BaseType_t xExpected; + uint8_t *pucUDPPayloadBuffer = malloc(uxBufferLength); + + __CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, + "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE"); + + __CPROVER_assume(uxBufferLength < CBMC_MAX_OBJECT_SIZE); + __CPROVER_assume(uxBufferLength <= NETWORK_BUFFER_SIZE); + __CPROVER_assume(pucUDPPayloadBuffer != NULL); + + uint32_t index = prvParseDNSReply( pucUDPPayloadBuffer, + uxBufferLength, + xExpected ); + +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/Makefile.json new file mode 100644 index 000000000..c708bac13 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/Makefile.json @@ -0,0 +1,48 @@ +# 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, + +################################################################ +# 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", + +################################################################ + + "CBMCFLAGS": [ + # "--nondet-static", + "--unwind 1", + "--unwindset memcmp.0:7,prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/cbmc.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement/BufferAllocation_2.goto", + "$(FREERTOS)/Source/event_groups.goto", + "$(FREERTOS)/Source/list.goto" + ], + + "DEF": + [ + "CBMC_DHCPMESSAGE_HEADER_SIZE={BUFFER_HEADER}", + "CBMC_FREERTOS_RECVFROM_BUFFER_BOUND={BUFFER_SIZE}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c new file mode 100644 index 000000000..ec2fb1c8c --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c @@ -0,0 +1,37 @@ +/* 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_ARP.h" + + +/**************************************************************** + * Signature of function under test + ****************************************************************/ + +BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType ); + +/**************************************************************** + * 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; + + prvProcessDHCPReplies( xExpectedMessageType ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/README.md new file mode 100644 index 000000000..48fb7c48d --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/README.md @@ -0,0 +1 @@ +This directory contains the proofs checked by CBMC. For each entry point of FreeRTOS tested, there is a directory that contains the test harness and cbmc configuration information needed to check the proof.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/Makefile.json new file mode 100644 index 000000000..05f3d4208 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/Makefile.json @@ -0,0 +1,54 @@ +{ + "ENTRY": "ReadNameField", + +################################################################ +#Enable DNS callbacks or else ReadNameField is not defined + "callbacks": "1", + +################################################################ +# This is the network buffer size. Set to any positive value. + "NETWORK_BUFFER_SIZE" : "10", + +################################################################ +# This is the size of the buffer into which the name is copied. +# Set to any positive value. +# In the source, NAME_SIZE=254 and NETWORK_BUFFER_SIZE >> NAME_SIZE +# In the proof, NAME_SIZE >= 4 required for good coverage. + "NAME_SIZE": "6", + +################################################################ +# Loop prvReadNameField.0: +# should be min of buffer size and name size +# but loop must be unwound at least once, so max of this and 1+1 + "READLOOP0": "prvReadNameField.0", + "READLOOP0_UNWIND": "__eval max(2, min({NETWORK_BUFFER_SIZE}, {NAME_SIZE}+1))", + +################################################################ +# Loop prvReadNameField.1: +# should be min of buffer size and name size +# but loop must be unwound at least twice, so max of this and 2+1 + "READLOOP1": "prvReadNameField.1", + "READLOOP1_UNWIND": "__eval max(3, min({NETWORK_BUFFER_SIZE}, {NAME_SIZE}))", + +################################################################ + + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset {READLOOP0}:{READLOOP0_UNWIND},{READLOOP1}:{READLOOP1_UNWIND}" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + + "DEF": + [ + "NETWORK_BUFFER_SIZE={NETWORK_BUFFER_SIZE}", + "NAME_SIZE={NAME_SIZE}", + "ipconfigDNS_USE_CALLBACKS={callbacks}", + "ipconfigDNS_CACHE_NAME_LENGTH=254" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c new file mode 100644 index 000000000..86e30b1fd --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c @@ -0,0 +1,102 @@ +/* Standard includes. */ +#include <stdint.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "list.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_DNS.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" +#include "IPTraceMacroDefaults.h" + +#include "cbmc.h" + +/**************************************************************** + * Signature of function under test + ****************************************************************/ + +size_t prvReadNameField( const uint8_t *pucByte, + size_t uxRemainingBytes, + char *pcName, + size_t uxDestLen ); + +/**************************************************************** + * The function under test is not defined in all configurations + ****************************************************************/ + +#if ( ipconfigUSE_DNS_CACHE == 1 ) || ( ipconfigDNS_USE_CALLBACKS == 1 ) + +/* prvReadNameField is defined in this configuration */ + +#else + +/* prvReadNameField is not defined in this configuration, stub it. */ + +size_t prvReadNameField( const uint8_t *pucByte, + size_t uxRemainingBytes, + char *pcName, + size_t uxDestLen ) +{ + return 0; +} + +#endif + + +/**************************************************************** + * Proof of prvReadNameField function contract + ****************************************************************/ + +void harness() { + + __CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, + "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE"); + __CPROVER_assert(NAME_SIZE < CBMC_MAX_OBJECT_SIZE, + "NAME_SIZE < CBMC_MAX_OBJECT_SIZE"); + + __CPROVER_assert(NAME_SIZE >= 4, + "NAME_SIZE >= 4 required for good coverage."); + + + size_t uxRemainingBytes; + size_t uxDestLen; + + uint8_t *pucByte = malloc(uxRemainingBytes); + char *pcName = malloc(uxDestLen); + + /* Preconditions */ + + __CPROVER_assume(uxRemainingBytes < CBMC_MAX_OBJECT_SIZE); + __CPROVER_assume(uxDestLen < CBMC_MAX_OBJECT_SIZE); + + __CPROVER_assume(uxRemainingBytes <= NETWORK_BUFFER_SIZE); + __CPROVER_assume(uxDestLen <= NAME_SIZE); + + __CPROVER_assume( pucByte != NULL ); + __CPROVER_assume( pcName != NULL ); + + /* Avoid overflow on uxSourceLen - 1U with uxSourceLen == uxRemainingBytes */ + //__CPROVER_assume(uxRemainingBytes > 0); + + /* Avoid overflow on uxDestLen - 1U */ + __CPROVER_assume(uxDestLen > 0); + + size_t index = prvReadNameField( pucByte, + uxRemainingBytes, + pcName, + uxDestLen ); + + /* Postconditions */ + + __CPROVER_assert( index <= uxDestLen+1 && index <= uxRemainingBytes, + "prvReadNamefield: index <= uxDestLen+1"); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/Makefile.json new file mode 100644 index 000000000..cb2e7a9cc --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/Makefile.json @@ -0,0 +1,32 @@ +{ + "ENTRY": "SkipNameField", + +################################################################ +# This is the network buffer size. This can be set to any positive value. + "NETWORK_BUFFER_SIZE": 10, + +################################################################ +# Loop prvSkipNameField.0: +# file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 778 +# bound should be half network buffer size, since chunk length is at least 2 + "SKIPLOOP0": "prvSkipNameField.0", + "SKIPLOOP0_UNWIND": "__eval ({NETWORK_BUFFER_SIZE} + 1) / 2", + +################################################################ + + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset {SKIPLOOP0}:{SKIPLOOP0_UNWIND}" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + "DEF": + [ + "NETWORK_BUFFER_SIZE={NETWORK_BUFFER_SIZE}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/SkipNameField_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/SkipNameField_harness.c new file mode 100644 index 000000000..2820e444d --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/SkipNameField_harness.c @@ -0,0 +1,54 @@ +/* Standard includes. */ +#include <stdint.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "list.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_DNS.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" +#include "IPTraceMacroDefaults.h" + +#include "cbmc.h" + +/**************************************************************** + * Signature of function under test + ****************************************************************/ + +size_t prvSkipNameField( const uint8_t *pucByte, size_t uxLength ); + +/**************************************************************** + * Proof of prvSkipNameField function contract + ****************************************************************/ + +void harness() { + + __CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, + "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE"); + + size_t uxLength; + uint8_t *pucByte = malloc( uxLength ); + + /* Preconditions */ + + __CPROVER_assume(uxLength < CBMC_MAX_OBJECT_SIZE); + __CPROVER_assume(uxLength <= NETWORK_BUFFER_SIZE); + __CPROVER_assume(pucByte != NULL); + + size_t index = prvSkipNameField( pucByte, uxLength ); + + /* Postconditions */ + + __CPROVER_assert(index <= uxLength, + "prvSkipNameField: index <= uxLength"); + +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/Makefile.json new file mode 100644 index 000000000..8f2f3037e --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/Makefile.json @@ -0,0 +1,59 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 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 +# + +{ + "ENTRY": "TCPHandleState", + "TX_DRIVER":1, + "RX_MESSAGES":1, + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvWinScaleFactor.0:2", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto" + ], + "DEF": + [ + "ipconfigZERO_COPY_TX_DRIVER={TX_DRIVER}", + "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INSTFLAGS": + [ + "--remove-function-body prvTCPPrepareSend", + "--remove-function-body prvTCPReturnPacket" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/README.md new file mode 100644 index 000000000..8f08c5931 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/README.md @@ -0,0 +1,22 @@ +This is the memory safety proof for prvTCPHandleState. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* prvTCPPrepareSend (proved independently) +* prvTCPReturnPacket (proved independently) + +* lTCPAddRxdata +* lTCPWindowRxCheck +* lTCPWindowTxAdd +* ulTCPWindowTxAck +* vTCPWindowInit +* xTCPWindowRxEmpty +* xTCPWindowTxDone + +* uxStreamBufferGet +* vReleaseNetworkBufferAndDescriptor +* vSocketWakeUpUser +* xTaskGetTickCount diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c new file mode 100644 index 000000000..03867685a --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c @@ -0,0 +1,73 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 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 + */ + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_TCP_IP.h" + +#include "../../utility/memory_assignments.c" + +/* This proof assumes that prvTCPPrepareSend and prvTCPReturnPacket are correct. +These functions are proved to be correct separately. */ + +BaseType_t publicTCPHandleState( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer ); + +void harness() { + FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + size_t socketSize = sizeof(FreeRTOS_Socket_t); + if (ensure_memory_is_valid(pxSocket, socketSize)) { + /* ucOptionLength is the number of valid bytes in ulOptionsData[]. + ulOptionsData[] is initialized as uint32_t ulOptionsData[ipSIZE_TCP_OPTIONS/sizeof(uint32_t)]. + This assumption is required for a memcpy function that copies uxOptionsLength + data from pxTCPHeader->ucOptdata to pxTCPWindow->ulOptionsData.*/ + __CPROVER_assume(pxSocket->u.xTCP.xTCPWindow.ucOptionLength == sizeof(uint32_t) * ipSIZE_TCP_OPTIONS/sizeof(uint32_t)); + /* uxRxWinSize is initialized as size_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/ + __CPROVER_assume(pxSocket->u.xTCP.uxRxWinSize >= 0 && pxSocket->u.xTCP.uxRxWinSize <= sizeof(size_t)); + /* uxRxWinSize is initialized as uint16_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/ + __CPROVER_assume(pxSocket->u.xTCP.usInitMSS == sizeof(uint16_t)); + } + + NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + size_t bufferSize = sizeof(NetworkBufferDescriptor_t); + if(ensure_memory_is_valid(pxNetworkBuffer, bufferSize)) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(TCPPacket_t)); + } + if (ensure_memory_is_valid(pxSocket, socketSize) && + ensure_memory_is_valid(pxNetworkBuffer, bufferSize) && + ensure_memory_is_valid(pxNetworkBuffer->pucEthernetBuffer, sizeof(TCPPacket_t)) && + ensure_memory_is_valid(pxSocket->u.xTCP.pxPeerSocket, socketSize)) { + + publicTCPHandleState(pxSocket, &pxNetworkBuffer); + + } +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/Makefile.json new file mode 100644 index 000000000..5d34818b5 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/Makefile.json @@ -0,0 +1,49 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 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 +# + +{ + "ENTRY": "TCPPrepareSend", + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto" + ], + "DEF": + [ + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/README.md new file mode 100644 index 000000000..323461918 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/README.md @@ -0,0 +1,15 @@ +This is the memory safety proof for prvTCPPrepareSend. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* ulTCPWindowTxGet +* xTCPWindowTxDone + +* xTaskGetTickCount + +* uxStreamBufferGet +* vReleaseNetworkBufferAndDescriptor +* vSocketWakeUpUser diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c new file mode 100644 index 000000000..9c41d7b7f --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c @@ -0,0 +1,72 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 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 + */ + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_TCP_IP.h" +#include "FreeRTOS_Stream_Buffer.h" + +#include "../../utility/memory_assignments.c" + +/* This proof assumes that pxGetNetworkBufferWithDescriptor is implemented correctly. */ +int32_t publicTCPPrepareSend( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer, UBaseType_t uxOptionsLength ); + +/* Abstraction of pxGetNetworkBufferWithDescriptor. It creates a buffer. */ +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + NetworkBufferDescriptor_t *pxBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated (); + size_t bufferSize = sizeof(NetworkBufferDescriptor_t); + if (ensure_memory_is_valid(pxBuffer, bufferSize)) { + /* The code does not expect pucEthernetBuffer to be equal to NULL if + pxBuffer is not NULL. */ + pxBuffer->pucEthernetBuffer = malloc(xRequestedSizeBytes); + pxBuffer->xDataLength = xRequestedSizeBytes; + } + return pxBuffer; +} + +void harness() { + FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + size_t socketSize = sizeof(FreeRTOS_Socket_t); + size_t bufferSize = sizeof(TCPPacket_t); + if (ensure_memory_is_valid(pxNetworkBuffer, sizeof(*pxNetworkBuffer))) { + pxNetworkBuffer->xDataLength = bufferSize; + /* The code does not expect pucEthernetBuffer to be equal to NULL if + pxNetworkBuffer is not NULL. */ + pxNetworkBuffer->pucEthernetBuffer = malloc(bufferSize); + } + UBaseType_t uxOptionsLength; + if(pxSocket) { + publicTCPPrepareSend(pxSocket, &pxNetworkBuffer, uxOptionsLength ); + } +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/Makefile.json new file mode 100644 index 000000000..e0f4b2403 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/Makefile.json @@ -0,0 +1,51 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 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 +# + +{ + "ENTRY": "TCPReturnPacket", + "RX_MESSAGES":1, + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto" + ], + "DEF": + [ + "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/README.md new file mode 100644 index 000000000..1efd644d1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/README.md @@ -0,0 +1,10 @@ +This is the memory safety proof for prvTCPReturnPacket. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* usGenerateChecksum +* usGenerateProtocolChecksum +* xNetworkInterfaceOutput diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c new file mode 100644 index 000000000..19552565b --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c @@ -0,0 +1,67 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 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 + */ + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_TCP_IP.h" + +#include "../../utility/memory_assignments.c" + +/* This proof assumes that pxDuplicateNetworkBufferWithDescriptor is implemented correctly. */ + +void publicTCPReturnPacket( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t *pxNetworkBuffer, uint32_t ulLen, BaseType_t xReleaseAfterSend ); + +/* Abstraction of pxDuplicateNetworkBufferWithDescriptor*/ +NetworkBufferDescriptor_t *pxDuplicateNetworkBufferWithDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer, + BaseType_t xNewLength ) { + NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + if (ensure_memory_is_valid(pxNetworkBuffer, sizeof(*pxNetworkBuffer))) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(TCPPacket_t)); + __CPROVER_assume(pxNetworkBuffer->pucEthernetBuffer); + } + return pxNetworkBuffer; +} + +void harness() { + FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + if (ensure_memory_is_valid(pxNetworkBuffer, sizeof(*pxNetworkBuffer))) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(TCPPacket_t)); + __CPROVER_assume(pxNetworkBuffer->pucEthernetBuffer); + } + uint32_t ulLen; + BaseType_t xReleaseAfterSend; + /* The code does not expect both of these to be equal to NULL at the same time. */ + __CPROVER_assume(pxSocket != NULL || pxNetworkBuffer != NULL); + publicTCPReturnPacket(pxSocket, pxNetworkBuffer, ulLen, xReleaseAfterSend); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_cbmc_batch_files.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_cbmc_batch_files.py new file mode 100755 index 000000000..622e000c3 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_cbmc_batch_files.py @@ -0,0 +1,53 @@ +#!/usr/bin/env python3 +# +# Generation of the cbmc-batch.yaml files for the CBMC proofs. +# +# Copyright (C) 2019 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. + +import os +import platform +import subprocess + + +def remove_cbmc_yaml_files(): + for dyr, _, files in os.walk("."): + cbmc_batch_files = [os.path.join(os.path.abspath(dyr), file) + for file in files if file == "cbmc-batch.yaml"] + for file in cbmc_batch_files: + os.remove(file) + + +def create_cbmc_yaml_files(): + # The YAML files are only used by CI and are not needed on Windows. + if platform.system() == "Windows": + return + for dyr, _, files in os.walk("."): + harness = [file for file in files if file.endswith("_harness.c")] + if harness and "Makefile" in files: + subprocess.run(["make", "cbmc-batch.yaml"], + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + cwd=os.path.abspath(dyr), + check=True) + +if __name__ == '__main__': + remove_cbmc_yaml_files() + create_cbmc_yaml_files() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_common_makefile.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_common_makefile.py new file mode 100755 index 000000000..efcf1db8d --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_common_makefile.py @@ -0,0 +1,240 @@ +#!/usr/bin/env python3 +# +# Generation of common Makefile for CBMC proofs. +# +# Copyright (C) 2019 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. + +from pprint import pprint +import json +import sys +import re +import os +import argparse + +def cleanup_whitespace(string): + return re.sub('\s+', ' ', string.strip()) + +################################################################ +# Operating system specific values + +platform_definitions = { + "linux": { + "platform": "linux", + "separator": "/", + "define": "-D", + "include": "-I", + }, + "macos": { + "platform": "darwin", + "separator": "/", + "define": "-D", + "include": "-I", + }, + "windows": { + "platform": "win32", + "separator": "\\", + "define": "/D", + "include": "/I", + }, +} + + +def default_platform(): + for platform, definition in platform_definitions.items(): + if sys.platform == definition["platform"]: + return platform + return "linux" + + +def patch_path_separator(opsys, string): + from_separator = '/' + to_separator = platform_definitions[opsys]["separator"] + + def escape_separator(string): + return string.split(from_separator + from_separator) + + def change_separator(string): + return string.replace(from_separator, to_separator) + + return from_separator.join([change_separator(escaped) + for escaped in escape_separator(string)]) + +def patch_compile_output(opsys, line, key, value): + if opsys != "windows": + return line + + if key in ["COMPILE_ONLY", "COMPILE_LINK"] and value is not None: + if value[-1] == '/Fo': + return re.sub('/Fo\s+', '/Fo', line) + if value[-1] == '/Fe': + return re.sub('/Fe\s+', '/Fe', line) + return line + +################################################################ +# Argument parsing +# + +def get_arguments(): + parser = argparse.ArgumentParser() + parser.add_argument( + "--system", + metavar="OS", + choices=platform_definitions, + default=str(default_platform()), + help="Generate makefiles for operating system OS" + ) + return parser.parse_args() + +################################################################ +# Variable definitions +# +# JSON files give variable definitions for common, operating system, +# and harness specfic values +# + +def read_variable_definitions(filename): + variable = {} + with open(filename) as _file: + for key, values in json.load(_file).items(): + variable[cleanup_whitespace(key)] = [cleanup_whitespace(value) + for value in values] + return variable + +def find_definition_once(key, defines, prefix=None): + + # Try looking up key with and without prefix + prefix = "{}_".format(prefix.rstrip('_')) if prefix else "" + key2 = key[len(prefix):] if key.startswith(prefix) else prefix + key + + for _key in [key, key2]: + _value = defines.get(_key) + if _value is not None: + return _value + + return None + +def find_definition(key, defines): + common_defines, opsys_defines, harness_defines = defines + return (find_definition_once(key, harness_defines, "H") or + find_definition_once(key, opsys_defines, "O") or + find_definition_once(key, common_defines, "C")) + +################################################################ +# Makefile generation + +def construct_definition(opsys, key_prefix, value_prefix, key, definitions): + values = definitions.get(key) + if not values: + return "" + if key in ["INC", "DEF"]: + values = [patch_path_separator(opsys, value) + for value in values] + lines = ["\t{}{} \\".format(value_prefix, value) for value in values] + return "{}_{} = \\\n{}\n\t# empty\n".format(key_prefix, + key, + '\n'.join(lines)) + +def write_define(opsys, define, defines, makefile): + value = find_definition(define, defines) + if value: + if define in ["FREERTOS", "PROOFS"]: + value = os.path.abspath(value[0]) + makefile.write("{} = {}\n".format(define, value)) + +def write_common_defines(opsys, defines, makefile): + common_defines, opsys_defines, harness_defines = defines + + for key_prefix, defines in zip(["C", "O", "H"], + [common_defines, + opsys_defines, + harness_defines]): + for value_prefix, key in zip([platform_definitions[opsys]["include"], + platform_definitions[opsys]["define"], + "", ""], + ["INC", "DEF", "OPT", "CBMCFLAGS"]): + define = construct_definition(opsys, + key_prefix, value_prefix, + key, defines) + if define: + makefile.write(define + "\n") + + +def write_makefile(opsys, template, defines, makefile): + with open(template) as _template: + for line in _template: + line = patch_path_separator(opsys, line) + keys = re.findall('@(\w+)@', line) + values = [find_definition(key, defines) for key in keys] + for key, value in zip(keys, values): + if value is not None: + line = line.replace('@{}@'.format(key), " ".join(value)) + line = patch_compile_output(opsys, line, key, value) + makefile.write(line) + +def write_cbmcbatchyaml_target(opsys, _makefile): + target = """ +################################################################ +# Build configuration file to run cbmc under cbmc-batch in CI + +define encode_options +'=$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')=' +endef + +cbmc-batch.yaml: + @echo "Building $@" + @$(RM) $@ + @echo "jobos: ubuntu16" >> $@ + @echo "cbmcflags: $(call encode_options,$(CBMCFLAGS) --unwinding-assertions)" >> $@ + @echo "goto: $(ENTRY).goto" >> $@ + @echo "expected: $(H_EXPECTED)" >> $@ + +################################################################ +""" + if opsys != "windows": + _makefile.write(target) + +def makefile_from_template(opsys, template, defines, makefile="Makefile"): + with open(makefile, "w") as _makefile: + write_define(opsys, "FREERTOS", defines, _makefile) + write_define(opsys, "PROOFS", defines, _makefile) + write_common_defines(opsys, defines, _makefile) + write_makefile(opsys, template, defines, _makefile) + write_cbmcbatchyaml_target(opsys, _makefile) + +################################################################ +# Main + +def main(): + args = get_arguments() + + common_defines = read_variable_definitions("MakefileCommon.json") + opsys_defines = read_variable_definitions("MakefileWindows.json" + if args.system == "windows" + else "MakefileLinux.json") + harness_defines = {} + + makefile_from_template(args.system, + "Makefile.template", + (common_defines, opsys_defines, harness_defines), + "Makefile.common") + +if __name__ == "__main__": + main() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_configuration_directories.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_configuration_directories.py new file mode 100755 index 000000000..9e006e9ed --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_configuration_directories.py @@ -0,0 +1,163 @@ +#!/usr/bin/env python3 +# +# Creating the CBMC proofs from Configurations.json. +# +# Copyright (C) 2019 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. + +import collections +import json +import logging +import os +import pathlib +import shutil +import textwrap + +from make_proof_makefiles import load_json_config_file + +LOGGER = logging.getLogger("ComputeConfigurations") + +def prolog(): + return textwrap.dedent("""\ + This script Generates Makefile.json from Configrations.json. + + Starting in the current directory, it walks down every subdirectory + looking for Configurations.json files. Every found Configurations.json + file is assumed to look similar to the following format: + + { + "ENTRY": "ARPProcessPacket", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/lib/FreeRTOS-Plus-TCP/source/FreeRTOS_ARP.goto" + ], + "DEF": + [ + {"disableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=0"]}, + {"enableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=1"]} + ] + } + + The format is mainly taken from the Makefile.json files. + The only difference is that it expects a list of json object in the DEF + section. This script will generate a Makefile.json in a subdirectory and + copy the harness to each subdirectory. + The key is later taken as the name for the configuration subdirectory + prexied by 'config_'. + + So for the above script, we get two subdirectories: + -config_disableClashDetection + -config_enableClashDetection + + As an example, the resulting Makefile.json for the + config_disableClashDetection directory will be: + + { + "ENTRY": "ARPProcessPacket", + "CBMCFLAGS": [ + "--unwind 1", + "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17", + "--nondet-static" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/lib/FreeRTOS-Plus-TCP/source/FreeRTOS_ARP.goto" + ], + "DEF": [ + "ipconfigARP_USE_CLASH_DETECTION=0" + ] + } + + These Makefile.json files then can be turned into Makefiles for running + the proof by executing the make-proof-makefiles.py script. + """) + + +def process(folder, files): + json_content = load_json_config_file(os.path.join(folder, + "Configurations.json")) + try: + def_list = json_content["DEF"] + except KeyError: + LOGGER.error("Expected DEF as key in a Configurations.json files.") + return + for config in def_list: + logging.debug(config) + try: + configname = [name for name in config.keys() + if name != "EXPECTED"][0] + configbody = config[configname] + except (AttributeError, IndexError) as e: + LOGGER.error(e) + LOGGER.error(textwrap.dedent("""\ + The expected layout for an entry in the Configurations.json + file is a dictonary. Here is an example of the expected format: + + "DEF": + [ + {"disableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=0"]}, + {"enableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=1"]} + ] + """)) + LOGGER.error("The offending entry is %s", config) + return + new_config_folder = os.path.join(folder, "config_" + configname) + pathlib.Path(new_config_folder).mkdir(exist_ok=True, parents=True) + harness_copied = False + for file in files: + if file.endswith("harness.c"): + shutil.copy(os.path.join(folder, file), + os.path.join(new_config_folder, file)) + harness_copied = True + + if not harness_copied: + LOGGER.error("Could not find a harness in folder %s.", folder) + LOGGER.error("This folder is not processed do the end!") + return + # The order of keys must be maintained as otherwise the + # make_proof_makefiles script might fail. + current_config = collections.OrderedDict(json_content) + current_config["DEF"] = configbody + if "EXPECTED" in config.keys(): + current_config["EXPECTED"] = config["EXPECTED"] + else: + current_config["EXPECTED"] = True + with open(os.path.join(new_config_folder, "Makefile.json"), + "w") as output_file: + json.dump(current_config, output_file, indent=2) + + +def main(): + for fldr, _, fyles in os.walk("."): + if "Configurations.json" in fyles: + process(fldr, fyles) + + +if __name__ == '__main__': + logging.basicConfig(format="{script}: %(levelname)s %(message)s".format( + script=os.path.basename(__file__))) + main() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_proof_makefiles.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_proof_makefiles.py new file mode 100755 index 000000000..846942ee4 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_proof_makefiles.py @@ -0,0 +1,416 @@ +#!/usr/bin/env python3 +# +# Generation of Makefiles for CBMC proofs. +# +# Copyright (C) 2019 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. + + +import argparse +import ast +import collections +import json +import logging +import operator +import os +import os.path +import platform +import re +import sys +import textwrap +import traceback + + +# ______________________________________________________________________________ +# Compatibility between different python versions +# `````````````````````````````````````````````````````````````````````````````` + +# Python 3 doesn't have basestring +try: + basestring +except NameError: + basestring = str + +# ast.Num was deprecated in python 3.8 +_plat = platform.python_version().split(".") +if _plat[0] == "3" and int(_plat[1]) > 7: + ast_num = ast.Constant +else: + ast_num = ast.Num +# ______________________________________________________________________________ + + +def prolog(): + return textwrap.dedent("""\ + This script generates Makefiles that can be used either on Windows (with + NMake) or Linux (with GNU Make). The Makefiles consist only of variable + definitions; they are intended to be used with a common Makefile that + defines the actual rules. + + The Makefiles are generated from JSON specifications. These are simple + key-value dicts, but can contain variables and computation, as + well as comments (lines whose first character is "#"). If the + JSON file contains the following information: + + { + # 'T was brillig, and the slithy toves + "FOO": "BAR", + "BAZ": "{FOO}", + + # Did gyre and gimble in the wabe; + "QUUX": 30 + "XYZZY": "__eval 5 if {QUUZ} < 5 else min({QUUX}, 60)" + } + + then the resulting Makefile will look like + + H_FOO = BAR + H_BAZ = BAR + H_QUUX = 30 + H_XYZZY = 30 + + The language used for evaluation is highly restricted; arbitrary + python is not allowed. JSON values that are lists will be + joined with whitespace: + + { "FOO": ["BAR", "BAZ", "QUX"] } + + -> + + H_FOO = BAR BAZ QUX + + As a special case, if a key is equal to "DEF", "INC" (and maybe more, + read the code) the list of values is treated as a list of defines or + include paths. Thus, they have -D or /D, or -I or /I, prepended to them + as appropriate for the platform. + + + { "DEF": ["DEBUG", "FOO=BAR"] } + + on Linux -> + + H_DEF = -DDEBUG -DFOO=BAR + + Pathnames are written with a forward slash in the JSON file. In + each value, all slashes are replaced with backslashes if + generating Makefiles for Windows. If you wish to generate a + slash even on Windows, use two slashes---that will be changed + into a single forward slash on both Windows and Linux. + + { + "INC": [ "my/cool/directory" ], + "DEF": [ "HALF=//2" ] + } + + On Windows -> + + H_INC = /Imy\cool\directory + H_DEF = /DHALF=/2 + + When invoked, this script walks the directory tree looking for files + called "Makefile.json". It reads that file and dumps a Makefile in that + same directory. We assume that this script lives in the same directory + as a Makefile called "Makefile.common", which contains the actual Make + rules. The final line of each of the generated Makefiles will be an + include statement, including Makefile.common. + """) + +def load_json_config_file(file): + with open(file) as handle: + lines = handle.read().splitlines() + no_comments = "\n".join([line for line in lines + if line and not line.lstrip().startswith("#")]) + try: + data = json.loads(no_comments, + object_pairs_hook=collections.OrderedDict) + except json.decoder.JSONDecodeError: + traceback.print_exc() + logging.error("parsing file %s", file) + sys.exit(1) + return data + + +def dump_makefile(dyr, system): + data = load_json_config_file(os.path.join(dyr, "Makefile.json")) + + makefile = collections.OrderedDict() + + # Makefile.common expects a variable called OBJS_EXCEPT_HARNESS to be + # set to a list of all the object files except the harness. + if "OBJS" not in data: + logging.error( + "Expected a list of object files in %s/Makefile.json" % dyr) + exit(1) + makefile["OBJS_EXCEPT_HARNESS"] = " ".join( + o for o in data["OBJS"] if not o.endswith("_harness.goto")) + + so_far = collections.OrderedDict() + for name, value in data.items(): + if isinstance(value, list): + new_value = [] + for item in value: + new_value.append(compute(item, so_far, system, name, dyr, True)) + makefile[name] = " ".join(new_value) + else: + makefile[name] = compute(value, so_far, system, name, dyr) + + if (("EXPECTED" not in makefile.keys()) or + str(makefile["EXPECTED"]).lower() == "true"): + makefile["EXPECTED"] = "SUCCESSFUL" + elif str(makefile["EXPECTED"]).lower() == "false": + makefile["EXPECTED"] = "FAILURE" + makefile = ["H_%s = %s" % (k, v) for k, v in makefile.items()] + + # Deal with the case of a harness being nested several levels under + # the top-level proof directory, where the common Makefile lives + common_dir_path = "..%s" % _platform_choices[system]["path-sep"] + common_dir_path = common_dir_path * len(dyr.split(os.path.sep)[1:]) + + with open(os.path.join(dyr, "Makefile"), "w") as handle: + handle.write(("""{contents} + +{include} {common_dir_path}Makefile.common""").format( + contents="\n".join(makefile), + include=_platform_choices[system]["makefile-inc"], + common_dir_path=common_dir_path)) + + +def compute(value, so_far, system, key, harness, appending=False): + if not isinstance(value, (basestring, float, int)): + logging.error(wrap("""\ + in file %s, the key '%s' has value '%s', + which is of the wrong type (%s)"""), + os.path.join(harness, "Makefile.json"), key, + str(value), str(type(value))) + exit(1) + + value = str(value) + try: + var_subbed = value.format(**so_far) + except KeyError as e: + logging.error(wrap("""\ + in file %s, the key '%s' has value '%s', which + contains the variable %s, but that variable has + not previously been set in the file"""), + os.path.join(harness, "Makefile.json"), key, + value, str(e)) + exit(1) + + if var_subbed[:len("__eval")] != "__eval": + tmp = re.sub("//", "__DOUBLE_SLASH__", var_subbed) + tmp = re.sub("/", _platform_choices[system]["path-sep-re"], tmp) + evaluated = re.sub("__DOUBLE_SLASH__", "/", tmp) + else: + to_eval = var_subbed[len("__eval"):].strip() + logging.debug("About to evaluate '%s'", to_eval) + evaluated = eval_expr(to_eval, + os.path.join(harness, "Makefile.json"), + key, value) + + if key == "DEF": + final_value = "%s%s" % (_platform_choices[system]["define"], + evaluated) + elif key == "INC": + final_value = "%s%s" % (_platform_choices[system]["include"], + evaluated) + else: + final_value = evaluated + + # Allow this value to be used for future variable substitution + if appending: + try: + so_far[key] = "%s %s" % (so_far[key], final_value) + except KeyError: + so_far[key] = final_value + logging.debug("Appending final value '%s' to key '%s'", + final_value, key) + else: + so_far[key] = final_value + logging.info("Key '%s' set to final value '%s'", key, final_value) + + return final_value + + +def eval_expr(expr_string, harness, key, value): + """ + Safe evaluation of purely arithmetic expressions + """ + try: + tree = ast.parse(expr_string, mode="eval").body + except SyntaxError: + traceback.print_exc() + logging.error(wrap("""\ + in file %s at key '%s', value '%s' contained the expression + '%s' which is an invalid expression"""), harness, key, + value, expr_string) + exit(1) + + def eval_single_node(node): + logging.debug(node) + if isinstance(node, ast_num): + return node.n + # We're only doing IfExp, which is Python's ternary operator + # (i.e. it's an expression). NOT If, which is a statement. + if isinstance(node, ast.IfExp): + # Let's be strict and only allow actual booleans in the guard + guard = eval_single_node(node.test) + if guard is not True and guard is not False: + logging.error(wrap("""\ + in file %s at key '%s', there was an invalid guard + for an if statement."""), harness, key) + exit(1) + if guard: + return eval_single_node(node.body) + return eval_single_node(node.orelse) + if isinstance(node, ast.Compare): + left = eval_single_node(node.left) + # Don't allow expressions like (a < b) < c + right = eval_single_node(node.comparators[0]) + op = eval_single_node(node.ops[0]) + return op(left, right) + if isinstance(node, ast.BinOp): + left = eval_single_node(node.left) + right = eval_single_node(node.right) + op = eval_single_node(node.op) + return op(left, right) + if isinstance(node, ast.Call): + valid_calls = { + "max": max, + "min": min, + } + if node.func.id not in valid_calls: + logging.error(wrap("""\ + in file %s at key '%s', there was an invalid + call to %s()"""), harness, key, node.func.id) + exit(1) + left = eval_single_node(node.args[0]) + right = eval_single_node(node.args[1]) + return valid_calls[node.func.id](left, right) + try: + return { + ast.Eq: operator.eq, + ast.NotEq: operator.ne, + ast.Lt: operator.lt, + ast.LtE: operator.le, + ast.Gt: operator.gt, + ast.GtE: operator.ge, + + ast.Add: operator.add, + ast.Sub: operator.sub, + ast.Mult: operator.mul, + # Use floordiv (i.e. //) so that we never need to + # cast to an int + ast.Div: operator.floordiv, + }[type(node)] + except KeyError: + logging.error(wrap("""\ + in file %s at key '%s', there was expression that + was impossible to evaluate"""), harness, key) + exit(1) + + return eval_single_node(tree) + + +_platform_choices = { + "linux": { + "platform": "linux", + "path-sep": "/", + "path-sep-re": "/", + "define": "-D", + "include": "-I", + "makefile-inc": "include", + }, + "windows": { + "platform": "win32", + "path-sep": "\\", + "path-sep-re": re.escape("\\"), + "define": "/D", + "include": "/I", + "makefile-inc": "!INCLUDE", + }, +} +# Assuming macos is the same as linux +_mac_os = dict(_platform_choices["linux"]) +_mac_os["platform"] = "darwin" +_platform_choices["macos"] = _mac_os + + +def default_platform(): + for arg_string, os_data in _platform_choices.items(): + if sys.platform == os_data["platform"]: + return arg_string + return "linux" + + +_args = [{ + "flags": ["-s", "--system"], + "metavar": "OS", + "choices": _platform_choices, + "default": str(default_platform()), + "help": textwrap.dedent("""\ + which operating system to generate makefiles for. + Defaults to the current platform (%(default)s); + choices are {choices}""").format( + choices="[%s]" % ", ".join(_platform_choices)), +}, { + "flags": ["-v", "--verbose"], + "help": "verbose output", + "action": "store_true", +}, { + "flags": ["-w", "--very-verbose"], + "help": "very verbose output", + "action": "store_true", + }] + + +def get_args(): + pars = argparse.ArgumentParser( + description=prolog(), + formatter_class=argparse.RawDescriptionHelpFormatter) + for arg in _args: + flags = arg.pop("flags") + pars.add_argument(*flags, **arg) + return pars.parse_args() + + +def set_up_logging(args): + fmt = "{script}: %(levelname)s %(message)s".format( + script=os.path.basename(__file__)) + if args.very_verbose: + logging.basicConfig(format=fmt, level=logging.DEBUG) + elif args.verbose: + logging.basicConfig(format=fmt, level=logging.INFO) + else: + logging.basicConfig(format=fmt, level=logging.WARNING) + +def wrap(string): + return re.sub(r"\s+", " ", re.sub("\n", " ", string)) + +def main(): + args = get_args() + set_up_logging(args) + + for root, _, fyles in os.walk("."): + if "Makefile.json" in fyles: + dump_makefile(root, args.system) + + +if __name__ == "__main__": + main() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_remove_makefiles.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_remove_makefiles.py new file mode 100755 index 000000000..12d0c72f1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_remove_makefiles.py @@ -0,0 +1,48 @@ +#!/usr/bin/env python3 +# +# Removing the generated Makefiles and cbmc-batch.yaml files. +# +# Copyright (C) 2019 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. + +import os + +from make_cbmc_batch_files import remove_cbmc_yaml_files + +def main(): + try: + os.remove("Makefile.common") + except FileNotFoundError: + pass + + for root, _, files in os.walk("."): + # We do not want to remove hand-written Makefiles, so + # only remove Makefiles that are in the same directory as + # a Makefile.json. Such Makefiles are generated from the + # JSON file. + if "Makefile.json" in files: + try: + os.remove(os.path.join(root, "Makefile")) + except FileNotFoundError: + pass + +if __name__ == "__main__": + remove_cbmc_yaml_files() + main() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_type_header_files.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_type_header_files.py new file mode 100755 index 000000000..a8ac66384 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_type_header_files.py @@ -0,0 +1,162 @@ +#!/usr/bin/env python3 +# +# Compute type header files for c modules +# +# Copyright (C) 2019 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. + + +import argparse +import logging +import os +import re +import shutil +import subprocess +import sys +from tempfile import TemporaryDirectory + +def epilog(): + return """\ + This program dumps a header file containing the types and macros + contained in the C file passed as input. It uses `goto-instrument` + from the CBMC tool suite instead of the preprocessor, to dump types + and other constructs as well as preprocessor directives. + + This program should be used in cases where types or macros declared + for internal use in a C file use are needed to write a test harness + or CBMC proof. The intention is that the build process will run + this program to dump the header file, and the proof will #include + the header. + """ + +_DEFINE_REGEX_HEADER = re.compile(r"\s*#\s*define\s*([\w]+)") + + +def get_module_name(fyle): + base = os.path.basename(fyle) + return base.split(".")[0] + + +def collect_defines(fyle): + collector_result = "" + continue_define = False + in_potential_def_scope = "" + potential_define = False + potential_define_confirmed = False + with open(fyle) as in_file: + for line in in_file: + matched = _DEFINE_REGEX_HEADER.match(line) + if line.strip().startswith("#if"): + potential_define = True + in_potential_def_scope += line + elif line.strip().startswith("#endif") and potential_define: + if potential_define_confirmed: + in_potential_def_scope += line + collector_result += in_potential_def_scope + in_potential_def_scope = "" + potential_define = False + potential_define_confirmed = False + elif matched and potential_define: + potential_define_confirmed = True + in_potential_def_scope += line + elif matched or continue_define: + continue_define = line.strip("\n").endswith("\\") + collector_result += line + elif potential_define: + in_potential_def_scope += line + return collector_result + + +def make_header_file(goto_binary, fyle, target_folder): + fyle = os.path.normpath(fyle) + with TemporaryDirectory() as tmpdir: + module = get_module_name(fyle) + header_file = "{}_datastructure.h".format(module) + + drop_header_cmd = ["goto-instrument", + "--dump-c-type-header", + module, + goto_binary, + header_file] + res = subprocess.run(drop_header_cmd, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + universal_newlines=True, + cwd=tmpdir) + if res.returncode: + logging.error("Dumping type header for file '%s' failed", fyle) + logging.error("The command `%s` returned %s", + drop_header_cmd, + res.stdout) + logging.error("The return code is %d", int(res.returncode)) + sys.exit(1) + + header = os.path.normpath(os.path.join(tmpdir, header_file)) + collected = collect_defines(fyle) + logging.debug("Dumping the following header file to '%s':\n%s\n" + "// END GENERATED HEADER FILE", header, collected) + with open(header, "a") as out: + print(collected, file=out) + + target_file = os.path.normpath(os.path.join(target_folder, header_file)) + shutil.move(header, target_file) + + +_ARGS = [{ + "flags": ["--c-file"], + "metavar": "F", + "help": "source file to extract types and headers from", + "required": True +}, { + "flags": ["--binary"], + "metavar": "B", + "help": "file compiled from the source file with CBMC's goto-cc compiler", + "required": True +}, { + "flags": ["--out-dir"], + "metavar": "D", + "help": ("directory to write the generated header file to " + "(default: %(default)s)"), + "default": os.path.abspath(os.getcwd()), +}, { + "flags": ["--verbose", "-v"], + "help": "verbose output", + "action": "store_true" +}] + + +if __name__ == '__main__': + pars = argparse.ArgumentParser( + epilog=epilog(), + description="Dump a C file's types and macros to a separate file") + for arg in _ARGS: + flags = arg.pop("flags") + pars.add_argument(*flags, **arg) + + args = pars.parse_args() + + fmt = "{script}: %(levelname)s %(message)s".format( + script=os.path.basename(__file__)) + if args.verbose: + logging.basicConfig(format=fmt, level=logging.DEBUG) + else: + logging.basicConfig(format=fmt, level=logging.INFO) + + make_header_file(args.binary, args.c_file, args.out_dir) diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ninja.py b/FreeRTOS-Plus/Test/CBMC/proofs/ninja.py new file mode 100755 index 000000000..4bfd3c8d4 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ninja.py @@ -0,0 +1,219 @@ +#!/usr/bin/env python3 + +""" +Write a ninja build file to generate reports for cbmc proofs. + +Given a list of folders containing cbmc proofs, write a ninja build +file the generate reports for these proofs. The list of folders may +be given on the command line, in a json file, or found in the file +system. +""" + +# Add task pool + +import sys +import os +import platform +import argparse +import json + +################################################################ +# The command line parser + +def argument_parser(): + """Return the command line parser.""" + + parser = argparse.ArgumentParser( + description='Generate ninja build file for cbmc proofs.', + epilog=""" + Given a list of folders containing cbmc proofs, write a ninja build + file the generate reports for these proofs. The list of folders may + be given on the command line, in a json file, or found in the file + system. + In the json file, there should be a dict mapping the key "proofs" + to a list of folders containing proofs. + The file system, all folders folders under the current directory + containing a file named 'cbmc-batch.yaml' is considered a + proof folder. + This script assumes that the proof is driven by a Makefile + with targets goto, cbmc, coverage, property, and report. + This script does not work with Windows and Visual Studio. + """ + ) + parser.add_argument('folders', metavar='PROOF', nargs='*', + help='Folder containing a cbmc proof') + parser.add_argument('--proofs', metavar='JSON', + help='Json file listing folders containing cbmc proofs') + return parser + +################################################################ +# The list of folders containing proofs +# +# The list of folders will be taken from +# 1. the list PROOFS defined here or +# 2. the command line +# 3. the json file specified on the command line containing a +# dict mapping the key JSON_KEY to a list of folders +# 4. the folders below the current directory containing +# a file named FS_KEY +# + +PROOFS = [ +] + +JSON_KEY = 'proofs' +FS_KEY = 'cbmc-batch.yaml' + +def find_proofs_in_json_file(filename): + """Read the list of folders containing proofs from a json file.""" + + if not filename: + return [] + try: + with open(filename) as proofs: + return json.load(proofs)[JSON_KEY] + except (FileNotFoundError, KeyError): + raise UserWarning("Can't find key {} in json file {}".format(JSON_KEY, filename)) + except json.decoder.JSONDecodeError: + raise UserWarning("Can't parse json file {}".format(filename)) + +def find_proofs_in_filesystem(): + """Locate the folders containing proofs in the filesystem.""" + + proofs = [] + for root, _, files in os.walk('.'): + if FS_KEY in files: + proofs.append(os.path.normpath(root)) + return proofs + +################################################################ +# The strings used to write sections of the ninja file + +NINJA_RULES = """ +################################################################ +# task pool to force sequential builds of goto binaries + +pool goto_pool + depth = 1 + +################################################################ +# proof target rules + +rule build_goto + command = make -C ${folder} goto + pool = goto_pool + +rule build_cbmc + command = make -C ${folder} cbmc + +rule build_coverage + command = make -C ${folder} coverage + +rule build_property + command = make -C ${folder} property + +rule build_report + command = make -C ${folder} report + +rule clean_folder + command = make -C ${folder} clean + +rule veryclean_folder + command = make -C ${folder} veryclean + +rule open_proof + command = open ${folder}/html/index.html + +""" + +NINJA_BUILDS = """ +################################################################ +# {folder} proof targets + +build {folder}/{entry}.goto: build_goto + folder={folder} + +build {folder}/cbmc.txt: build_cbmc {folder}/{entry}.goto + folder={folder} + +build {folder}/coverage.xml: build_coverage {folder}/{entry}.goto + folder={folder} + +build {folder}/property.xml: build_property {folder}/{entry}.goto + folder={folder} + +build {folder}/html/index.html: build_report {folder}/{entry}.goto {folder}/cbmc.txt {folder}/coverage.xml {folder}/property.xml + folder={folder} + +build clean_{folder}: clean_folder + folder={folder} + +build veryclean_{folder}: veryclean_folder + folder={folder} + +build open_{folder}: open_proof + folder={folder} + +build {folder}: phony {folder}/html/index.html + +default {folder} + +""" + +NINJA_GLOBALS = """ +################################################################ +# global targets + +build clean: phony {clean_targets} + +build veryclean: phony {veryclean_targets} + +build open: phony {open_targets} +""" + +################################################################ +# The main function + +def get_entry(folder): + """Find the name of the proof in the proof Makefile.""" + + with open('{}/Makefile'.format(folder)) as makefile: + for line in makefile: + if line.strip().lower().startswith('entry'): + return line[line.find('=')+1:].strip() + if line.strip().lower().startswith('h_entry'): + return line[line.find('=')+1:].strip() + raise UserWarning("Can't find ENTRY in {}/Makefile".format(folder)) + +def write_ninja_build_file(): + """Write a ninja build file to generate proof results.""" + + if platform.system().lower() == 'windows': + print("This script does not run on Windows.") + sys.exit() + + args = argument_parser().parse_args() + + proofs = (PROOFS or + args.folders or + find_proofs_in_json_file(args.proofs) or + find_proofs_in_filesystem()) + + with open('build.ninja', 'w') as ninja: + ninja.write(NINJA_RULES) + for proof in proofs: + entry = get_entry(proof) + ninja.write(NINJA_BUILDS.format(folder=proof, entry=entry)) + targets = lambda kind, folders: ' '.join( + ['{}_{}'.format(kind, folder) for folder in folders] + ) + ninja.write(NINJA_GLOBALS.format( + clean_targets=targets('clean', proofs), + veryclean_targets=targets('veryclean', proofs), + open_targets=targets('open', proofs) + )) + +################################################################ + +if __name__ == "__main__": + write_ninja_build_file() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json new file mode 100644 index 000000000..9ad1ef4e9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json @@ -0,0 +1,21 @@ +{ + "ENTRY": "ProcessIPPacket", + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto" + ], + "DEF": + [ + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c new file mode 100644 index 000000000..def244a51 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c @@ -0,0 +1,29 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" + +/* proof is done separately */ +BaseType_t xProcessReceivedTCPPacket(NetworkBufferDescriptor_t *pxNetworkBuffer) { } + +/* proof is done separately */ +BaseType_t xProcessReceivedUDPPacket(NetworkBufferDescriptor_t *pxNetworkBuffer, uint16_t usPort) { } + +/* This proof was done before. Hence we assume it to be correct here. */ +void vARPRefreshCacheEntry( const MACAddress_t * pxMACAddress, const uint32_t ulIPAddress ) { } + +eFrameProcessingResult_t publicProcessIPPacket( IPPacket_t * const pxIPPacket, NetworkBufferDescriptor_t * const pxNetworkBuffer); + +void harness() { + + NetworkBufferDescriptor_t * const pxNetworkBuffer = malloc(sizeof(NetworkBufferDescriptor_t)); + /* Pointer to the start of the Ethernet frame. It should be able to access the whole Ethernet frame.*/ + pxNetworkBuffer->pucEthernetBuffer = malloc(ipTOTAL_ETHERNET_FRAME_SIZE); + /* Minimum length of the pxNetworkBuffer->xDataLength is at least the size of the IPPacket_t. */ + __CPROVER_assume(pxNetworkBuffer->xDataLength >= sizeof(IPPacket_t) && pxNetworkBuffer->xDataLength <= ipTOTAL_ETHERNET_FRAME_SIZE); + IPPacket_t * const pxIPPacket = malloc(sizeof(IPPacket_t)); + publicProcessIPPacket(pxIPPacket, pxNetworkBuffer); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json new file mode 100644 index 000000000..901a72729 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json @@ -0,0 +1,31 @@ +{ + "ENTRY": "ProcessReceivedTCPPacket", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvTCPSendRepeated.0:13", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto" + ], + "INSTFLAGS": + [ + "--remove-function-body prvSingleStepTCPHeaderOptions", + "--remove-function-body prvCheckOptions", + "--remove-function-body prvTCPPrepareSend", + "--remove-function-body prvTCPReturnPacket", + "--remove-function-body prvTCPHandleState" + ], + "DEF": + [ + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} + diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c new file mode 100644 index 000000000..bf84ecf05 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c @@ -0,0 +1,62 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_TCP_IP.h" +#include "FreeRTOS_Stream_Buffer.h" + +/* This proof assumes FreeRTOS_socket, pxTCPSocketLookup and +pxGetNetworkBufferWithDescriptor are implemented correctly. + +It also assumes prvSingleStepTCPHeaderOptions, prvCheckOptions, prvTCPPrepareSend, +prvTCPHandleState and prvTCPReturnPacket are correct. These functions are +proved to be correct separately. */ + +/* Implementation of safe malloc */ +void *safeMalloc(size_t xWantedSize ){ + if(xWantedSize == 0){ + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +/* Abstraction of FreeRTOS_socket */ +Socket_t FreeRTOS_socket( BaseType_t xDomain, BaseType_t xType, BaseType_t xProtocol) { + return safeMalloc(sizeof(FreeRTOS_Socket_t)); +} + +/* Abstraction of pxTCPSocketLookup */ +FreeRTOS_Socket_t *pxTCPSocketLookup(uint32_t ulLocalIP, UBaseType_t uxLocalPort, uint32_t ulRemoteIP, UBaseType_t uxRemotePort) { + FreeRTOS_Socket_t * xRetSocket = safeMalloc(sizeof(FreeRTOS_Socket_t)); + if (xRetSocket) { + xRetSocket->u.xTCP.txStream = safeMalloc(sizeof(StreamBuffer_t)); + xRetSocket->u.xTCP.pxPeerSocket = safeMalloc(sizeof(StreamBuffer_t)); + } + return xRetSocket; +} + +/* Abstraction of pxGetNetworkBufferWithDescriptor */ +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + NetworkBufferDescriptor_t *pxNetworkBuffer = safeMalloc(sizeof(NetworkBufferDescriptor_t)); + if(pxNetworkBuffer) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(xRequestedSizeBytes); + __CPROVER_assume(pxNetworkBuffer->xDataLength == ipSIZE_OF_ETH_HEADER + sizeof(int32_t)); + } + return pxNetworkBuffer; +} + +void harness() { + NetworkBufferDescriptor_t *pxNetworkBuffer = safeMalloc(sizeof(NetworkBufferDescriptor_t)); + if (pxNetworkBuffer) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(TCPPacket_t)); + } + if (pxNetworkBuffer && pxNetworkBuffer->pucEthernetBuffer) { + xProcessReceivedTCPPacket(pxNetworkBuffer); + + } + +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json new file mode 100644 index 000000000..017f625f0 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json @@ -0,0 +1,23 @@ +{ + "ENTRY": "ProcessReceivedUDPPacket", + "MAX_RX_PACKETS":1, + "USE_LLMNR":1, + "USE_NBNS":1, + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_UDP_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto" + ], + "DEF": + [ + "ipconfigUDP_MAX_RX_PACKETS={MAX_RX_PACKETS}", + "ipconfigUSE_LLMNR={USE_LLMNR}", + "ipconfigUSE_NBNS={USE_NBNS}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c new file mode 100644 index 000000000..0082e5d61 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c @@ -0,0 +1,46 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_TCP_IP.h" + +/*This proof assumes that pxUDPSocketLookup is implemented correctly. */ + +/* This proof was done before. Hence we assume it to be correct here. */ +void vARPRefreshCacheEntry(const MACAddress_t * pxMACAddress, const uint32_t ulIPAddress) { } + +/* This proof was done before. Hence we assume it to be correct here. */ +BaseType_t xIsDHCPSocket(Socket_t xSocket) { } + +/* This proof was done before. Hence we assume it to be correct here. */ +uint32_t ulDNSHandlePacket(NetworkBufferDescriptor_t *pxNetworkBuffer) { } + +/* Implementation of safe malloc */ +void *safeMalloc(size_t xWantedSize) { + if(xWantedSize == 0) { + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +/* Abstraction of pxUDPSocketLookup */ +FreeRTOS_Socket_t *pxUDPSocketLookup( UBaseType_t uxLocalPort ) { + return safeMalloc(sizeof(FreeRTOS_Socket_t)); +} + +void harness() { + NetworkBufferDescriptor_t *pxNetworkBuffer = safeMalloc(sizeof(NetworkBufferDescriptor_t)); + if(pxNetworkBuffer) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(UDPPacket_t)); + } + uint16_t usPort; + if (pxNetworkBuffer && pxNetworkBuffer->pucEthernetBuffer) { + xProcessReceivedUDPPacket(pxNetworkBuffer, usPort); + } +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/prepare.py b/FreeRTOS-Plus/Test/CBMC/proofs/prepare.py new file mode 100755 index 000000000..58f9903db --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/prepare.py @@ -0,0 +1,115 @@ +#!/usr/bin/env python3 +# +# Python script for preparing the code base for the CBMC proofs. +# +# Copyright (C) 2019 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. + +import logging +import os +import sys +import textwrap +from subprocess import CalledProcessError + +from make_common_makefile import main as make_common_file +from make_configuration_directories import main as process_configurations +from make_proof_makefiles import main as make_proof_files +from make_cbmc_batch_files import create_cbmc_yaml_files + +CWD = os.getcwd() +sys.path.append(os.path.normpath(os.path.join(CWD, "..", "patches"))) + +#from compute_patch import create_patches +#from compute_patch import DirtyGitError +#from compute_patch import PatchCreationError +from patches_constants import HEADERS + +from compute_patch import find_all_defines +from compute_patch import manipulate_headerfile + +import patch + +PROOFS_DIR = os.path.dirname(os.path.abspath(__file__)) + +LOGGER = logging.getLogger("PrepareLogger") + +################################################################ + +def patch_headers(headers): + """Patch headers so we can define symbols on the command line. + + When building for CBMC, it is convenient to define symbols on the + command line and know that these definitions will override the + definitions of the same symbols in header files. + + The create_patches function takes a list of header files, searches + the Makefile.json files for symbols that will be defined in the + Makefiles, and creates patch files that protect the definition of + those symbols in header files with #ifndef/#endif. In this way, + command line definitions will override header file definitions. + + The create_patches function, however, depends on the fact that all + header files being modified are included in the top-level git + repository. This assumption is violated if header files live in + submodules. + + This function just updates the header files in place without + creating patch files. One potential vulnerability of this + function is that it could cause preexisting patch files to fail if + they patch a file being modified here. + """ + defines = find_all_defines() + for header in headers: + manipulate_headerfile(defines, header) + +################################################################ + +def build(): + process_configurations() + make_common_file() + make_proof_files() + try: + create_cbmc_yaml_files() + except CalledProcessError as e: + logging.error(textwrap.dedent("""\ + An error occured during cbmc-batch generation. + The error message is: {} + """.format(str(e)))) + exit(1) + + # Patch headers directly instead of creating patch files. + patch.patch() + patch_headers(HEADERS) + + #try: + # create_patches(HEADERS) + #except (DirtyGitError, PatchCreationError) as e: + # logging.error(textwrap.dedent("""\ + # An error occured during patch creation. + # The error message is: {} + # """.format(str(e)))) + # exit(1) + +################################################################ + +if __name__ == '__main__': + logging.basicConfig(format="{script}: %(levelname)s %(message)s".format( + script=os.path.basename(__file__))) + build() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c b/FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c new file mode 100644 index 000000000..6bcb9319a --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c @@ -0,0 +1,24 @@ +#define ensure_memory_is_valid( px, length ) (px != NULL) && __CPROVER_w_ok((px), length) + +/* Implementation of safe malloc which returns NULL if the requested size is 0. + Warning: The behavior of malloc(0) is platform dependent. + It is possible for malloc(0) to return an address without allocating memory.*/ +void *safeMalloc(size_t xWantedSize) { + return nondet_bool() ? malloc(xWantedSize) : NULL; +} + +/* Memory assignment for FreeRTOS_Socket_t */ +FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated () { + FreeRTOS_Socket_t *pxSocket = safeMalloc(sizeof(FreeRTOS_Socket_t)); + if (ensure_memory_is_valid(pxSocket, sizeof(FreeRTOS_Socket_t))) { + pxSocket->u.xTCP.rxStream = safeMalloc(sizeof(StreamBuffer_t)); + pxSocket->u.xTCP.txStream = safeMalloc(sizeof(StreamBuffer_t)); + pxSocket->u.xTCP.pxPeerSocket = safeMalloc(sizeof(FreeRTOS_Socket_t)); + } + return pxSocket; +} + +/* Memory assignment for FreeRTOS_Network_Buffer */ +NetworkBufferDescriptor_t * ensure_FreeRTOS_NetworkBuffer_is_allocated () { + return safeMalloc(sizeof(NetworkBufferDescriptor_t)); +} |