github-forks
/
FreeRTOS
mirror of https://github.com/FreeRTOS/FreeRTOS.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Add CBMC proofs for FreeRTOS-Plus-CLI (#296)

Browse Source
pull/286/head
Ravishankar Bhagavandas 4 years ago committed by GitHub
parent de502afcb2
commit 1fc1bd4321
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 173 additions and 2 deletions
Show Stats Download Patch File Download Diff File

4
FreeRTOS-Plus/Source/FreeRTOS-Plus-CLI/FreeRTOS_CLI.c
Unescape Escape View File

@ -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,

48
FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIGetParameter/FreeRTOS_CLIGetParameter_harness.c
Unescape Escape View File

@ -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 <stddef.h>
#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 );
}
}

34
FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIGetParameter/Makefile.json
Unescape Escape View File

@ -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"
]
}

49
FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIProcessCommand/FreeRTOS_CLIProcessCommand_harness.c
Unescape Escape View File

@ -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 <stddef.h>
#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 );
}
}

40
FreeRTOS-Plus/Test/CBMC/proofs/CLI/FreeRTOS_CLIProcessCommand/Makefile.json
Unescape Escape View File

@ -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"
]
}
Write Preview
Loading…
Cancel
Save