From 1fc1bd4321bf1720f46011a2d9fa350ca9e83b46 Mon Sep 17 00:00:00 2001 From: Ravishankar Bhagavandas Date: Thu, 24 Sep 2020 13:32:10 -0700 Subject: [PATCH] Add CBMC proofs for FreeRTOS-Plus-CLI (#296) --- .../Source/FreeRTOS-Plus-CLI/FreeRTOS_CLI.c | 4 +- .../FreeRTOS_CLIGetParameter_harness.c | 48 ++++++++++++++++++ .../FreeRTOS_CLIGetParameter/Makefile.json | 34 +++++++++++++ .../FreeRTOS_CLIProcessCommand_harness.c | 49 +++++++++++++++++++ .../FreeRTOS_CLIProcessCommand/Makefile.json | 40 +++++++++++++++ 5 files changed, 173 insertions(+), 2 deletions(-) create mode 100644 FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIGetParameter/FreeRTOS_CLIGetParameter_harness.c create mode 100644 FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIGetParameter/Makefile.json create mode 100644 FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIProcessCommand/FreeRTOS_CLIProcessCommand_harness.c create mode 100644 FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIProcessCommand/Makefile.json diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-CLI/FreeRTOS_CLI.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-CLI/FreeRTOS_CLI.c index a9770159c7..ded29b8faa 100644 --- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-CLI/FreeRTOS_CLI.c +++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-CLI/FreeRTOS_CLI.c @@ -165,9 +165,9 @@ size_t xCommandStringLength; a sub-string of a longer command, check the byte after the expected end of the string is either the end of the string or a space before a parameter. */ - if( ( pcCommandInput[ xCommandStringLength ] == ' ' ) || ( pcCommandInput[ xCommandStringLength ] == 0x00 ) ) + if( strncmp( pcCommandInput, pcRegisteredCommandString, xCommandStringLength ) == 0 ) { - if( strncmp( pcCommandInput, pcRegisteredCommandString, xCommandStringLength ) == 0 ) + if( ( pcCommandInput[ xCommandStringLength ] == ' ' ) || ( pcCommandInput[ xCommandStringLength ] == 0x00 ) ) { /* The command has been found. Check it has the expected number of parameters. If cExpectedNumberOfParameters is -1, diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIGetParameter/FreeRTOS_CLIGetParameter_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIGetParameter/FreeRTOS_CLIGetParameter_harness.c new file mode 100644 index 0000000000..781e5545e4 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIGetParameter/FreeRTOS_CLIGetParameter_harness.c @@ -0,0 +1,48 @@ +/* + * 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 +#include "FreeRTOS.h" +#include "FreeRTOS_CLI.h" + +#include "cbmc.h" + +void harness() { + + UBaseType_t xWantedParameter; + BaseType_t xParameterLength; + size_t commandStringLength; + + __CPROVER_assume ( commandStringLength > 0 && commandStringLength < CLI_INPUT_MAX_LENGTH ); + char * pcCommand = malloc( commandStringLength ); + + if( pcCommand ) { + pcCommand[ commandStringLength - 1U ] = '\0'; + FreeRTOS_CLIGetParameter( pcCommand, xWantedParameter, &xParameterLength ); + } + +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIGetParameter/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIGetParameter/Makefile.json new file mode 100644 index 0000000000..df883ebb4f --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIGetParameter/Makefile.json @@ -0,0 +1,34 @@ +{ + "ENTRY": "FreeRTOS_CLIGetParameter", + # CLI input command length is bounded here to bound overall loop iterations within + # the function under test. Function parses the input null terminated string to find + # parameters which are separated by one or more whitespaces. A longer input string + # does not add additional value in testing the memory safety of the function. + "CLI_INPUT_MAX_LENGTH": "5", + "CBMCFLAGS": + [ + # Setting unwind bound for all loops by 'CLI_INPUT_MAX_LENGTH' as in worst case all the + # loops iterates till end of the string. + "--unwind {CLI_INPUT_MAX_LENGTH}" + ], + + "OBJS": + [ + "FreeRTOS_CLIGetParameter_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-CLI/FreeRTOS_CLI.goto" + ], + "DEF": + [ + "_CONSOLE", + "_CRT_SECURE_NO_WARNINGS", + "__free_rtos__", + # Setting flag to assume input of maximum length 'CLI_INPUT_MAX_LENGTH' from the tests. + "CLI_INPUT_MAX_LENGTH={CLI_INPUT_MAX_LENGTH}" + ], + + "INC": + [ + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-CLI" + ] + } + diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIProcessCommand/FreeRTOS_CLIProcessCommand_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIProcessCommand/FreeRTOS_CLIProcessCommand_harness.c new file mode 100644 index 0000000000..c4d16a9225 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIProcessCommand/FreeRTOS_CLIProcessCommand_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 +#include "FreeRTOS.h" +#include "FreeRTOS_CLI.h" + +#include "cbmc.h" + +void harness() { + + size_t commandStringLength; + size_t outputBufferLength; + + __CPROVER_assume ( commandStringLength > 0 && commandStringLength < CLI_INPUT_MAX_LENGTH ); + __CPROVER_assume ( outputBufferLength > 0 && outputBufferLength < CLI_OUTPUT_MAX_LENGTH ); + char * pcCommand = malloc( commandStringLength ); + char * pcWriteBuffer = malloc( outputBufferLength ); + + if( pcCommand && pcWriteBuffer ) { + pcCommand[ commandStringLength - 1U ] = '\0'; + FreeRTOS_CLIProcessCommand( pcCommand, pcWriteBuffer, outputBufferLength ); + } + +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIProcessCommand/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIProcessCommand/Makefile.json new file mode 100644 index 0000000000..fb13ed7fa9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIProcessCommand/Makefile.json @@ -0,0 +1,40 @@ +{ + "ENTRY": "FreeRTOS_CLIProcessCommand", + # Bound the input command string to an acceptable value to test the memory + # safety of the funtion. The input string is compared against a pre-registered list of commands of + # finite length so a higher length will add to the runtime to the proof but will not add much value + # to test the memory safety of the function. + "CLI_INPUT_MAX_LENGTH": "256", + # Output length is limited to sufficient value inorder to check for all buffer overflows when CLI writes + # error logs to output buffer. + "CLI_OUTPUT_MAX_LENGTH": "32", + "CBMCFLAGS": + [ + "--unwind 2", + # Loop in strncpy is bounded to maximum length of the outputbuffer to which the error string is copied. + # prvGetNumberOfParameters is used to count number of parameters separated by whitespaces, the loop unwinding + # is bounded by maximum length of the input buffer. + "--unwindset strlen.0:10,strncmp.0:10,strncpy.0:{CLI_OUTPUT_MAX_LENGTH},prvGetNumberOfParameters.0:{CLI_INPUT_MAX_LENGTH}" + ], + + "OBJS": + [ + "FreeRTOS_CLIProcessCommand_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-CLI/FreeRTOS_CLI.goto" + ], + "DEF": + [ + "_CONSOLE", + "_CRT_SECURE_NO_WARNINGS", + "__free_rtos__", + # Pass the flags for maximum input and output length to test inorder to bound inputs within this limit. + "CLI_INPUT_MAX_LENGTH={CLI_INPUT_MAX_LENGTH}", + "CLI_OUTPUT_MAX_LENGTH={CLI_OUTPUT_MAX_LENGTH}" + ], + + "INC": + [ + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-CLI" + ] + } +