diff options
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC')
139 files changed, 6970 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/.gitignore b/FreeRTOS-Plus/Test/CBMC/.gitignore new file mode 100644 index 000000000..225be8104 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/.gitignore @@ -0,0 +1,5 @@ +cbmc.txt +property.xml +coverage.xml +*.goto +**/html/*
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/README.md b/FreeRTOS-Plus/Test/CBMC/README.md new file mode 100644 index 000000000..09d5e1481 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/README.md @@ -0,0 +1,133 @@ +CBMC Proof Infrastructure +========================= + +This directory contains automated proofs of the memory safety of various parts +of the FreeRTOS codebase. A continuous integration system validates every +pull request posted to the repository against these proofs, and developers can +also run the proofs on their local machines. + +The proofs are checked using the +[C Bounded Model Checker](http://www.cprover.org/cbmc/), an open-source static +analysis tool +([GitHub repository](https://github.com/diffblue/cbmc)). This README describes +how to run the proofs on your local clone of a:FR. + + +Bulding and running proofs +-------------------------- + +For historical reasons, some of the proofs are built and run using CMake +and CTest. Others use a custom python-based build system. New proofs +should use CMake. This README describes how to build and run both kinds +of proof. + + +CMake-based build +----------------- + +Follow the CBMC installation instructions below. + +Suppose that the freertos source tree is located at +`~/src/freertos` and you wish to build the proofs into +`~/build/freertos`. The following three commands build and run +the proofs: + +```sh +cmake -S~/src/freertos -B~/build/freertos -DCOMPILER=cbmc +-DBOARD=windows -DVENDOR=pc +cmake --build ~/build/freertos --target all-proofs +cd ~/build/freertos && ctest -L cbmc +``` + +Alternatively, this single command does the same thing, assuming you +have the Ninja build tool installed: + +```sh +ctest --build-and-test \ + ~/src/freertos \ + ~/build/freertos \ + --build-target cbmc \ + --build-generator Ninja \ + --build-options \ + -DCOMPILER=cbmc \ + -DBOARD=windows \ + -DVENDOR=pc \ + --test-command ctest -j4 -L cbmc --output-on-failure +``` + + + +Python-based build +------------------ + +### Prerequisites + +You will need Python 3. On Windows, you will need Visual Studio 2015 or later +(in particular, you will need the Developer Command Prompt and NMake). On macOS +and Linux, you will need Make. + + +### Installing CBMC + +- Clone the [CBMC repository](https://github.com/diffblue/cbmc). + +- The canonical compilation and installation instructions are in the + [COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md) + file in the CBMC repository; we reproduce the most important steps for + Windows users here, but refer to that document if in doubt. + - Download and install CMake from the [CMake website](https://cmake.org/download). + - Download and install the "git for Windows" package, which also + provides the `patch` command, from [here](https://git-scm.com/download/win). + - Download the flex and bison for Windows package from + [this sourceforge site](https://sourceforge.net/projects/winflexbison). + "Install" it by dropping the contents of the entire unzipped + package into the top-level CBMC source directory. + - Change into the top-level CBMC source directory and run + ``` + cmake -H. -Bbuild -DCMAKE_BUILD_TYPE=Release -DWITH_JBMC=OFF + cmake --build build + ``` + +- Ensure that you can run the programs `cbmc`, `goto-cc` (or `goto-cl` + on Windows), and `goto-instrument` from the command line. If you build + CBMC with CMake, the programs will have been installed under the + `build/bin/Debug` directory under the top-level `cbmc` directory; you + should add that directory to your `$PATH`. If you built CBMC using + Make, then those programs will have been installed in the `src/cbmc`, + `src/goto-cc`, and `src/goto-instrument` directories respectively. + + +### Setting up the proofs + +Change into the `proofs` directory. On Windows, run +``` +python prepare.py +``` +On macOS or Linux, run +``` +./prepare.py +``` +If you are on a Windows machine but want to generate Linux Makefiles (or vice +versa), you can pass the `--system linux` or `--system windows` options to those +programs. + + +### Running the proofs + +Each of the leaf directories under `proofs` is a proof of the memory +safety of a single entry point in FreeRTOS. The scripts that you ran in the +previous step will have left a Makefile in each of those directories. To +run a proof, change into the directory for that proof and run `nmake` on +Windows or `make` on Linux or macOS. The proofs may take some time to +run; they eventually write their output to `cbmc.txt`, which should have +the text `VERIFICATION SUCCESSFUL` at the end. + + +### Proof directory structure + +This directory contains the following subdirectories: + +- `proofs` contains the proofs run against each pull request +- `patches` contains a set of patches that get applied to the codebase prior to + running the proofs +- `include` and `windows` contain header files used by the proofs. diff --git a/FreeRTOS-Plus/Test/CBMC/cmake/compute-coverage.cmake b/FreeRTOS-Plus/Test/CBMC/cmake/compute-coverage.cmake new file mode 100644 index 000000000..819fa11bb --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/cmake/compute-coverage.cmake @@ -0,0 +1,14 @@ +execute_process( + COMMAND + cbmc --cover location --xml-ui + ${cbmc_flags} ${cbmc_verbosity} ${goto_binary} + OUTPUT_FILE ${out_file} + ERROR_FILE ${out_file} + RESULT_VARIABLE res +) + +if(NOT (${res} EQUAL 0 OR ${res} EQUAL 10)) + message(FATAL_ERROR + "Unexpected CBMC coverage return code '${res}' for proof ${proof_name}. Log written to ${out_file}." + ) +endif() diff --git a/FreeRTOS-Plus/Test/CBMC/cmake/compute-property.cmake b/FreeRTOS-Plus/Test/CBMC/cmake/compute-property.cmake new file mode 100644 index 000000000..3192aa99a --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/cmake/compute-property.cmake @@ -0,0 +1,14 @@ +execute_process( + COMMAND + cbmc --show-properties --unwinding-assertions --xml-ui + ${cbmc_flags} ${cbmc_verbosity} ${goto_binary} + OUTPUT_FILE ${out_file} + ERROR_FILE ${out_file} + RESULT_VARIABLE res +) + +if(NOT (${res} EQUAL 0 OR ${res} EQUAL 10)) + message(FATAL_ERROR + "Unexpected CBMC property return code '${res}' for proof ${proof_name}. Log written to ${out_file}." + ) +endif() diff --git a/FreeRTOS-Plus/Test/CBMC/cmake/model-check.cmake b/FreeRTOS-Plus/Test/CBMC/cmake/model-check.cmake new file mode 100644 index 000000000..8dc37b094 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/cmake/model-check.cmake @@ -0,0 +1,14 @@ +execute_process( + COMMAND + cbmc --trace --unwinding-assertions + ${cbmc_flags} ${cbmc_verbosity} ${goto_binary} + OUTPUT_FILE ${out_file} + ERROR_FILE ${out_file} + RESULT_VARIABLE res +) + +if(NOT (${res} EQUAL 0 OR ${res} EQUAL 10)) + message(FATAL_ERROR + "Unexpected CBMC return code '${res}' for proof ${proof_name}. Log written to ${out_file}." + ) +endif() diff --git a/FreeRTOS-Plus/Test/CBMC/include/README.md b/FreeRTOS-Plus/Test/CBMC/include/README.md new file mode 100644 index 000000000..fa317dc04 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/include/README.md @@ -0,0 +1,2 @@ +This directory contains include files used by the CBMC proofs: +* cbmc.h defines some macros used in the proof test harnesses diff --git a/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h b/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h new file mode 100644 index 000000000..22434a91c --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h @@ -0,0 +1,3 @@ +eFrameProcessingResult_t publicProcessIPPacket( IPPacket_t * const pxIPPacket, NetworkBufferDescriptor_t * const pxNetworkBuffer ) { + prvProcessIPPacket(pxIPPacket, pxNetworkBuffer); +} diff --git a/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h b/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h new file mode 100644 index 000000000..01075d2ba --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h @@ -0,0 +1,12 @@ +int32_t publicTCPPrepareSend( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer, UBaseType_t uxOptionsLength ) { + prvTCPPrepareSend( pxSocket, ppxNetworkBuffer, uxOptionsLength ); +} + +BaseType_t publicTCPHandleState( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer ) { + prvTCPHandleState(pxSocket, ppxNetworkBuffer); +} + +void publicTCPReturnPacket( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t *pxNetworkBuffer, + uint32_t ulLen, BaseType_t xReleaseAfterSend ) { + prvTCPReturnPacket(pxSocket, pxNetworkBuffer, ulLen, xReleaseAfterSend ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/include/cbmc.h b/FreeRTOS-Plus/Test/CBMC/include/cbmc.h new file mode 100644 index 000000000..c30063bae --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/include/cbmc.h @@ -0,0 +1,100 @@ +/* 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" + +/* + * CBMC models a pointer as an object id and an offset into that + * object. The top bits of a pointer encode the object id and the + * remaining bits encode the offset. This means there is a bound on + * the maximum offset into an object in CBMC, and hence a bound on the + * size of objects in CBMC. + */ +#define CBMC_BITS 7 +#define CBMC_MAX_OBJECT_SIZE ( 0xFFFFFFFF >> ( CBMC_BITS + 1 ) ) + +#define IMPLIES( a, b ) ( !( a ) || ( b ) ) + +BaseType_t nondet_basetype(); +UBaseType_t nondet_ubasetype(); +TickType_t nondet_ticktype(); +int32_t nondet_int32(); +uint32_t nondet_uint32(); +size_t nondet_sizet(); + +#define nondet_BaseType() nondet_basetype() + +void * safeMalloc( size_t size ); + + +enum CBMC_LOOP_CONDITION +{ + CBMC_LOOP_BREAK, CBMC_LOOP_CONTINUE, CBMC_LOOP_RETURN +}; + +/* CBMC specification: capture old value for precondition and */ +/* postcondition checking */ + +#define OLDVAL( var ) _old_ ## var +#define SAVE_OLDVAL( var, typ ) const typ OLDVAL( var ) = var + +/* CBMC specification: capture old value for values passed by */ +/* reference in function abstractions */ + +#define OBJ( var ) ( * var ) +#define OLDOBJ( var ) _oldobj_ ## var +#define SAVE_OLDOBJ( var, typ ) const typ OLDOBJ( var ) = OBJ( var ) + +/* CBMC debugging: printfs for expressions */ + +#define __CPROVER_printf( var ) { uint32_t ValueOf_ ## var = ( uint32_t ) var; } +#define __CPROVER_printf2( str, exp ) { uint32_t ValueOf_ ## str = ( uint32_t ) ( exp ); } + +/* CBMC debugging: printfs for pointer expressions */ + +#define __CPROVER_printf_ptr( var ) { uint8_t * ValueOf_ ## var = ( uint8_t * ) var; } +#define __CPROVER_printf2_ptr( str, exp ) { uint8_t * ValueOf_ ## str = ( uint8_t * ) ( exp ); } + +/* + * An assertion that pvPortMalloc returns NULL when asked to allocate 0 bytes. + * This assertion is used in some of the TaskPool proofs. + */ +#define __CPROVER_assert_zero_allocation() \ + __CPROVER_assert( pvPortMalloc( 0 ) == NULL, \ + "pvPortMalloc allows zero-allocated memory." ) + +/* + * A stub for pvPortMalloc that nondeterministically chooses to return + * either NULL or an allocation of the requested space. The stub is + * guaranteed to return NULL when asked to allocate 0 bytes. + * This stub is used in some of the TaskPool proofs. + */ +void * pvPortMalloc( size_t xWantedSize ) +{ + if( xWantedSize == 0 ) + { + return NULL; + } + + return nondet_bool() ? malloc( xWantedSize ) : NULL; +} + +void vPortFree( void * pv ) +{ + ( void ) pv; + free( pv ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/include/queue_init.h b/FreeRTOS-Plus/Test/CBMC/include/queue_init.h new file mode 100644 index 000000000..f05d18830 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/include/queue_init.h @@ -0,0 +1,141 @@ +#include "FreeRTOS.h" +#include "queue.h" +#include "queue_datastructure.h" + +#ifndef CBMC_OBJECT_BITS +#define CBMC_OBJECT_BITS 7 +#endif + +#ifndef CBMC_OBJECT_MAX_SIZE +#define CBMC_OBJECT_MAX_SIZE (UINT32_MAX>>(CBMC_OBJECT_BITS+1)) +#endif + +/* Using prvCopyDataToQueue together with prvNotifyQueueSetContainer + leads to a problem space explosion. Therefore, we use this stub + and a sepearted proof on prvCopyDataToQueue to deal with it. + As prvNotifyQueueSetContainer is disabled if configUSE_QUEUE_SETS != 1, + in other cases the original implementation should be used. */ +#if( configUSE_QUEUE_SETS == 1 ) + BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) + { + if(pxQueue->uxItemSize > ( UBaseType_t ) 0) + { + __CPROVER_assert(__CPROVER_r_ok(pvItemToQueue, ( size_t ) pxQueue->uxItemSize), "pvItemToQueue region must be readable"); + if(xPosition == queueSEND_TO_BACK){ + __CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize), "pxQueue->pcWriteTo region must be writable"); + }else{ + __CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize), "pxQueue->u.xQueue.pcReadFrom region must be writable"); + } + return pdFALSE; + }else + { + return nondet_BaseType_t(); + } + } +#endif + +/* xQueueCreateSet is compiled out if configUSE_QUEUE_SETS != 1.*/ +#if( configUSE_QUEUE_SETS == 1 ) + QueueSetHandle_t xUnconstrainedQueueSet() + { + UBaseType_t uxEventQueueLength = 2; + QueueSetHandle_t xSet = xQueueCreateSet(uxEventQueueLength); + if( xSet ) + { + xSet->cTxLock = nondet_int8_t(); + xSet->cRxLock = nondet_int8_t(); + xSet->uxMessagesWaiting = nondet_UBaseType_t(); + xSet->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t(); + /* This is an invariant checked with a couple of asserts in the code base. + If it is false from the beginning, the CBMC proofs are not able to succeed*/ + __CPROVER_assume(xSet->uxMessagesWaiting < xSet->uxLength); + xSet->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t(); + } + return xSet; + } +#endif + +/* Create a mostly unconstrained Queue but bound the max item size. + This is required for performance reasons in CBMC at the moment. */ +QueueHandle_t xUnconstrainedQueueBoundedItemSize( UBaseType_t uxItemSizeBound ) { + UBaseType_t uxQueueLength; + UBaseType_t uxItemSize; + uint8_t ucQueueType; + __CPROVER_assume(uxQueueLength > 0); + __CPROVER_assume(uxItemSize < uxItemSizeBound); + + // QueueGenericCreate method does not check for multiplication overflow + size_t uxQueueStorageSize; + __CPROVER_assume(uxQueueStorageSize < CBMC_OBJECT_MAX_SIZE); + __CPROVER_assume(uxItemSize < uxQueueStorageSize/uxQueueLength); + + QueueHandle_t xQueue = + xQueueGenericCreate(uxQueueLength, uxItemSize, ucQueueType); + if(xQueue){ + xQueue->cTxLock = nondet_int8_t(); + xQueue->cRxLock = nondet_int8_t(); + xQueue->uxMessagesWaiting = nondet_UBaseType_t(); + /* This is an invariant checked with a couple of asserts in the code base. + If it is false from the beginning, the CBMC proofs are not able to succeed*/ + __CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength); + xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t(); + xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t(); + #if( configUSE_QUEUE_SETS == 1) + xQueueAddToSet(xQueue, xUnconstrainedQueueSet()); + #endif + } + return xQueue; +} + +/* Create a mostly unconstrained Queue */ +QueueHandle_t xUnconstrainedQueue( void ) { + UBaseType_t uxQueueLength; + UBaseType_t uxItemSize; + uint8_t ucQueueType; + + __CPROVER_assume(uxQueueLength > 0); + + // QueueGenericCreate method does not check for multiplication overflow + size_t uxQueueStorageSize; + __CPROVER_assume(uxQueueStorageSize < CBMC_OBJECT_MAX_SIZE); + __CPROVER_assume(uxItemSize < uxQueueStorageSize/uxQueueLength); + + QueueHandle_t xQueue = + xQueueGenericCreate(uxQueueLength, uxItemSize, ucQueueType); + + if(xQueue){ + xQueue->cTxLock = nondet_int8_t(); + xQueue->cRxLock = nondet_int8_t(); + xQueue->uxMessagesWaiting = nondet_UBaseType_t(); + /* This is an invariant checked with a couple of asserts in the code base. + If it is false from the beginning, the CBMC proofs are not able to succeed*/ + __CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength); + xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t(); + xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t(); + #if( configUSE_QUEUE_SETS == 1) + xQueueAddToSet(xQueue, xUnconstrainedQueueSet()); + #endif + } + return xQueue; +} + +/* Create a mostly unconstrained Mutex */ +QueueHandle_t xUnconstrainedMutex( void ) { + uint8_t ucQueueType; + QueueHandle_t xQueue = + xQueueCreateMutex(ucQueueType); + if(xQueue){ + xQueue->cTxLock = nondet_int8_t(); + xQueue->cRxLock = nondet_int8_t(); + xQueue->uxMessagesWaiting = nondet_UBaseType_t(); + /* This is an invariant checked with a couple of asserts in the code base. + If it is false from the beginning, the CBMC proofs are not able to succeed*/ + __CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength); + xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t(); + xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t(); + #if( configUSE_QUEUE_SETS == 1) + xQueueAddToSet(xQueue, xUnconstrainedQueueSet()); + #endif + } + return xQueue; +} diff --git a/FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h b/FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h new file mode 100644 index 000000000..a0dd6de4a --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h @@ -0,0 +1,10 @@ +#ifndef INC_TASK_STUBS_H +#define INC_TASK_STUBS_H + +#include "FreeRTOS.h" +#include "task.h" + +BaseType_t xState; +void vInitTaskCheckForTimeOut(BaseType_t maxCounter, BaseType_t maxCounter_limit); + +#endif /* INC_TASK_STUBS_H */ diff --git a/FreeRTOS-Plus/Test/CBMC/patches/.gitattributes b/FreeRTOS-Plus/Test/CBMC/patches/.gitattributes new file mode 100644 index 000000000..a41fc7b45 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/.gitattributes @@ -0,0 +1,2 @@ +# It seems git apply does not want crlf line endings on Windows +*.patch eol=lf diff --git a/FreeRTOS-Plus/Test/CBMC/patches/.gitignore b/FreeRTOS-Plus/Test/CBMC/patches/.gitignore new file mode 100644 index 000000000..4dec98ff0 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/.gitignore @@ -0,0 +1,2 @@ +auto_patch* +patched diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch b/FreeRTOS-Plus/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch new file mode 100644 index 000000000..29cde0e77 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch @@ -0,0 +1,79 @@ +This patch removes the volatile qualifier from some global variable +declarations in the tasks.c file. For task pool proofs, we are running +`goto-instrument` with the `--nondet-volatile` flag on, which causes reads from +volatile variable to be nondeterministic (i.e., any possible value can be +returned). This is actually the desired behavior for volatile variables +regarding verification purposes. However, this causes a lot of trouble when +such variables are pointers, since one of the possible values we can get when +dereferencing a volatile pointer is `NULL`. + +In the case of `uxPendedTicks`, a non-volatile copy of the variable is done +before the following loop in tasks.c (lines 2231-2255): + +{ + UBaseType_t uxPendedCounts = uxPendedTicks; /* Non-volatile copy. */ + + if( uxPendedCounts > ( UBaseType_t ) 0U ) + { + do + { + if( xTaskIncrementTick() != pdFALSE ) + { + xYieldPending = pdTRUE; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + --uxPendedCounts; + } while( uxPendedCounts > ( UBaseType_t ) 0U ); + + uxPendedTicks = 0; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } +} + +Here, `uxPendedTicks` could return any value, making it impossible to unwind +(or unroll) this loop in CBMC. Therefore, we require `uxPendedTicks` to behave +as a regular variable so that the loop can be unwound. + +--- +diff --git a/FreeRTOS/Source/tasks.c b/FreeRTOS/Source/tasks.c +index ff657733..8b57d198 100644 +--- a/FreeRTOS/Source/tasks.c ++++ b/FreeRTOS/Source/tasks.c +@@ -331,7 +331,7 @@ typedef tskTCB TCB_t; + + /*lint -save -e956 A manual analysis and inspection has been used to determine + which static variables must be declared volatile. */ +-PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL; ++PRIVILEGED_DATA TCB_t * pxCurrentTCB = NULL; + + /* Lists for ready and blocked tasks. -------------------- + xDelayedTaskList1 and xDelayedTaskList2 could be move to function scople but +@@ -340,8 +340,8 @@ the static qualifier. */ + PRIVILEGED_DATA static List_t pxReadyTasksLists[ configMAX_PRIORITIES ];/*< Prioritised ready tasks. */ + PRIVILEGED_DATA static List_t xDelayedTaskList1; /*< Delayed tasks. */ + PRIVILEGED_DATA static List_t xDelayedTaskList2; /*< Delayed tasks (two lists are used - one for delays that have overflowed the current tick count. */ +-PRIVILEGED_DATA static List_t * volatile pxDelayedTaskList; /*< Points to the delayed task list currently being used. */ +-PRIVILEGED_DATA static List_t * volatile pxOverflowDelayedTaskList; /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */ ++PRIVILEGED_DATA static List_t * pxDelayedTaskList; /*< Points to the delayed task list currently being used. */ ++PRIVILEGED_DATA static List_t * pxOverflowDelayedTaskList; /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */ + PRIVILEGED_DATA static List_t xPendingReadyList; /*< Tasks that have been readied while the scheduler was suspended. They will be moved to the ready list when the scheduler is resumed. */ + + #if( INCLUDE_vTaskDelete == 1 ) +@@ -368,10 +368,10 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseTyp + + /* Other file private variables. --------------------------------*/ + PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseType_t ) 0U; + PRIVILEGED_DATA static volatile TickType_t xTickCount = ( TickType_t ) configINITIAL_TICK_COUNT; + PRIVILEGED_DATA static volatile UBaseType_t uxTopReadyPriority = tskIDLE_PRIORITY; + PRIVILEGED_DATA static volatile BaseType_t xSchedulerRunning = pdFALSE; +-PRIVILEGED_DATA static volatile TickType_t xPendedTicks = ( TickType_t ) 0U; ++PRIVILEGED_DATA static TickType_t xPendedTicks = ( TickType_t ) 0U; + PRIVILEGED_DATA static volatile BaseType_t xYieldPending = pdFALSE; + PRIVILEGED_DATA static volatile BaseType_t xNumOfOverflows = ( BaseType_t ) 0; + PRIVILEGED_DATA static UBaseType_t uxTaskNumber = ( UBaseType_t ) 0U; diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch b/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch new file mode 100644 index 000000000..5a79ae8cd --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch @@ -0,0 +1,22 @@ +diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c +index df2b9c8c..c2265c26 100644 +--- a/FreeRTOS/Source/queue.c ++++ b/FreeRTOS/Source/queue.c +@@ -105,7 +105,7 @@ static BaseType_t prvIsQueueFull( const Queue_t *pxQueue ) PRIVILEGED_FUNCTION; + * Copies an item into the queue, either at the front of the queue or the + * back of the queue. + */ +-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION; ++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION; + + /* + * Copies an item out of a queue. +@@ -1985,7 +1985,7 @@ Queue_t * const pxQueue = xQueue; + #endif /* configUSE_MUTEXES */ + /*-----------------------------------------------------------*/ + +-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) ++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) + { + BaseType_t xReturn = pdFALSE; + UBaseType_t uxMessagesWaiting; diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch b/FreeRTOS-Plus/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch new file mode 100644 index 000000000..9cbe7cf5f --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch @@ -0,0 +1,22 @@ +diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c +index 17a6964e..24a40c29 100644 +--- a/FreeRTOS/Source/queue.c ++++ b/FreeRTOS/Source/queue.c +@@ -207,7 +207,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer + * Checks to see if a queue is a member of a queue set, and if so, notifies + * the queue set that the queue contains data. + */ +- static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION; ++ BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION; + #endif + + /* +@@ -2887,7 +2887,7 @@ Queue_t * const pxQueue = xQueue; + + #if ( configUSE_QUEUE_SETS == 1 ) + +- static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) ++ BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) + { + Queue_t *pxQueueSetContainer = pxQueue->pxQueueSetContainer; + BaseType_t xReturn = pdFALSE; diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch b/FreeRTOS-Plus/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch new file mode 100644 index 000000000..eaae401c6 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch @@ -0,0 +1,22 @@ +diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c +index 17a6964e..60ea3e69 100644 +--- a/FreeRTOS/Source/queue.c ++++ b/FreeRTOS/Source/queue.c +@@ -175,7 +175,7 @@ typedef xQUEUE Queue_t; + * to indicate that a task may require unblocking. When the queue in unlocked + * these lock counts are inspected, and the appropriate action taken. + */ +-static void prvUnlockQueue( Queue_t * const pxQueue ) PRIVILEGED_FUNCTION; ++void prvUnlockQueue( Queue_t * const pxQueue ) PRIVILEGED_FUNCTION; + + /* + * Uses a critical section to determine if there is any data in a queue. +@@ -2175,7 +2175,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer + } + /*-----------------------------------------------------------*/ + +-static void prvUnlockQueue( Queue_t * const pxQueue ) ++void prvUnlockQueue( Queue_t * const pxQueue ) + { + /* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. */ + diff --git a/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h new file mode 100644 index 000000000..28de2bd15 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h @@ -0,0 +1,237 @@ +/* + * FreeRTOS Kernel V10.0.1 + * Copyright (C) 2017 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 + */ + +#ifndef FREERTOS_CONFIG_H +#define FREERTOS_CONFIG_H + +/*----------------------------------------------------------- +* Application specific definitions. +* +* These definitions should be adjusted for your particular hardware and +* application requirements. +* +* THESE PARAMETERS ARE DESCRIBED WITHIN THE 'CONFIGURATION' SECTION OF THE +* FreeRTOS API DOCUMENTATION AVAILABLE ON THE FreeRTOS.org WEB SITE. +* http://www.freertos.org/a00110.html +* +* The bottom of this file contains some constants specific to running the UDP +* stack in this demo. Constants specific to FreeRTOS+TCP itself (rather than +* the demo) are contained in FreeRTOSIPConfig.h. +*----------------------------------------------------------*/ +#define configENABLE_BACKWARD_COMPATIBILITY 1 +#define configUSE_PREEMPTION 1 +#define configUSE_PORT_OPTIMISED_TASK_SELECTION 1 +#define configMAX_PRIORITIES ( 7 ) +#define configTICK_RATE_HZ ( 1000 ) /* In this non-real time simulated environment the tick frequency has to be at least a multiple of the Win32 tick frequency, and therefore very slow. */ +#define configMINIMAL_STACK_SIZE ( ( unsigned short ) 60 ) /* In this simulated case, the stack only has to hold one small structure as the real stack is part of the Win32 thread. */ +#define configTOTAL_HEAP_SIZE ( ( size_t ) ( 2048U * 1024U ) ) +#define configMAX_TASK_NAME_LEN ( 15 ) +#define configUSE_16_BIT_TICKS 0 +#define configIDLE_SHOULD_YIELD 1 +#define configUSE_CO_ROUTINES 0 +#ifndef configUSE_MUTEXES + #define configUSE_MUTEXES 1 +#endif +#ifndef configUSE_RECURSIVE_MUTEXES + #define configUSE_RECURSIVE_MUTEXES 1 +#endif +#define configQUEUE_REGISTRY_SIZE 0 +#define configUSE_APPLICATION_TASK_TAG 1 +#define configUSE_COUNTING_SEMAPHORES 1 +#define configUSE_ALTERNATIVE_API 0 +#define configNUM_THREAD_LOCAL_STORAGE_POINTERS 3 /* FreeRTOS+FAT requires 2 pointers if a CWD is supported. */ +#define configRECORD_STACK_HIGH_ADDRESS 1 + +/* Hook function related definitions. */ +#ifndef configUSE_TICK_HOOK + #define configUSE_TICK_HOOK 0 +#endif +#define configUSE_IDLE_HOOK 1 +#define configUSE_MALLOC_FAILED_HOOK 1 +#define configCHECK_FOR_STACK_OVERFLOW 0 /* Not applicable to the Win32 port. */ + +/* Software timer related definitions. */ +#define configUSE_TIMERS 1 +#define configTIMER_TASK_PRIORITY ( configMAX_PRIORITIES - 1 ) +#define configTIMER_QUEUE_LENGTH 5 +#define configTIMER_TASK_STACK_DEPTH ( configMINIMAL_STACK_SIZE * 2 ) + +/* Event group related definitions. */ +#define configUSE_EVENT_GROUPS 1 + +/* Co-routine definitions. */ +#define configUSE_CO_ROUTINES 0 +#define configMAX_CO_ROUTINE_PRIORITIES ( 2 ) + +/* Memory allocation strategy. */ +#ifndef configSUPPORT_DYNAMIC_ALLOCATION + #define configSUPPORT_DYNAMIC_ALLOCATION 1 +#endif +#ifndef configSUPPORT_STATIC_ALLOCATION + #define configSUPPORT_STATIC_ALLOCATION 1 +#endif + + +/* Set the following definitions to 1 to include the API function, or zero + * to exclude the API function. */ +#define INCLUDE_vTaskPrioritySet 1 +#define INCLUDE_uxTaskPriorityGet 1 +#define INCLUDE_vTaskDelete 1 +#define INCLUDE_vTaskCleanUpResources 0 +#ifndef INCLUDE_vTaskSuspend + #define INCLUDE_vTaskSuspend 1 +#endif +#define INCLUDE_vTaskDelayUntil 1 +#define INCLUDE_vTaskDelay 1 +#define INCLUDE_uxTaskGetStackHighWaterMark 1 +#ifndef INCLUDE_xTaskGetSchedulerState + #define INCLUDE_xTaskGetSchedulerState 1 +#endif +#define INCLUDE_xTimerGetTimerTaskHandle 0 +#define INCLUDE_xTaskGetIdleTaskHandle 0 +#define INCLUDE_xQueueGetMutexHolder 1 +#define INCLUDE_eTaskGetState 1 +#define INCLUDE_xEventGroupSetBitsFromISR 1 +#define INCLUDE_xTimerPendFunctionCall 1 +#define INCLUDE_xTaskGetCurrentTaskHandle 1 +#define INCLUDE_xTaskAbortDelay 1 + +/* This demo makes use of one or more example stats formatting functions. These + * format the raw data provided by the uxTaskGetSystemState() function in to human + * readable ASCII form. See the notes in the implementation of vTaskList() within + * FreeRTOS/Source/tasks.c for limitations. configUSE_STATS_FORMATTING_FUNCTIONS + * is set to 2 so the formatting functions are included without the stdio.h being + * included in tasks.c. That is because this project defines its own sprintf() + * functions. */ +#define configUSE_STATS_FORMATTING_FUNCTIONS 1 + +/* Assert call defined for debug builds. */ +extern void vAssertCalled( const char * pcFile, + uint32_t ulLine ); +#ifndef configASSERT +#define configASSERT( x ) if( ( x ) == 0 ) vAssertCalled( __FILE__, __LINE__ ) +#endif + +/* Remove logging in formal verification */ +#define configPRINTF( X ) + +/* Non-format version thread-safe print. */ +#define configPRINT_STRING( X ) + +/* Application specific definitions follow. **********************************/ + +/* If configINCLUDE_DEMO_DEBUG_STATS is set to one, then a few basic IP trace + * macros are defined to gather some UDP stack statistics that can then be viewed + * through the CLI interface. */ +#define configINCLUDE_DEMO_DEBUG_STATS 1 + +/* The size of the global output buffer that is available for use when there + * are multiple command interpreters running at once (for example, one on a UART + * and one on TCP/IP). This is done to prevent an output buffer being defined by + * each implementation - which would waste RAM. In this case, there is only one + * command interpreter running, and it has its own local output buffer, so the + * global buffer is just set to be one byte long as it is not used and should not + * take up unnecessary RAM. */ +#define configCOMMAND_INT_MAX_OUTPUT_SIZE 1 + +/* Only used when running in the FreeRTOS Windows simulator. Defines the + * priority of the task used to simulate Ethernet interrupts. */ +#define configMAC_ISR_SIMULATOR_PRIORITY ( configMAX_PRIORITIES - 1 ) + +/* This demo creates a virtual network connection by accessing the raw Ethernet + * or WiFi data to and from a real network connection. Many computers have more + * than one real network port, and configNETWORK_INTERFACE_TO_USE is used to tell + * the demo which real port should be used to create the virtual port. The ports + * available are displayed on the console when the application is executed. For + * example, on my development laptop setting configNETWORK_INTERFACE_TO_USE to 4 + * results in the wired network being used, while setting + * configNETWORK_INTERFACE_TO_USE to 2 results in the wireless network being + * used. */ +#define configNETWORK_INTERFACE_TO_USE ( 0L ) + +/* The address of an echo server that will be used by the two demo echo client + * tasks: + * http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_Echo_Clients.html, + * http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/UDP_Echo_Clients.html. */ +#define configECHO_SERVER_ADDR0 192 +#define configECHO_SERVER_ADDR1 168 +#define configECHO_SERVER_ADDR2 2 +#define configECHO_SERVER_ADDR3 6 +#define configTCP_ECHO_CLIENT_PORT 7 + +/* Default MAC address configuration. The demo creates a virtual network + * connection that uses this MAC address by accessing the raw Ethernet/WiFi data + * to and from a real network connection on the host PC. See the + * configNETWORK_INTERFACE_TO_USE definition above for information on how to + * configure the real network connection to use. */ +#define configMAC_ADDR0 0x00 +#define configMAC_ADDR1 0x11 +#define configMAC_ADDR2 0x22 +#define configMAC_ADDR3 0x33 +#define configMAC_ADDR4 0x44 +#define configMAC_ADDR5 0x21 + +/* Default IP address configuration. Used in ipconfigUSE_DHCP is set to 0, or + * ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configIP_ADDR0 192 +#define configIP_ADDR1 168 +#define configIP_ADDR2 0 +#define configIP_ADDR3 105 + +/* Default gateway IP address configuration. Used in ipconfigUSE_DHCP is set to + * 0, or ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configGATEWAY_ADDR0 192 +#define configGATEWAY_ADDR1 168 +#define configGATEWAY_ADDR2 0 +#define configGATEWAY_ADDR3 1 + +/* Default DNS server configuration. OpenDNS addresses are 208.67.222.222 and + * 208.67.220.220. Used in ipconfigUSE_DHCP is set to 0, or ipconfigUSE_DHCP is + * set to 1 but a DNS server cannot be contacted.*/ +#define configDNS_SERVER_ADDR0 208 +#define configDNS_SERVER_ADDR1 67 +#define configDNS_SERVER_ADDR2 222 +#define configDNS_SERVER_ADDR3 222 + +/* Default netmask configuration. Used in ipconfigUSE_DHCP is set to 0, or + * ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configNET_MASK0 255 +#define configNET_MASK1 255 +#define configNET_MASK2 255 +#define configNET_MASK3 0 + +/* The UDP port to which print messages are sent. */ +#define configPRINT_PORT ( 15000 ) + +#define configPROFILING ( 0 ) + +/* Pseudo random number generater used by some demo tasks. */ +extern uint32_t ulRand(); +#define configRAND32() ulRand() + +/* The platform that FreeRTOS is running on. */ +#define configPLATFORM_NAME "WinSim" + +#endif /* FREERTOS_CONFIG_H */ diff --git a/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSIPConfig.h b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSIPConfig.h new file mode 100644 index 000000000..13a2450b9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSIPConfig.h @@ -0,0 +1,305 @@ +/* +FreeRTOS Kernel V10.2.0 +Copyright (C) 2017 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 +*/ + + +/***************************************************************************** +* +* See the following URL for configuration information. +* http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_IP_Configuration.html +* +*****************************************************************************/ + +#ifndef FREERTOS_IP_CONFIG_H +#define FREERTOS_IP_CONFIG_H + +/* Set to 1 to print out debug messages. If ipconfigHAS_DEBUG_PRINTF is set to + * 1 then FreeRTOS_debug_printf should be defined to the function used to print + * out the debugging messages. */ +#define ipconfigHAS_DEBUG_PRINTF 0 +#if ( ipconfigHAS_DEBUG_PRINTF == 1 ) + #define FreeRTOS_debug_printf( X ) configPRINTF( X ) +#endif + +/* Set to 1 to print out non debugging messages, for example the output of the + * FreeRTOS_netstat() command, and ping replies. If ipconfigHAS_PRINTF is set to 1 + * then FreeRTOS_printf should be set to the function used to print out the + * messages. */ +#define FreeRTOS_printf( X ) + + +/* Define the byte order of the target MCU (the MCU FreeRTOS+TCP is executing + * on). Valid options are pdFREERTOS_BIG_ENDIAN and pdFREERTOS_LITTLE_ENDIAN. */ +#define ipconfigBYTE_ORDER pdFREERTOS_LITTLE_ENDIAN + +/* If the network card/driver includes checksum offloading (IP/TCP/UDP checksums) + * then set ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM to 1 to prevent the software + * stack repeating the checksum calculations. */ +#define ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM 1 + +/* Several API's will block until the result is known, or the action has been + * performed, for example FreeRTOS_send() and FreeRTOS_recv(). The timeouts can be + * set per socket, using setsockopt(). If not set, the times below will be + * used as defaults. */ +#define ipconfigSOCK_DEFAULT_RECEIVE_BLOCK_TIME ( 5000 ) +#define ipconfigSOCK_DEFAULT_SEND_BLOCK_TIME ( 5000 ) + +/* Include support for DNS caching. For TCP, having a small DNS cache is very + * useful. When a cache is present, ipconfigDNS_REQUEST_ATTEMPTS can be kept low + * and also DNS may use small timeouts. If a DNS reply comes in after the DNS + * socket has been destroyed, the result will be stored into the cache. The next + * call to FreeRTOS_gethostbyname() will return immediately, without even creating + * a socket. */ +#define ipconfigUSE_DNS_CACHE ( 1 ) +#define ipconfigDNS_REQUEST_ATTEMPTS ( 2 ) + +/* The IP stack executes it its own task (although any application task can make + * use of its services through the published sockets API). ipconfigUDP_TASK_PRIORITY + * sets the priority of the task that executes the IP stack. The priority is a + * standard FreeRTOS task priority so can take any value from 0 (the lowest + * priority) to (configMAX_PRIORITIES - 1) (the highest priority). + * configMAX_PRIORITIES is a standard FreeRTOS configuration parameter defined in + * FreeRTOSConfig.h, not FreeRTOSIPConfig.h. Consideration needs to be given as to + * the priority assigned to the task executing the IP stack relative to the + * priority assigned to tasks that use the IP stack. */ +#define ipconfigIP_TASK_PRIORITY ( configMAX_PRIORITIES - 2 ) + +/* The size, in words (not bytes), of the stack allocated to the FreeRTOS+TCP + * task. This setting is less important when the FreeRTOS Win32 simulator is used + * as the Win32 simulator only stores a fixed amount of information on the task + * stack. FreeRTOS includes optional stack overflow detection, see: + * http://www.freertos.org/Stacks-and-stack-overflow-checking.html. */ +#define ipconfigIP_TASK_STACK_SIZE_WORDS ( configMINIMAL_STACK_SIZE * 5 ) + +/* ipconfigRAND32() is called by the IP stack to generate random numbers for + * things such as a DHCP transaction number or initial sequence number. Random + * number generation is performed via this macro to allow applications to use their + * own random number generation method. For example, it might be possible to + * generate a random number by sampling noise on an analogue input. */ +extern uint32_t ulRand(); +#define ipconfigRAND32() ulRand() + +/* If ipconfigUSE_NETWORK_EVENT_HOOK is set to 1 then FreeRTOS+TCP will call the + * network event hook at the appropriate times. If ipconfigUSE_NETWORK_EVENT_HOOK + * is not set to 1 then the network event hook will never be called. See: + * http://www.FreeRTOS.org/FreeRTOS-Plus/FreeRTOS_Plus_UDP/API/vApplicationIPNetworkEventHook.shtml. + */ +#define ipconfigUSE_NETWORK_EVENT_HOOK 1 + +/* Sockets have a send block time attribute. If FreeRTOS_sendto() is called but + * a network buffer cannot be obtained then the calling task is held in the Blocked + * state (so other tasks can continue to executed) until either a network buffer + * becomes available or the send block time expires. If the send block time expires + * then the send operation is aborted. The maximum allowable send block time is + * capped to the value set by ipconfigMAX_SEND_BLOCK_TIME_TICKS. Capping the + * maximum allowable send block time prevents prevents a deadlock occurring when + * all the network buffers are in use and the tasks that process (and subsequently + * free) the network buffers are themselves blocked waiting for a network buffer. + * ipconfigMAX_SEND_BLOCK_TIME_TICKS is specified in RTOS ticks. A time in + * milliseconds can be converted to a time in ticks by dividing the time in + * milliseconds by portTICK_PERIOD_MS. */ +#define ipconfigUDP_MAX_SEND_BLOCK_TIME_TICKS ( 5000U / portTICK_PERIOD_MS ) + +/* If ipconfigUSE_DHCP is 1 then FreeRTOS+TCP will attempt to retrieve an IP + * address, netmask, DNS server address and gateway address from a DHCP server. If + * ipconfigUSE_DHCP is 0 then FreeRTOS+TCP will use a static IP address. The + * stack will revert to using the static IP address even when ipconfigUSE_DHCP is + * set to 1 if a valid configuration cannot be obtained from a DHCP server for any + * reason. The static configuration used is that passed into the stack by the + * FreeRTOS_IPInit() function call. */ +#define ipconfigUSE_DHCP 1 +#define ipconfigDHCP_REGISTER_HOSTNAME 1 +#define ipconfigDHCP_USES_UNICAST 1 + +/* If ipconfigDHCP_USES_USER_HOOK is set to 1 then the application writer must + * provide an implementation of the DHCP callback function, + * xApplicationDHCPUserHook(). */ +#define ipconfigUSE_DHCP_HOOK 0 + +/* When ipconfigUSE_DHCP is set to 1, DHCP requests will be sent out at + * increasing time intervals until either a reply is received from a DHCP server + * and accepted, or the interval between transmissions reaches + * ipconfigMAXIMUM_DISCOVER_TX_PERIOD. The IP stack will revert to using the + * static IP address passed as a parameter to FreeRTOS_IPInit() if the + * re-transmission time interval reaches ipconfigMAXIMUM_DISCOVER_TX_PERIOD without + * a DHCP reply being received. */ +#define ipconfigMAXIMUM_DISCOVER_TX_PERIOD \ + ( 120000U / portTICK_PERIOD_MS ) + +/* The ARP cache is a table that maps IP addresses to MAC addresses. The IP + * stack can only send a UDP message to a remove IP address if it knowns the MAC + * address associated with the IP address, or the MAC address of the router used to + * contact the remote IP address. When a UDP message is received from a remote IP + * address the MAC address and IP address are added to the ARP cache. When a UDP + * message is sent to a remote IP address that does not already appear in the ARP + * cache then the UDP message is replaced by a ARP message that solicits the + * required MAC address information. ipconfigARP_CACHE_ENTRIES defines the maximum + * number of entries that can exist in the ARP table at any one time. */ +#define ipconfigARP_CACHE_ENTRIES 6 + +/* ARP requests that do not result in an ARP response will be re-transmitted a + * maximum of ipconfigMAX_ARP_RETRANSMISSIONS times before the ARP request is + * aborted. */ +#define ipconfigMAX_ARP_RETRANSMISSIONS ( 5 ) + +/* ipconfigMAX_ARP_AGE defines the maximum time between an entry in the ARP + * table being created or refreshed and the entry being removed because it is stale. + * New ARP requests are sent for ARP cache entries that are nearing their maximum + * age. ipconfigMAX_ARP_AGE is specified in tens of seconds, so a value of 150 is + * equal to 1500 seconds (or 25 minutes). */ +#define ipconfigMAX_ARP_AGE 150 + +/* Implementing FreeRTOS_inet_addr() necessitates the use of string handling + * routines, which are relatively large. To save code space the full + * FreeRTOS_inet_addr() implementation is made optional, and a smaller and faster + * alternative called FreeRTOS_inet_addr_quick() is provided. FreeRTOS_inet_addr() + * takes an IP in decimal dot format (for example, "192.168.0.1") as its parameter. + * FreeRTOS_inet_addr_quick() takes an IP address as four separate numerical octets + * (for example, 192, 168, 0, 1) as its parameters. If + * ipconfigINCLUDE_FULL_INET_ADDR is set to 1 then both FreeRTOS_inet_addr() and + * FreeRTOS_indet_addr_quick() are available. If ipconfigINCLUDE_FULL_INET_ADDR is + * not set to 1 then only FreeRTOS_indet_addr_quick() is available. */ +#define ipconfigINCLUDE_FULL_INET_ADDR 1 + +/* ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS defines the total number of network buffer that + * are available to the IP stack. The total number of network buffers is limited + * to ensure the total amount of RAM that can be consumed by the IP stack is capped + * to a pre-determinable value. */ +#define ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS 60 + +/* A FreeRTOS queue is used to send events from application tasks to the IP + * stack. ipconfigEVENT_QUEUE_LENGTH sets the maximum number of events that can + * be queued for processing at any one time. The event queue must be a minimum of + * 5 greater than the total number of network buffers. */ +#define ipconfigEVENT_QUEUE_LENGTH \ + ( ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS + 5 ) + +/* The address of a socket is the combination of its IP address and its port + * number. FreeRTOS_bind() is used to manually allocate a port number to a socket + * (to 'bind' the socket to a port), but manual binding is not normally necessary + * for client sockets (those sockets that initiate outgoing connections rather than + * wait for incoming connections on a known port number). If + * ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND is set to 1 then calling + * FreeRTOS_sendto() on a socket that has not yet been bound will result in the IP + * stack automatically binding the socket to a port number from the range + * socketAUTO_PORT_ALLOCATION_START_NUMBER to 0xffff. If + * ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND is set to 0 then calling FreeRTOS_sendto() + * on a socket that has not yet been bound will result in the send operation being + * aborted. */ +#define ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND 1 + +/* Defines the Time To Live (TTL) values used in outgoing UDP packets. */ +#define ipconfigUDP_TIME_TO_LIVE 128 +/* Also defined in FreeRTOSIPConfigDefaults.h. */ +#define ipconfigTCP_TIME_TO_LIVE 128 + +/* USE_TCP: Use TCP and all its features. */ +#define ipconfigUSE_TCP ( 1 ) + +/* USE_WIN: Let TCP use windowing mechanism. */ +#define ipconfigUSE_TCP_WIN ( 1 ) + +/* The MTU is the maximum number of bytes the payload of a network frame can + * contain. For normal Ethernet V2 frames the maximum MTU is 1500. Setting a + * lower value can save RAM, depending on the buffer management scheme used. If + * ipconfigCAN_FRAGMENT_OUTGOING_PACKETS is 1 then (ipconfigNETWORK_MTU - 28) must + * be divisible by 8. */ +#define ipconfigNETWORK_MTU 1200U + +/* Set ipconfigUSE_DNS to 1 to include a basic DNS client/resolver. DNS is used + * through the FreeRTOS_gethostbyname() API function. */ +#define ipconfigUSE_DNS 1 + +/* If ipconfigREPLY_TO_INCOMING_PINGS is set to 1 then the IP stack will + * generate replies to incoming ICMP echo (ping) requests. */ +#define ipconfigREPLY_TO_INCOMING_PINGS 1 + +/* If ipconfigSUPPORT_OUTGOING_PINGS is set to 1 then the + * FreeRTOS_SendPingRequest() API function is available. */ +#define ipconfigSUPPORT_OUTGOING_PINGS 0 + +/* If ipconfigSUPPORT_SELECT_FUNCTION is set to 1 then the FreeRTOS_select() + * (and associated) API function is available. */ +#define ipconfigSUPPORT_SELECT_FUNCTION 0 + +/* If ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES is set to 1 then Ethernet frames + * that are not in Ethernet II format will be dropped. This option is included for + * potential future IP stack developments. */ +#define ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES 1 + +/* If ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES is set to 1 then it is the + * responsibility of the Ethernet interface to filter out packets that are of no + * interest. If the Ethernet interface does not implement this functionality, then + * set ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES to 0 to have the IP stack + * perform the filtering instead (it is much less efficient for the stack to do it + * because the packet will already have been passed into the stack). If the + * Ethernet driver does all the necessary filtering in hardware then software + * filtering can be removed by using a value other than 1 or 0. */ +#define ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES 1 + +/* The windows simulator cannot really simulate MAC interrupts, and needs to + * block occasionally to allow other tasks to run. */ +#define configWINDOWS_MAC_INTERRUPT_SIMULATOR_DELAY ( 20 / portTICK_PERIOD_MS ) + +/* Advanced only: in order to access 32-bit fields in the IP packets with + * 32-bit memory instructions, all packets will be stored 32-bit-aligned, + * plus 16-bits. This has to do with the contents of the IP-packets: all + * 32-bit fields are 32-bit-aligned, plus 16-bit. */ +#define ipconfigPACKET_FILLER_SIZE 2U + +/* Define the size of the pool of TCP window descriptors. On the average, each + * TCP socket will use up to 2 x 6 descriptors, meaning that it can have 2 x 6 + * outstanding packets (for Rx and Tx). When using up to 10 TP sockets + * simultaneously, one could define TCP_WIN_SEG_COUNT as 120. */ +#define ipconfigTCP_WIN_SEG_COUNT 240 + +/* Each TCP socket has a circular buffers for Rx and Tx, which have a fixed + * maximum size. Define the size of Rx buffer for TCP sockets. */ +#define ipconfigTCP_RX_BUFFER_LENGTH ( 10000 ) + +/* Define the size of Tx buffer for TCP sockets. */ +#define ipconfigTCP_TX_BUFFER_LENGTH ( 10000 ) + +/* When using call-back handlers, the driver may check if the handler points to + * real program memory (RAM or flash) or just has a random non-zero value. */ +#define ipconfigIS_VALID_PROG_ADDRESS( x ) ( ( x ) != NULL ) + +/* Include support for TCP keep-alive messages. */ +#define ipconfigTCP_KEEP_ALIVE ( 1 ) +#define ipconfigTCP_KEEP_ALIVE_INTERVAL ( 20 ) /* Seconds. */ + +/* The socket semaphore is used to unblock the MQTT task. */ +#define ipconfigSOCKET_HAS_USER_SEMAPHORE ( 0 ) + +#define ipconfigSOCKET_HAS_USER_WAKE_CALLBACK ( 1 ) +#define ipconfigUSE_CALLBACKS ( 0 ) + + +#define portINLINE __inline + +void vApplicationMQTTGetKeys( const char ** ppcRootCA, + const char ** ppcClientCert, + const char ** ppcClientPrivateKey ); + +#endif /* FREERTOS_IP_CONFIG_H */ diff --git a/FreeRTOS-Plus/Test/CBMC/patches/Makefile b/FreeRTOS-Plus/Test/CBMC/patches/Makefile new file mode 100644 index 000000000..27888e63b --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/Makefile @@ -0,0 +1,24 @@ +BRANCH=freertos + +PATCHED=patched + +default: + git format-patch $(BRANCH)..$(BRANCH)-cbmc-patches + +patch: + if [ ! -f $(PATCHED) ]; then \ + for p in *.patch; do \ + (cd ../../..; patch -p1 < CBMC/patches/$${p}) \ + done; \ + cat > $(PATCHED) < /dev/null; \ + fi + +unpatch: + git checkout ../../../lib + $(RM) $(PATCHED) + +#patching file lib/FreeRTOS-Plus-TCP/include/FreeRTOS_IP_Private.h +#patching file lib/include/private/list.h +#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DHCP.c +#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c +#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_TCP_WIN.c diff --git a/FreeRTOS-Plus/Test/CBMC/patches/README.md b/FreeRTOS-Plus/Test/CBMC/patches/README.md new file mode 100644 index 000000000..ec0e5d424 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/README.md @@ -0,0 +1,6 @@ +This directory includes patches to FreeRTOS required to run the CBMC proofs. + +The patches fall into three classes: +* First is a refactoring of prvCheckOptions +* Second is the removal of static attributes from some functions +* Third is two patches dealing with shortcomings of CBMC that should be removed soon.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/patches/__init__.py b/FreeRTOS-Plus/Test/CBMC/patches/__init__.py new file mode 100755 index 000000000..e69de29bb --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/__init__.py diff --git a/FreeRTOS-Plus/Test/CBMC/patches/compute_patch.py b/FreeRTOS-Plus/Test/CBMC/patches/compute_patch.py new file mode 100755 index 000000000..3e854177c --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/compute_patch.py @@ -0,0 +1,241 @@ +#!/usr/bin/env python3 +# +# Generation of patches 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 json +import os +import re +import subprocess +import textwrap +import unittest + +from patches_constants import PATCHES_DIR +from patches_constants import HEADERS + + +DEFINE_REGEX_MAKEFILE = re.compile(r"(?:['\"])?([\w]+)") +DEFINE_REGEX_HEADER = re.compile(r"\s*#\s*define\s*([\w]+)") + +class DirtyGitError(Exception): + pass + +class PatchCreationError(Exception): + pass + +def prolog(): + return textwrap.dedent("""\ + This script generates patch files for the header files used + in the cbmc proof. These patches permit setting values of preprocessor + macros as part of the proof configuration. + """) + + +def find_all_defines(): + """Collects all define values in Makefile.json. + + Some of the Makefiles use # in the json to make comments. + As this is non standard json, we need to remove the comment + lines before parsing. Then we extract all defines from the file. + """ + defines = set() + + proof_dir = os.path.abspath(os.path.join(PATCHES_DIR, "..", "proofs")) + + for fldr, _, fyles in os.walk(proof_dir): + if "Makefile.json" in fyles: + file = os.path.join(fldr, "Makefile.json") + key = "DEF" + elif "MakefileCommon.json" in fyles: + file = os.path.join(fldr, "MakefileCommon.json") + key = "DEF " + else: + continue + with open(file, "r") as source: + content = "".join([line for line in source + if line and not line.strip().startswith("#")]) + makefile = json.loads(content) + if key in makefile.keys(): + """This regex parses the define declaration in Makefile.json + 'macro(x)=false' is an example for a declaration. + 'macro' is expected to be matched. + """ + for define in makefile[key]: + matched = DEFINE_REGEX_MAKEFILE.match(define) + if matched: + defines.add(matched.group(1)) + return defines + +def manipulate_headerfile(defines, header_file): + """Wraps all defines used in an ifndef.""" + + # This regex matches the actual define in the header file. + modified_content = "" + with open(header_file, "r") as source: + last = "" + for line in source: + match = DEFINE_REGEX_HEADER.match(line) + if (match and + match.group(1) in defines and + not last.lstrip().startswith("#ifndef")): + full_def = line + # this loop deals with multiline definitions + while line.rstrip().endswith("\\"): + line = next(source) + full_def += line + # indentation for multiline definitions can be improved + modified_content += textwrap.dedent("""\ + #ifndef {target} + {original}\ + #endif + """.format(target=match.group(1), original=full_def)) + else: + modified_content += line + last = line + with open(header_file, "w") as output: + output.write(modified_content) + + +def header_dirty(header_files): + """Check that the header_file is not previously modified.""" + + # Git does not update the modified file list returned by diff-files on + # apply -R (at least not on MacOS). + # Running git status updates git's internal state. + status = subprocess.run(["git", "status"], stdout=subprocess.DEVNULL, + stderr=subprocess.PIPE, universal_newlines=True) + + diff_state = subprocess.run(["git", "diff-files"], stdout=subprocess.PIPE, + stderr=subprocess.PIPE, universal_newlines=True) + + if status.returncode: + raise DirtyGitError(textwrap.dedent("""\ + Could not run git status. Exited: {} + stderr: {} + """.format(status.returncode, status.stderr))) + + if diff_state.returncode: + raise DirtyGitError(textwrap.dedent("""\ + Could not run git diff-files. Exited: {} + stderr: {} + """.format(diff_state.returncode, diff_state.stderr))) + + for header_file in header_files: + if os.path.basename(header_file) + "\n" in diff_state.stdout: + return True + return False + + +def create_patch(defines, header_file): + """Computes a patch enclosing defines used in CBMC proofs with #ifndef.""" + manipulate_headerfile(defines, header_file) + patch = subprocess.run(["git", "diff", header_file], + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, universal_newlines=True) + cleaned = subprocess.run(["git", "checkout", "--", header_file], + stdout=subprocess.DEVNULL, + stderr=subprocess.PIPE, universal_newlines=True) + + if patch.returncode: + raise PatchCreationError(textwrap.dedent("""\ + git diff exited with error code: {} + stderr: {} + """.format(patch.returncode, patch.stderr))) + + if cleaned.returncode: + raise DirtyGitError(textwrap.dedent("""\ + git checkout for cleaning files failed with error code: {} + on file {} + stderr: {} + """.format(cleaned.returncode, header_file, cleaned.stderr))) + + header_path_part = header_file.replace(os.sep, "_") + path_name = "auto_patch_" + header_path_part + ".patch" + path_name = os.path.join(PATCHES_DIR, path_name) + if patch.stdout: + with open(path_name, "w") as patch_file: + patch_file.write(patch.stdout) + + +def create_patches(headers): + defines = find_all_defines() + + if not header_dirty(headers): + for header in headers: + create_patch(defines, header) + else: + raise DirtyGitError(textwrap.dedent("""\ + It seems like one of the header files is in dirty state. + This script cannot patch files in dirty state. + """)) + +# Invoke 'python3 -m unittest compute_patch.py" for running tests. +class TestDefineRegexes(unittest.TestCase): + def test_makefile_regex(self): + input1 = "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}" + input2 = "ipconfigETHERNET_MINIMUM_PACKET_BYTES=50" + input3 = "'configASSERT(X)=__CPROVER_assert(x, \"must hold\")'" + input4 = '"configASSERT (X)=__CPROVER_assert(x, "must hold")"' + input5 = "configASSERT(X)=__CPROVER_assert(x,\"must hold\")" + + match1 = DEFINE_REGEX_MAKEFILE.match(input1) + match2 = DEFINE_REGEX_MAKEFILE.match(input2) + match3 = DEFINE_REGEX_MAKEFILE.match(input3) + match4 = DEFINE_REGEX_MAKEFILE.match(input4) + match5 = DEFINE_REGEX_MAKEFILE.match(input5) + + self.assertIsNotNone(match1) + self.assertIsNotNone(match2) + self.assertIsNotNone(match3) + self.assertIsNotNone(match4) + self.assertIsNotNone(match5) + + self.assertEqual(match1.group(1), + "ipconfigETHERNET_MINIMUM_PACKET_BYTES") + self.assertEqual(match2.group(1), + "ipconfigETHERNET_MINIMUM_PACKET_BYTES") + self.assertEqual(match3.group(1), "configASSERT") + self.assertEqual(match4.group(1), "configASSERT") + self.assertEqual(match5.group(1), "configASSERT") + + + def test_header_regex(self): + input1 = ("#define configASSERT( x ) if( ( x ) == 0 )" + + "vAssertCalled( __FILE__, __LINE__ )") + input2 = "#define ipconfigMAX_ARP_RETRANSMISSIONS ( 5 )" + input3 = "#define ipconfigINCLUDE_FULL_INET_ADDR 1" + + match1 = DEFINE_REGEX_HEADER.match(input1) + match2 = DEFINE_REGEX_HEADER.match(input2) + match3 = DEFINE_REGEX_HEADER.match(input3) + + self.assertIsNotNone(match1) + self.assertIsNotNone(match2) + self.assertIsNotNone(match3) + + self.assertEqual(match1.group(1), "configASSERT") + self.assertEqual(match2.group(1), "ipconfigMAX_ARP_RETRANSMISSIONS") + self.assertEqual(match3.group(1), "ipconfigINCLUDE_FULL_INET_ADDR") + +if __name__ == '__main__': + create_patches(HEADERS) diff --git a/FreeRTOS-Plus/Test/CBMC/patches/patch.py b/FreeRTOS-Plus/Test/CBMC/patches/patch.py new file mode 100755 index 000000000..c2c0883a3 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/patch.py @@ -0,0 +1,36 @@ +#!/usr/bin/env python3 + +import logging +import os +import subprocess +import sys +from glob import glob + +from patches_constants import PATCHES_DIR + +def patch(): + if os.path.isfile("patched"): + sys.exit() + + applied_patches = [] + failed_patches = [] + for tmpfile in glob(os.path.join(PATCHES_DIR, "*.patch")): + print("patch", tmpfile) + result = subprocess.run(["git", "apply", "--ignore-space-change", "--ignore-whitespace", tmpfile], + cwd=os.path.join("..", "..", "..", "..")) + if result.returncode: + failed_patches.append(tmpfile) + logging.error("patching failed: %s", tmpfile) + else: + applied_patches.append(tmpfile) + + with open(os.path.join(PATCHES_DIR, "patched"), "w") as outp: + print("Success:", file=outp) + print("\n".join(map(lambda x: "\t" + x, applied_patches)), file=outp) + + print("Failure:", file=outp) + print("\n".join(map(lambda x: "\t" + x, failed_patches)), file=outp) + + +if __name__ == "__main__": + patch() diff --git a/FreeRTOS-Plus/Test/CBMC/patches/patches_constants.py b/FreeRTOS-Plus/Test/CBMC/patches/patches_constants.py new file mode 100755 index 000000000..1093e6538 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/patches_constants.py @@ -0,0 +1,42 @@ +#!/usr/bin/env python3 +# +# Constants for the generation of patches 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 os + +PATCHES_DIR = os.path.dirname(os.path.abspath(__file__)) + + +shared_prefix = [ + "." +] +shared_prefix_port = [ + "..", "..", "..", "..", "FreeRTOS", "Source", "portable", "MSVC-MingW" +] + +absolute_prefix = os.path.abspath(os.path.join(PATCHES_DIR, *shared_prefix)) +absolute_prefix_port = os.path.abspath(os.path.join(PATCHES_DIR, *shared_prefix_port)) + +HEADERS = [os.path.join(absolute_prefix, "FreeRTOSConfig.h"), + os.path.join(absolute_prefix, "FreeRTOSIPConfig.h"), + os.path.join(absolute_prefix_port, "portmacro.h")] diff --git a/FreeRTOS-Plus/Test/CBMC/patches/unpatch.py b/FreeRTOS-Plus/Test/CBMC/patches/unpatch.py new file mode 100755 index 000000000..2162971fd --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/unpatch.py @@ -0,0 +1,42 @@ +#!/usr/bin/env python3 +# +# unpatching changes 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 subprocess +import os +import sys +from glob import glob + +from patches_constants import PATCHES_DIR + +try: + os.remove(os.path.join(PATCHES_DIR, "patched")) +except FileNotFoundError: + print("Nothing to do here.") + sys.exit(0) +for tmpfile in glob(os.path.join(PATCHES_DIR, "*.patch")): + print("unpatch", tmpfile) + result = subprocess.run(["git", "apply", "-R", "--ignore-space-change", "--ignore-whitespace", tmpfile], + cwd=os.path.join("..", "..", "..", "..")) + if result.returncode: + print("Unpatching failed: {}".format(tmpfile)) 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)); +} diff --git a/FreeRTOS-Plus/Test/CBMC/stubs/cbmc.c b/FreeRTOS-Plus/Test/CBMC/stubs/cbmc.c new file mode 100644 index 000000000..73ad21893 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/stubs/cbmc.c @@ -0,0 +1,12 @@ +#include "cbmc.h" + +/**************************************************************** + * Model a malloc that can fail (CBMC malloc does not fail) and + * check that CBMC can model an object of the requested size. + ****************************************************************/ + +void * safeMalloc( size_t size ) +{ + __CPROVER_assert( size < CBMC_MAX_OBJECT_SIZE, "safeMalloc size too big" ); + return nondet_bool() ? NULL : malloc( size ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.c b/FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.c new file mode 100644 index 000000000..668f8b941 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.c @@ -0,0 +1,379 @@ +/* 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_UDP_IP.h" +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_DNS.h" +#include "NetworkBufferManagement.h" + +#include "cbmc.h" + +/**************************************************************** + * This is a collection of abstractions of methods in the FreeRTOS TCP + * API. The abstractions simply perform minimal validation of + * function arguments, and return unconstrained values of the + * appropriate type. + ****************************************************************/ + +/**************************************************************** + * Abstract FreeRTOS_socket. + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/socket.html + * + * We stub out this function to do nothing but allocate space for a + * socket containing unconstrained data or return an error. + ****************************************************************/ + +Socket_t FreeRTOS_socket( BaseType_t xDomain, + BaseType_t xType, + BaseType_t xProtocol ) +{ + return nondet_bool() ? + FREERTOS_INVALID_SOCKET : malloc( sizeof( Socket_t ) ); +} + +/**************************************************************** + * Abstract FreeRTOS_setsockopt. + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/setsockopt.html + ****************************************************************/ + +BaseType_t FreeRTOS_setsockopt( Socket_t xSocket, + int32_t lLevel, + int32_t lOptionName, + const void * pvOptionValue, + size_t uxOptionLength ) +{ + __CPROVER_assert( xSocket != NULL, + "FreeRTOS precondition: xSocket != NULL" ); + __CPROVER_assert( pvOptionValue != NULL, + "FreeRTOS precondition: pvOptionValue != NULL" ); + return nondet_BaseType(); +} + +/**************************************************************** + * Abstract FreeRTOS_closesocket. + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/close.html + ****************************************************************/ + +BaseType_t FreeRTOS_closesocket( Socket_t xSocket ) +{ + __CPROVER_assert( xSocket != NULL, + "FreeRTOS precondition: xSocket != NULL" ); + return nondet_BaseType(); +} + +/**************************************************************** + * Abstract FreeRTOS_bind. + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/bind.html + ****************************************************************/ + +BaseType_t FreeRTOS_bind( Socket_t xSocket, + struct freertos_sockaddr * pxAddress, + socklen_t xAddressLength ) +{ + __CPROVER_assert( xSocket != NULL, + "FreeRTOS precondition: xSocket != NULL" ); + __CPROVER_assert( pxAddress != NULL, + "FreeRTOS precondition: pxAddress != NULL" ); + return nondet_BaseType(); +} + +/**************************************************************** + * Abstract FreeRTOS_inet_addr. + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/inet_addr.html + ****************************************************************/ + +uint32_t FreeRTOS_inet_addr( const char * pcIPAddress ) +{ + __CPROVER_assert( pcIPAddress != NULL, + "FreeRTOS precondition: pcIPAddress != NULL" ); + return nondet_uint32(); +} + +/**************************************************************** + * Abstract FreeRTOS_recvfrom. + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/recvfrom.html + * + * We stub out this function to do nothing but allocate a buffer of + * unconstrained size containing unconstrained data and return the + * size (or return the size 0 if the allocation fails). + ****************************************************************/ + +int32_t FreeRTOS_recvfrom( Socket_t xSocket, + void * pvBuffer, + size_t uxBufferLength, + BaseType_t xFlags, + struct freertos_sockaddr * pxSourceAddress, + socklen_t * pxSourceAddressLength ) + +{ + /**************************************************************** + * "If the zero copy calling semantics are used (the ulFlasg + * parameter does not have the FREERTOS_ZERO_COPY bit set) then + * pvBuffer does not point to a buffer and xBufferLength is not + * used." This is from the documentation. + ****************************************************************/ + __CPROVER_assert( xFlags & FREERTOS_ZERO_COPY, "I can only do ZERO_COPY" ); + + __CPROVER_assert( pvBuffer != NULL, + "FreeRTOS precondition: pvBuffer != NULL" ); + + /**************************************************************** + * TODO: We need to check this out. + * + * The code calls recvfrom with these parameters NULL, it is not + * clear from the documentation that this is allowed. + ****************************************************************/ + #if 0 + __CPROVER_assert( pxSourceAddress != NULL, + "FreeRTOS precondition: pxSourceAddress != NULL" ); + __CPROVER_assert( pxSourceAddressLength != NULL, + "FreeRTOS precondition: pxSourceAddress != NULL" ); + #endif + + size_t payload_size; + __CPROVER_assume( payload_size + sizeof( UDPPacket_t ) + < CBMC_MAX_OBJECT_SIZE ); + + /**************************************************************** + * TODO: We need to make this lower bound explicit in the Makefile.json + * + * DNSMessage_t is a typedef in FreeRTOS_DNS.c + * sizeof(DNSMessage_t) = 6 * sizeof(uint16_t) + ****************************************************************/ + __CPROVER_assume( payload_size >= 6 * sizeof( uint16_t ) ); + + #ifdef CBMC_FREERTOS_RECVFROM_BUFFER_BOUND + __CPROVER_assume( payload_size <= CBMC_FREERTOS_RECVFROM_BUFFER_BOUND ); + #endif + + uint32_t buffer_size = payload_size + sizeof( UDPPacket_t ); + uint8_t *buffer = safeMalloc( buffer_size ); + + if ( buffer == NULL ) { + buffer_size = 0; + } + else + { + buffer = buffer + sizeof( UDPPacket_t ); + buffer_size = buffer_size - sizeof( UDPPacket_t ); + } + + *( ( uint8_t ** ) pvBuffer ) = buffer; + return buffer_size; +} + +/**************************************************************** + * Abstract FreeRTOS_recvfrom. + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/sendto.html + ****************************************************************/ + +int32_t FreeRTOS_sendto( Socket_t xSocket, + const void * pvBuffer, + size_t uxTotalDataLength, + BaseType_t xFlags, + const struct freertos_sockaddr * pxDestinationAddress, + socklen_t xDestinationAddressLength ) +{ + __CPROVER_assert( xSocket != NULL, + "FreeRTOS precondition: xSocket != NULL" ); + __CPROVER_assert( pvBuffer != NULL, + "FreeRTOS precondition: pvBuffer != NULL" ); + __CPROVER_assert( pxDestinationAddress != NULL, + "FreeRTOS precondition: pxDestinationAddress != NULL" ); + return nondet_int32(); +} + +/**************************************************************** + * Abstract FreeRTOS_GetUDPPayloadBuffer + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_UDP/API/FreeRTOS_GetUDPPayloadBuffer.html + * + * We stub out this function to do nothing but allocate a buffer of + * unconstrained size containing unconstrained data and return a + * pointer to the buffer (or NULL). + ****************************************************************/ + +void * FreeRTOS_GetUDPPayloadBuffer( size_t xRequestedSizeBytes, + TickType_t xBlockTimeTicks ) +{ + size_t size; + + __CPROVER_assume( size < CBMC_MAX_OBJECT_SIZE ); + __CPROVER_assume( size >= sizeof( UDPPacket_t ) ); + + uint8_t *buffer = safeMalloc( size ); + return buffer == NULL ? buffer : buffer + sizeof( UDPPacket_t ); +} + +/**************************************************************** + * Abstract FreeRTOS_GetUDPPayloadBuffer + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/FreeRTOS_ReleaseUDPPayloadBuffer.html + ****************************************************************/ + +void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer ) +{ + __CPROVER_assert( pvBuffer != NULL, + "FreeRTOS precondition: pvBuffer != NULL" ); + __CPROVER_assert( __CPROVER_POINTER_OFFSET( pvBuffer ) + == sizeof( UDPPacket_t ), + "FreeRTOS precondition: pvBuffer offset" ); + + free( pvBuffer - sizeof( UDPPacket_t ) ); +} + +/**************************************************************** + * Abstract pxGetNetworkBufferWithDescriptor. + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/pxGetNetworkBufferWithDescriptor.html + * + * The real allocator take buffers off a list. + ****************************************************************/ + +uint32_t GetNetworkBuffer_failure_count; + +NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, + TickType_t xBlockTimeTicks ) +{ + __CPROVER_assert( + xRequestedSizeBytes + ipBUFFER_PADDING < CBMC_MAX_OBJECT_SIZE, + "pxGetNetworkBufferWithDescriptor: request too big" ); + + /* + * The semantics of this function is to wait until a buffer with + * at least the requested number of bytes becomes available. If a + * timeout occurs before the buffer is available, then return a + * NULL pointer. + */ + + NetworkBufferDescriptor_t * desc = safeMalloc( sizeof( *desc ) ); + + #ifdef CBMC_GETNETWORKBUFFER_FAILURE_BOUND + /* + * This interprets the failure bound as being one greater than the + * actual number of times GetNetworkBuffer should be allowed to + * fail. + * + * This makes it possible to use the same bound for loop unrolling + * which must be one greater than the actual number of times the + * loop should be unwound. + * + * NOTE: Using this bound with --nondet-static requires setting + * (or assuming) GetNetworkBuffer_failure_count to a value (like 0) + * in the proof harness that won't induce an integer overflow. + */ + GetNetworkBuffer_failure_count++; + __CPROVER_assume( + IMPLIES( + GetNetworkBuffer_failure_count >= CBMC_GETNETWORKBUFFER_FAILURE_BOUND, + desc != NULL ) ); + #endif + + if( desc != NULL ) + { + /* + * We may want to experiment with allocating space other than + * (more than) the exact amount of space requested. + */ + + size_t size = xRequestedSizeBytes; + __CPROVER_assume( size < CBMC_MAX_OBJECT_SIZE ); + + desc->pucEthernetBuffer = safeMalloc( size ); + desc->xDataLength = desc->pucEthernetBuffer == NULL ? 0 : size; + + #ifdef CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL + /* This may be implied by the semantics of the function. */ + __CPROVER_assume( desc->pucEthernetBuffer != NULL ); + #endif + + /* Allow method to fail again next time */ + GetNetworkBuffer_failure_count = 0; + } + + return desc; +} + +/**************************************************************** + * Abstract pxGetNetworkBufferWithDescriptor. + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/vReleaseNetworkBufferAndDescriptor.html + ****************************************************************/ + +void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, + "Precondition: pxNetworkBuffer != NULL" ); + + if( pxNetworkBuffer->pucEthernetBuffer != NULL ) + { + free( pxNetworkBuffer->pucEthernetBuffer ); + } + + free( pxNetworkBuffer ); +} + +/**************************************************************** + * Abstract FreeRTOS_GetAddressConfiguration + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/FreeRTOS_GetAddressConfiguration.html + ****************************************************************/ + +void FreeRTOS_GetAddressConfiguration( uint32_t * pulIPAddress, + uint32_t * pulNetMask, + uint32_t * pulGatewayAddress, + uint32_t * pulDNSServerAddress ) +{ + if( pulIPAddress != NULL ) + { + *pulIPAddress = nondet_unint32(); + } + + if( pulNetMask != NULL ) + { + *pulNetMask = nondet_unint32(); + } + + if( pulGatewayAddress != NULL ) + { + *pulGatewayAddress = nondet_unint32(); + } + + if( pulDNSServerAddress != NULL ) + { + *pulDNSServerAddress = nondet_unint32(); + } +} + +/****************************************************************/ + +/**************************************************************** + * This is a collection of methods that are defined by the user + * application but are invoked by the FreeRTOS API. + ****************************************************************/ + +/**************************************************************** + * Abstract FreeRTOS_GetAddressConfiguration + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/vApplicationIPNetworkEventHook.html + ****************************************************************/ + +void vApplicationIPNetworkEventHook( eIPCallbackEvent_t eNetworkEvent ) +{ +} + +/**************************************************************** + * Abstract pcApplicationHostnameHook + * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_IP_Configuration.html + ****************************************************************/ + +const char * pcApplicationHostnameHook( void ) +{ + return "hostname"; +} + +/****************************************************************/ diff --git a/FreeRTOS-Plus/Test/CBMC/windows/README.md b/FreeRTOS-Plus/Test/CBMC/windows/README.md new file mode 100644 index 000000000..e9f415060 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/windows/README.md @@ -0,0 +1,2 @@ +This directory contains include files used by the CBMC proofs: +* Windows.h and WinBase.h are include files used to build FreeRTOS (the parts we currently test) on Linux
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/windows/WinBase.h b/FreeRTOS-Plus/Test/CBMC/windows/WinBase.h new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/windows/WinBase.h diff --git a/FreeRTOS-Plus/Test/CBMC/windows/Windows.h b/FreeRTOS-Plus/Test/CBMC/windows/Windows.h new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/windows/Windows.h diff --git a/FreeRTOS-Plus/Test/CBMC/windows/direct.h b/FreeRTOS-Plus/Test/CBMC/windows/direct.h new file mode 100644 index 000000000..8b1378917 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/windows/direct.h @@ -0,0 +1 @@ + diff --git a/FreeRTOS-Plus/Test/CBMC/windows2/windows.h b/FreeRTOS-Plus/Test/CBMC/windows2/windows.h new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/windows2/windows.h |