diff --git a/test/cbmc/proofs/BitConfig/BitConfigInit/BitConfigInit_harness.c b/test/cbmc/proofs/BitConfig/BitConfigInit/BitConfigInit_harness.c new file mode 100644 index 0000000000..dfb8337318 --- /dev/null +++ b/test/cbmc/proofs/BitConfig/BitConfigInit/BitConfigInit_harness.c @@ -0,0 +1,72 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2022 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* Standard includes. */ +#include + +/* cbmc.h pulls in FreeRTOS.h and the +TCP headers that define the base + * types (BaseType_t, size_t, ...) that FreeRTOS_BitConfig.h relies on, so + * it MUST be included first. */ +#include "cbmc.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_BitConfig.h" + +/**************************************************************** +* Signature of function under test +****************************************************************/ + +BaseType_t xBitConfig_init( BitConfig_t * pxConfig, + const uint8_t * pucData, + size_t uxSize ); + +/**************************************************************** +* Proof of xBitConfig_init memory safety. +* +* Minimal assumptions: +* - pxConfig points to a valid (stack) BitConfig_t; the function +* memset()s it fully before use. +* - uxSize is nondeterministic, bounded only to keep the CBMC object +* model finite. +* - pucData is EITHER NULL (memset path) OR a buffer of EXACTLY uxSize +* bytes (memcpy path). safeMalloc returns NULL or malloc(uxSize), so +* both branches are explored and any over-read of pucData is genuine. +****************************************************************/ + +void harness() +{ + BitConfig_t xConfig; + size_t uxSize; + + __CPROVER_assume( uxSize <= 32 ); + + /* Source buffer is either NULL or allocated to EXACTLY uxSize bytes. */ + const uint8_t * pucData = ( const uint8_t * ) safeMalloc( uxSize ); + + ( void ) xBitConfig_init( &xConfig, pucData, uxSize ); +} diff --git a/test/cbmc/proofs/BitConfig/BitConfigInit/Makefile.json b/test/cbmc/proofs/BitConfig/BitConfigInit/Makefile.json new file mode 100644 index 0000000000..38b630cc3c --- /dev/null +++ b/test/cbmc/proofs/BitConfig/BitConfigInit/Makefile.json @@ -0,0 +1,21 @@ +{ + "ENTRY": "BitConfigInit", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "INSTFLAGS": + [ + "--malloc-may-fail" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto" + ], + "DEF": + [ + "ipconfigUSE_DHCPv6=1" + ] +} diff --git a/test/cbmc/proofs/BitConfig/BitConfigPeekLast/BitConfigPeekLast_harness.c b/test/cbmc/proofs/BitConfig/BitConfigPeekLast/BitConfigPeekLast_harness.c new file mode 100644 index 0000000000..3fa70121a3 --- /dev/null +++ b/test/cbmc/proofs/BitConfig/BitConfigPeekLast/BitConfigPeekLast_harness.c @@ -0,0 +1,83 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2022 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* Standard includes. */ +#include + +/* cbmc.h pulls in FreeRTOS.h and the +TCP headers that define the base + * types (BaseType_t, size_t, ...) that FreeRTOS_BitConfig.h relies on, so + * it MUST be included first. */ +#include "cbmc.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_BitConfig.h" + +/**************************************************************** +* Signature of function under test +****************************************************************/ + +BaseType_t pucBitConfig_peek_last_index_uc( BitConfig_t * pxConfig, + uint8_t * pucData, + size_t uxSize ); + +/**************************************************************** +* Proof of pucBitConfig_peek_last_index_uc memory safety. +* +* The function peeks uxSize bytes ending at the current index, reading +* from &ucContents[uxIndex - uxSize] when uxIndex >= uxSize. We model +* any REACHABLE BitConfig_t: +* - ucContents allocated to EXACTLY uxSize_buf bytes (over-read => genuine). +* - uxIndex nondeterministic but within the maintained invariant +* 0 <= uxIndex <= uxSize_buf, so the backward peek boundary is exercised. +* - xHasError nondeterministic. +* - The peek length and destination are nondeterministic; the destination +* is either NULL or EXACTLY uxPeekLen bytes. +****************************************************************/ + +void harness() +{ + BitConfig_t xConfig; + size_t uxSize; + + __CPROVER_assume( uxSize <= 32 ); + + xConfig.ucContents = ( uint8_t * ) malloc( uxSize ); + __CPROVER_assume( xConfig.ucContents != NULL ); + xConfig.uxSize = uxSize; + xConfig.uxIndex = nondet_sizet(); + __CPROVER_assume( xConfig.uxIndex <= uxSize ); + xConfig.xHasError = nondet_basetype(); + + size_t uxPeekLen; + __CPROVER_assume( uxPeekLen <= 32 ); + + /* Destination is either NULL or allocated to EXACTLY uxPeekLen bytes. */ + uint8_t * pucData = ( uint8_t * ) safeMalloc( uxPeekLen ); + + ( void ) pucBitConfig_peek_last_index_uc( &xConfig, pucData, uxPeekLen ); +} diff --git a/test/cbmc/proofs/BitConfig/BitConfigPeekLast/Makefile.json b/test/cbmc/proofs/BitConfig/BitConfigPeekLast/Makefile.json new file mode 100644 index 0000000000..14a425a3aa --- /dev/null +++ b/test/cbmc/proofs/BitConfig/BitConfigPeekLast/Makefile.json @@ -0,0 +1,21 @@ +{ + "ENTRY": "BitConfigPeekLast", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "INSTFLAGS": + [ + "--malloc-may-fail" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto" + ], + "DEF": + [ + "ipconfigUSE_DHCPv6=1" + ] +} diff --git a/test/cbmc/proofs/BitConfig/BitConfigRead16/BitConfigRead16_harness.c b/test/cbmc/proofs/BitConfig/BitConfigRead16/BitConfigRead16_harness.c new file mode 100644 index 0000000000..d17139e36f --- /dev/null +++ b/test/cbmc/proofs/BitConfig/BitConfigRead16/BitConfigRead16_harness.c @@ -0,0 +1,72 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2022 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* Standard includes. */ +#include + +/* cbmc.h pulls in FreeRTOS.h and the +TCP headers that define the base + * types (BaseType_t, size_t, ...) that FreeRTOS_BitConfig.h relies on, so + * it MUST be included first. */ +#include "cbmc.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_BitConfig.h" + +/**************************************************************** +* Signature of function under test +****************************************************************/ + +uint16_t usBitConfig_read_16( BitConfig_t * pxConfig ); + +/**************************************************************** +* Proof of usBitConfig_read_16 memory safety. +* +* usBitConfig_read_16 reads sizeof(uint16_t) bytes via xBitConfig_read_uc +* into a local stack buffer. We model any REACHABLE BitConfig_t: +* - ucContents allocated to EXACTLY uxSize bytes (over-read => genuine). +* - uxIndex nondeterministic but within the maintained invariant +* 0 <= uxIndex <= uxSize, so the read boundary is exercised. +* - xHasError nondeterministic. +****************************************************************/ + +void harness() +{ + BitConfig_t xConfig; + size_t uxSize; + + __CPROVER_assume( uxSize <= 32 ); + + xConfig.ucContents = ( uint8_t * ) malloc( uxSize ); + __CPROVER_assume( xConfig.ucContents != NULL ); + xConfig.uxSize = uxSize; + xConfig.uxIndex = nondet_sizet(); + __CPROVER_assume( xConfig.uxIndex <= uxSize ); + xConfig.xHasError = nondet_basetype(); + + ( void ) usBitConfig_read_16( &xConfig ); +} diff --git a/test/cbmc/proofs/BitConfig/BitConfigRead16/Makefile.json b/test/cbmc/proofs/BitConfig/BitConfigRead16/Makefile.json new file mode 100644 index 0000000000..000b5cd1c9 --- /dev/null +++ b/test/cbmc/proofs/BitConfig/BitConfigRead16/Makefile.json @@ -0,0 +1,21 @@ +{ + "ENTRY": "BitConfigRead16", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "INSTFLAGS": + [ + "--malloc-may-fail" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto" + ], + "DEF": + [ + "ipconfigUSE_DHCPv6=1" + ] +} diff --git a/test/cbmc/proofs/BitConfig/BitConfigRead32/BitConfigRead32_harness.c b/test/cbmc/proofs/BitConfig/BitConfigRead32/BitConfigRead32_harness.c new file mode 100644 index 0000000000..da050c14f8 --- /dev/null +++ b/test/cbmc/proofs/BitConfig/BitConfigRead32/BitConfigRead32_harness.c @@ -0,0 +1,72 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2022 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* Standard includes. */ +#include + +/* cbmc.h pulls in FreeRTOS.h and the +TCP headers that define the base + * types (BaseType_t, size_t, ...) that FreeRTOS_BitConfig.h relies on, so + * it MUST be included first. */ +#include "cbmc.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_BitConfig.h" + +/**************************************************************** +* Signature of function under test +****************************************************************/ + +uint32_t ulBitConfig_read_32( BitConfig_t * pxConfig ); + +/**************************************************************** +* Proof of ulBitConfig_read_32 memory safety. +* +* ulBitConfig_read_32 reads sizeof(uint32_t) bytes via xBitConfig_read_uc +* into a local stack buffer. We model any REACHABLE BitConfig_t: +* - ucContents allocated to EXACTLY uxSize bytes (over-read => genuine). +* - uxIndex nondeterministic but within the maintained invariant +* 0 <= uxIndex <= uxSize, so the read boundary is exercised. +* - xHasError nondeterministic. +****************************************************************/ + +void harness() +{ + BitConfig_t xConfig; + size_t uxSize; + + __CPROVER_assume( uxSize <= 32 ); + + xConfig.ucContents = ( uint8_t * ) malloc( uxSize ); + __CPROVER_assume( xConfig.ucContents != NULL ); + xConfig.uxSize = uxSize; + xConfig.uxIndex = nondet_sizet(); + __CPROVER_assume( xConfig.uxIndex <= uxSize ); + xConfig.xHasError = nondet_basetype(); + + ( void ) ulBitConfig_read_32( &xConfig ); +} diff --git a/test/cbmc/proofs/BitConfig/BitConfigRead32/Makefile.json b/test/cbmc/proofs/BitConfig/BitConfigRead32/Makefile.json new file mode 100644 index 0000000000..74b3c695a4 --- /dev/null +++ b/test/cbmc/proofs/BitConfig/BitConfigRead32/Makefile.json @@ -0,0 +1,21 @@ +{ + "ENTRY": "BitConfigRead32", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "INSTFLAGS": + [ + "--malloc-may-fail" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto" + ], + "DEF": + [ + "ipconfigUSE_DHCPv6=1" + ] +} diff --git a/test/cbmc/proofs/BitConfig/BitConfigRead8/BitConfigRead8_harness.c b/test/cbmc/proofs/BitConfig/BitConfigRead8/BitConfigRead8_harness.c new file mode 100644 index 0000000000..23cdd7030d --- /dev/null +++ b/test/cbmc/proofs/BitConfig/BitConfigRead8/BitConfigRead8_harness.c @@ -0,0 +1,72 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2022 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* Standard includes. */ +#include + +/* cbmc.h pulls in FreeRTOS.h and the +TCP headers that define the base + * types (BaseType_t, size_t, ...) that FreeRTOS_BitConfig.h relies on, so + * it MUST be included first. */ +#include "cbmc.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_BitConfig.h" + +/**************************************************************** +* Signature of function under test +****************************************************************/ + +uint8_t ucBitConfig_read_8( BitConfig_t * pxConfig ); + +/**************************************************************** +* Proof of ucBitConfig_read_8 memory safety. +* +* ucBitConfig_read_8 reads sizeof(uint8_t) bytes via xBitConfig_read_uc +* into a local stack buffer. We model any REACHABLE BitConfig_t: +* - ucContents allocated to EXACTLY uxSize bytes (over-read => genuine). +* - uxIndex nondeterministic but within the maintained invariant +* 0 <= uxIndex <= uxSize, so the read boundary is exercised. +* - xHasError nondeterministic. +****************************************************************/ + +void harness() +{ + BitConfig_t xConfig; + size_t uxSize; + + __CPROVER_assume( uxSize <= 32 ); + + xConfig.ucContents = ( uint8_t * ) malloc( uxSize ); + __CPROVER_assume( xConfig.ucContents != NULL ); + xConfig.uxSize = uxSize; + xConfig.uxIndex = nondet_sizet(); + __CPROVER_assume( xConfig.uxIndex <= uxSize ); + xConfig.xHasError = nondet_basetype(); + + ( void ) ucBitConfig_read_8( &xConfig ); +} diff --git a/test/cbmc/proofs/BitConfig/BitConfigRead8/Makefile.json b/test/cbmc/proofs/BitConfig/BitConfigRead8/Makefile.json new file mode 100644 index 0000000000..4bf4299175 --- /dev/null +++ b/test/cbmc/proofs/BitConfig/BitConfigRead8/Makefile.json @@ -0,0 +1,21 @@ +{ + "ENTRY": "BitConfigRead8", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "INSTFLAGS": + [ + "--malloc-may-fail" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto" + ], + "DEF": + [ + "ipconfigUSE_DHCPv6=1" + ] +} diff --git a/test/cbmc/proofs/BitConfig/BitConfigReadUC/BitConfigReadUC_harness.c b/test/cbmc/proofs/BitConfig/BitConfigReadUC/BitConfigReadUC_harness.c new file mode 100644 index 0000000000..2133df4c28 --- /dev/null +++ b/test/cbmc/proofs/BitConfig/BitConfigReadUC/BitConfigReadUC_harness.c @@ -0,0 +1,85 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2022 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* Standard includes. */ +#include + +/* cbmc.h pulls in FreeRTOS.h and the +TCP headers that define the base + * types (BaseType_t, size_t, ...) that FreeRTOS_BitConfig.h relies on, so + * it MUST be included first. */ +#include "cbmc.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_BitConfig.h" + +/**************************************************************** +* Signature of function under test +****************************************************************/ + +BaseType_t xBitConfig_read_uc( BitConfig_t * pxConfig, + uint8_t * pucData, + size_t uxSize ); + +/**************************************************************** +* Proof of xBitConfig_read_uc memory safety. +* +* Minimal assumptions modelling any REACHABLE BitConfig_t: +* - ucContents is allocated to EXACTLY uxSize bytes, so any read past +* the end is a genuine over-read, not a harness artifact. +* - uxIndex satisfies the invariant maintained by xBitConfig_init and +* the read/write functions: 0 <= uxIndex <= uxSize. It is otherwise +* nondeterministic so the read boundary (uxIndex + uxSize <= uxSize) +* is fully exercised. +* - xHasError is nondeterministic (both the error and non-error entry +* states are explored). +* - The read length and destination buffer are nondeterministic; the +* destination is either NULL (skip path) or EXACTLY uxReadLen bytes. +****************************************************************/ + +void harness() +{ + BitConfig_t xConfig; + size_t uxSize; + + __CPROVER_assume( uxSize <= 32 ); + + xConfig.ucContents = ( uint8_t * ) malloc( uxSize ); + __CPROVER_assume( xConfig.ucContents != NULL ); + xConfig.uxSize = uxSize; + xConfig.uxIndex = nondet_sizet(); + __CPROVER_assume( xConfig.uxIndex <= uxSize ); + xConfig.xHasError = nondet_basetype(); + + size_t uxReadLen; + __CPROVER_assume( uxReadLen <= 32 ); + + /* Destination is either NULL (skip) or allocated to EXACTLY uxReadLen. */ + uint8_t * pucData = ( uint8_t * ) safeMalloc( uxReadLen ); + + ( void ) xBitConfig_read_uc( &xConfig, pucData, uxReadLen ); +} diff --git a/test/cbmc/proofs/BitConfig/BitConfigReadUC/Makefile.json b/test/cbmc/proofs/BitConfig/BitConfigReadUC/Makefile.json new file mode 100644 index 0000000000..6fac4cbf40 --- /dev/null +++ b/test/cbmc/proofs/BitConfig/BitConfigReadUC/Makefile.json @@ -0,0 +1,21 @@ +{ + "ENTRY": "BitConfigReadUC", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "INSTFLAGS": + [ + "--malloc-may-fail" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto" + ], + "DEF": + [ + "ipconfigUSE_DHCPv6=1" + ] +} diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleStatusCode/DHCPv6HandleStatusCode_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6HandleStatusCode/DHCPv6HandleStatusCode_harness.c new file mode 100644 index 0000000000..d9338e9087 --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6HandleStatusCode/DHCPv6HandleStatusCode_harness.c @@ -0,0 +1,66 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2022 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * SPDX-License-Identifier: MIT + * http://www.FreeRTOS.org + */ + +/* Standard includes. */ +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#include "FreeRTOS_DHCPv6.h" +#include "FreeRTOS_BitConfig.h" + +/* CBMC includes. */ +#include "cbmc.h" + +/* Bound the modeled receive buffer to keep the state space finite. + * The real DHCPv6 payload is MTU-bounded; 100 matches DHCPv6Analyse. */ +#define DHCPv6_PAYLOAD_LENGTH_MAX ( 100 ) + +/* Target: file-local static in FreeRTOS_DHCPv6.c, reached via + * --export-file-local-symbols. Reads a 16-bit status from the wire, then + * copies up to sizeof(ucMessage)-1 bytes into a local ucMessage[50]. The + * real BitConfig reader (bounds-checked) is linked, NOT stubbed. */ +BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleStatusCode( size_t uxLength, + BitConfig_t * pxMessage ); + +void harness() +{ + BitConfig_t * pxMessage = safeMalloc( sizeof( BitConfig_t ) ); + size_t uxSize; + size_t uxLength; + + __CPROVER_assume( pxMessage != NULL ); + + /* Model the bit-stream: buffer allocated to EXACTLY uxSize so any + * over-read is a genuine out-of-bounds access. Contents are the nondet + * bytes returned by malloc (attacker-controlled). */ + __CPROVER_assume( ( uxSize > 0U ) && ( uxSize <= DHCPv6_PAYLOAD_LENGTH_MAX ) ); + pxMessage->ucContents = safeMalloc( uxSize ); + __CPROVER_assume( pxMessage->ucContents != NULL ); + pxMessage->uxSize = uxSize; + + /* The read cursor may sit anywhere within the buffer (mid-parse). */ + __CPROVER_assume( pxMessage->uxIndex <= uxSize ); + + /* Parsing only continues while no prior read error occurred. */ + pxMessage->xHasError = pdFALSE; + + /* uxLength is the attacker-supplied option length. Leave it FULLY + * non-deterministic (including < 2, which underflows uxLength - 2U in + * the source) so the clamp arithmetic is exercised. */ + ( void ) __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleStatusCode( uxLength, pxMessage ); +} diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleStatusCode/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6HandleStatusCode/Makefile.json new file mode 100644 index 0000000000..844044430c --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6HandleStatusCode/Makefile.json @@ -0,0 +1,27 @@ +{ + "ENTRY": "DHCPv6HandleStatusCode", + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static --flush" + ], + "INSTFLAGS": + [ + "--malloc-may-fail" + ], + "OPT": + [ + "--export-file-local-symbols" + ], + "DEF": + [ + "ipconfigUSE_DHCPv6=1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto" + ] +} diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6IsOptionLengthValid/DHCPv6IsOptionLengthValid_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6IsOptionLengthValid/DHCPv6IsOptionLengthValid_harness.c new file mode 100644 index 0000000000..4429bb22ce --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6IsOptionLengthValid/DHCPv6IsOptionLengthValid_harness.c @@ -0,0 +1,46 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2022 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * SPDX-License-Identifier: MIT + * http://www.FreeRTOS.org + */ + +/* Standard includes. */ +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#include "FreeRTOS_DHCPv6.h" +#include "FreeRTOS_BitConfig.h" + +/* CBMC includes. */ +#include "cbmc.h" + +/* Target: file-local static in FreeRTOS_DHCPv6.c. Exposed via + * --export-file-local-symbols. This function is pure arithmetic on + * attacker-controlled length fields; it performs NO pointer dereference. + * Minimal assumptions: all three inputs are fully non-deterministic. */ +BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvIsOptionLengthValid( uint16_t usOption, + size_t uxOptionLength, + size_t uxRemainingSize ); + +void harness() +{ + uint16_t usOption; + size_t uxOptionLength; + size_t uxRemainingSize; + + ( void ) __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvIsOptionLengthValid( usOption, + uxOptionLength, + uxRemainingSize ); +} diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6IsOptionLengthValid/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6IsOptionLengthValid/Makefile.json new file mode 100644 index 0000000000..e3d857edda --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6IsOptionLengthValid/Makefile.json @@ -0,0 +1,22 @@ +{ + "ENTRY": "DHCPv6IsOptionLengthValid", + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static --flush" + ], + "OPT": + [ + "--export-file-local-symbols" + ], + "DEF": + [ + "ipconfigUSE_DHCPv6=1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto" + ] +} diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6SubOption/DHCPv6SubOption_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6SubOption/DHCPv6SubOption_harness.c new file mode 100644 index 0000000000..fe2a553db7 --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6SubOption/DHCPv6SubOption_harness.c @@ -0,0 +1,80 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2022 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * SPDX-License-Identifier: MIT + * http://www.FreeRTOS.org + */ + +/* Standard includes. */ +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#include "FreeRTOS_DHCPv6.h" +#include "FreeRTOS_BitConfig.h" + +/* CBMC includes. */ +#include "cbmc.h" + +/* Bound the modeled receive buffer to keep the state space finite. */ +#define DHCPv6_PAYLOAD_LENGTH_MAX ( 100 ) + +/* Bound the attacker-supplied option length. The sub-option scan loop + * consumes at least 4 bytes (option code + length) per iteration, so the + * loop runs at most OPTION_LENGTH_MAX/4 times. Must be covered by the + * --unwindset in Makefile.json for soundness. */ +#define OPTION_LENGTH_MAX ( 32 ) + +/* Target: file-local static in FreeRTOS_DHCPv6.c, reached via + * --export-file-local-symbols. Real BitConfig readers are linked (not + * stubbed) so the length-validation arithmetic runs against real memory. */ +BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_subOption( uint16_t usOption, + const DHCPOptionSet_t * pxSet, + DHCPMessage_IPv6_t * pxDHCPMessage, + BitConfig_t * pxMessage ); + +void harness() +{ + uint16_t usOption; + DHCPMessage_IPv6_t * pxDHCPMessage = safeMalloc( sizeof( DHCPMessage_IPv6_t ) ); + DHCPOptionSet_t * pxSet = safeMalloc( sizeof( DHCPOptionSet_t ) ); + BitConfig_t * pxMessage = safeMalloc( sizeof( BitConfig_t ) ); + size_t uxSize; + + __CPROVER_assume( pxDHCPMessage != NULL ); + __CPROVER_assume( pxSet != NULL ); + __CPROVER_assume( pxMessage != NULL ); + + /* Model the bit-stream: buffer allocated to EXACTLY uxSize so any + * over-read is a genuine out-of-bounds access. Contents nondet. */ + __CPROVER_assume( ( uxSize > 0U ) && ( uxSize <= DHCPv6_PAYLOAD_LENGTH_MAX ) ); + pxMessage->ucContents = safeMalloc( uxSize ); + __CPROVER_assume( pxMessage->ucContents != NULL ); + pxMessage->uxSize = uxSize; + __CPROVER_assume( pxMessage->uxIndex <= uxSize ); + pxMessage->xHasError = pdFALSE; + + /* pxSet describes the current option. uxStart is left non-deterministic + * (the source tolerates uxIndex < uxStart via the >= guard). Only + * uxOptionLength is bounded, purely to keep the scan loop finite. */ + __CPROVER_assume( pxSet->uxOptionLength <= OPTION_LENGTH_MAX ); + + /* Match the caller's option-code range so the switch default is reached. */ + __CPROVER_assume( ( usOption >= DHCPv6_Option_Client_Identifier ) && + ( usOption <= DHCPv6_Option_IA_Prefix ) ); + + ( void ) __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_subOption( usOption, + pxSet, + pxDHCPMessage, + pxMessage ); +} diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6SubOption/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6SubOption/Makefile.json new file mode 100644 index 0000000000..7df0307963 --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6SubOption/Makefile.json @@ -0,0 +1,29 @@ +{ + "ENTRY": "DHCPv6SubOption", + "OPTION_LOOP_BOUND": 10, + "CBMCFLAGS": + [ + "--nondet-static --flush", + "--unwind 10", + "--unwindset __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_subOption.0:{OPTION_LOOP_BOUND}" + ], + "INSTFLAGS": + [ + "--malloc-may-fail" + ], + "OPT": + [ + "--export-file-local-symbols" + ], + "DEF": + [ + "ipconfigUSE_DHCPv6=1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto" + ] +} diff --git a/test/cbmc/proofs/DNS/parseDNSAnswer/Makefile.json b/test/cbmc/proofs/DNS/parseDNSAnswer/Makefile.json new file mode 100644 index 0000000000..43e65add6c --- /dev/null +++ b/test/cbmc/proofs/DNS/parseDNSAnswer/Makefile.json @@ -0,0 +1,54 @@ +{ + "ENTRY": "parseDNSAnswer", + +################################################################ +# Modeled length of the attacker-controlled DNS payload remaining to be +# parsed. Kept small to bound the name-parse / answer-record loops, but the +# buffer is allocated to EXACTLY this length with nondeterministic contents so +# any over-read is a real defect. 32 bytes is enough to hold a full AAAA +# answer record (name ref 2 + fixed header 10 + IPv6 address 16 = 28). + "NETWORK_BUFFER_SIZE": 32, + +################################################################ +# parseDNSAnswer.0 : the "for( x = 0; x < usAnswers; x++ )" answer loop. +# The function's own ANCOUNT sanity check forces +# usAnswers <= uxSourceBytesRemaining / (sizeof(DNSAnswerRecord_t)+3), +# i.e. <= 32/13 = 2 before the loop is entered, so 3 fully covers it. + "ANSWERLOOP": "parseDNSAnswer.0", + "ANSWERLOOP_UNWIND": "3", + +################################################################ +# DNS_SkipNameField.0 : the name-walk while loop (linked in for real from the +# same translation unit). Each iteration consumes >= 2 bytes, so +# (NETWORK_BUFFER_SIZE + 1) / 2 + 1 iterations soundly cover it. + "SKIPLOOP": "DNS_SkipNameField.0", + "SKIPLOOP_UNWIND": "17", + +################################################################ + + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset {ANSWERLOOP}:{ANSWERLOOP_UNWIND},{SKIPLOOP}:{SKIPLOOP_UNWIND}" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto" + ], + + "DEF": + [ + "NETWORK_BUFFER_SIZE={NETWORK_BUFFER_SIZE}", + "ipconfigUSE_LLMNR=1", + "ipconfigUSE_MDNS=1", + "ipconfigUSE_IPv4=1", + "ipconfigUSE_IPv6=1", + "ipconfigUSE_DNS_CACHE=0", + "ipconfigDNS_USE_CALLBACKS=0", + "ipconfigDNS_CACHE_NAME_LENGTH=16", + "ipconfigDNS_CACHE_ADDRESSES_PER_ENTRY=4" + ] +} diff --git a/test/cbmc/proofs/DNS/parseDNSAnswer/parseDNSAnswer_harness.c b/test/cbmc/proofs/DNS/parseDNSAnswer/parseDNSAnswer_harness.c new file mode 100644 index 0000000000..22734fe9ab --- /dev/null +++ b/test/cbmc/proofs/DNS/parseDNSAnswer/parseDNSAnswer_harness.c @@ -0,0 +1,135 @@ +/* + * FreeRTOS memory safety proof for parseDNSAnswer(). + * + * parseDNSAnswer() walks the "answer" records of a DNS response. Every byte + * it reads originates from an attacker-controlled UDP payload, so this proof + * models the buffer with fully nondeterministic contents and allocates it to + * EXACTLY the modeled remaining length: any read past pxSet->pucByte + + * pxSet->uxSourceBytesRemaining is therefore a genuine out-of-bounds bug, not + * a proof artifact. + */ + +/* Standard includes. */ +#include +#include + +/* 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 "FreeRTOS_DNS_Parser.h" +#include "FreeRTOS_DNS_Globals.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" +#include "IPTraceMacroDefaults.h" + +#include "cbmc.h" + +/**************************************************************** +* Signature of the function under test +****************************************************************/ + +uint32_t parseDNSAnswer( ParseSet_t * pxSet, + struct freertos_addrinfo ** ppxAddressInfo, + size_t * uxBytesRead ); + +/**************************************************************** +* Stubs for callees that live OUTSIDE FreeRTOS_DNS_Parser.c. +* DNS_SkipNameField lives in the same translation unit and is linked in +* for real (it is what advances pucByte over the name field), so it is +* NOT stubbed here. +****************************************************************/ + +/* usChar2u16 reads two bytes from the packet in host order. The exact value + * is irrelevant to memory safety, but the read itself must be in-bounds. */ +uint16_t usChar2u16( const uint8_t * pucPtr ) +{ + uint16_t ret; + + __CPROVER_assert( __CPROVER_r_ok( pucPtr, 2 ), "usChar2u16: 2 bytes must be legal to read" ); + return ret; +} + +/* Allocate a fresh addrinfo (or fail). The real function copies pcName and + * the address bytes; those copies are proved elsewhere. Returning nondet + * NULL / non-NULL exercises both linked-list insertion branches. */ +struct freertos_addrinfo * pxNew_AddrInfo( const char * pcName, + BaseType_t xFamily, + const uint8_t * pucAddress ) +{ + struct freertos_addrinfo * pxAddr; + + if( nondet_bool() ) + { + pxAddr = NULL; + } + else + { + pxAddr = safeMalloc( sizeof( struct freertos_addrinfo ) ); + __CPROVER_assume( pxAddr != NULL ); + pxAddr->ai_next = NULL; + } + + return pxAddr; +} + +/**************************************************************** +* Proof harness +****************************************************************/ + +void harness() +{ + ParseSet_t xSet; + struct freertos_addrinfo * pxAddressInfo = NULL; + struct freertos_addrinfo ** ppxAddressInfo; + size_t uxBytesRead; + size_t uxRemaining; + + /* Bound the modeled remaining length just enough to keep the name-parse + * and answer-record loops finite (mirrors the small payload bounds used by + * the DNS_ParseDNSReply proof). It is otherwise nondeterministic so the + * parser's length arithmetic is fully exercised. */ + __CPROVER_assume( uxRemaining <= NETWORK_BUFFER_SIZE ); + __CPROVER_assume( uxRemaining < CBMC_MAX_OBJECT_SIZE ); + + /* Start from a clean ParseSet_t, then set only the fields parseDNSAnswer + * reads. memset mirrors DNS_ParseDNSReply, which zero-inits the struct. */ + ( void ) memset( &xSet, 0, sizeof( xSet ) ); + + /* Allocate the packet buffer to EXACTLY the modeled remaining length. */ + xSet.pucByte = safeMalloc( uxRemaining ); + __CPROVER_assume( xSet.pucByte != NULL ); + + /* Establish the caller's invariant: pucByte points at the first + * unparsed byte and uxSourceBytesRemaining is the count of bytes that are + * legal to read from there onward. */ + xSet.uxSourceBytesRemaining = uxRemaining; + + /* Number of answer records claimed by the (attacker-controlled) header. */ + xSet.usAnswers = nondet_uint16(); + + /* Records already stored is bounded by its natural range. */ + xSet.usNumARecordsStored = nondet_uint16(); + + /* The linked-list tail pointer is wired to the local as the real caller + * does. */ + xSet.ppxLastAddress = &( xSet.pxLastAddress ); + + /* pxDNSMessageHeader is only dereferenced on the logging / cache path + * (usIdentifier). Give it a valid backing object. */ + xSet.pxDNSMessageHeader = safeMalloc( sizeof( DNSMessage_t ) ); + __CPROVER_assume( xSet.pxDNSMessageHeader != NULL ); + + ppxAddressInfo = &pxAddressInfo; + + ( void ) parseDNSAnswer( &xSet, ppxAddressInfo, &uxBytesRead ); +} diff --git a/test/cbmc/proofs/ICMP/ProcessICMPEchoReply/Makefile.json b/test/cbmc/proofs/ICMP/ProcessICMPEchoReply/Makefile.json new file mode 100644 index 0000000000..d499589dd5 --- /dev/null +++ b/test/cbmc/proofs/ICMP/ProcessICMPEchoReply/Makefile.json @@ -0,0 +1,23 @@ +{ + "ENTRY": "ProcessICMPEchoReply", + "ECHO_DATA_LOOP": 21, + "CBMCFLAGS": [ + "--unwind 1", + "--unwindset __CPROVER_file_local_FreeRTOS_ICMP_c_prvProcessICMPEchoReply.0:{ECHO_DATA_LOOP}", + "--nondet-static" + ], + "OPT": + [ + "--export-file-local-symbols" + ], + "DEF": + [ + "ipconfigSUPPORT_OUTGOING_PINGS=1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ICMP.goto" + ] +} diff --git a/test/cbmc/proofs/ICMP/ProcessICMPEchoReply/ProcessICMPEchoReply_harness.c b/test/cbmc/proofs/ICMP/ProcessICMPEchoReply/ProcessICMPEchoReply_harness.c new file mode 100644 index 0000000000..53ca605dbb --- /dev/null +++ b/test/cbmc/proofs/ICMP/ProcessICMPEchoReply/ProcessICMPEchoReply_harness.c @@ -0,0 +1,44 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" + +/* CBMC includes. */ +#include "cbmc.h" + +/* prvProcessICMPEchoReply() is file-local (static); exported for verification + * via --export-file-local-symbols. */ +void __CPROVER_file_local_FreeRTOS_ICMP_c_prvProcessICMPEchoReply( const NetworkBufferDescriptor_t * const pxNetworkBuffer ); + +/* Application hook invoked with the ping-reply result. Body does not matter. */ +void vApplicationPingReplyHook( ePingReplyStatus_t eStatus, + uint16_t usIdentifier ) +{ +} + +void harness() +{ + NetworkBufferDescriptor_t xNetworkBuffer; + size_t xDataLength; + + /* Minimal assumptions: the caller (ProcessICMPPacket) guarantees the frame + * is at least an ICMPPacket_t. Beyond that the length is nondeterministic. + * The data-scan loop is bounded by (xDataLength - headers), so capping the + * upper bound keeps the loop finite while leaving the wire-derived length + * field (usLength) fully nondeterministic. */ + __CPROVER_assume( ( xDataLength >= sizeof( ICMPPacket_t ) ) && + ( xDataLength <= ( sizeof( ICMPPacket_t ) + 20U ) ) ); + + /* Allocate exactly xDataLength bytes so any read past the reported length + * is a genuine out-of-bounds access, not a harness artifact. */ + uint8_t * pucEthernetBuffer = ( uint8_t * ) safeMalloc( xDataLength ); + __CPROVER_assume( pucEthernetBuffer != NULL ); + + xNetworkBuffer.pucEthernetBuffer = pucEthernetBuffer; + xNetworkBuffer.xDataLength = xDataLength; + + __CPROVER_file_local_FreeRTOS_ICMP_c_prvProcessICMPEchoReply( &xNetworkBuffer ); +} diff --git a/test/cbmc/proofs/ReadSackOption/Makefile.json b/test/cbmc/proofs/ReadSackOption/Makefile.json new file mode 100644 index 0000000000..529176155a --- /dev/null +++ b/test/cbmc/proofs/ReadSackOption/Makefile.json @@ -0,0 +1,29 @@ +{ + "ENTRY": "ReadSackOption", + "CBMCFLAGS": [ + "--unwind 1", + "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowTxCheckAck.0:2", + "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowFastRetransmit.0:2" + ], + "OPT": + [ + "--export-file-local-symbols" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Reception.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_WIN.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Stream_Buffer.goto", + "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto", + "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto" + ], + "DEF": + [ + "ipconfigUSE_TCP=1", + "ipconfigUSE_TCP_WIN=1", + "ipconfigNETWORK_MTU=586" + ] +} diff --git a/test/cbmc/proofs/ReadSackOption/ReadSackOption_harness.c b/test/cbmc/proofs/ReadSackOption/ReadSackOption_harness.c new file mode 100644 index 0000000000..ba2db8cfc9 --- /dev/null +++ b/test/cbmc/proofs/ReadSackOption/ReadSackOption_harness.c @@ -0,0 +1,113 @@ +/* + * Minimal-assumptions memory-safety proof for prvReadSackOption() in + * FreeRTOS_TCP_Reception.c. + * + * prvReadSackOption unconditionally reads eight option bytes: + * ulChar2u32( &pucPtr[ uxIndex ] ) -> pucPtr[uxIndex .. uxIndex+3] + * ulChar2u32( &pucPtr[ uxIndex + 4U ] ) -> pucPtr[uxIndex+4 .. uxIndex+7] + * so the sole memory-safety precondition is uxIndex + 8 <= buffer_size + * (this is exactly the invariant the caller prvSingleStepTCPHeaderOptions + * maintains via its `while( ucLen >= 8 )` loop). + * + * The buffer is allocated to EXACTLY buffer_size with nondeterministic + * contents, and uxIndex is left nondeterministic within the modeled bound, + * so the eight-byte read window is checked against the true buffer end. + */ + +/* Standard includes. */ +#include +#include + +/* 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. +****************************************************************/ + +void __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvReadSackOption( const uint8_t * const pucPtr, + size_t uxIndex, + FreeRTOS_Socket_t * const pxSocket ); + +/**************************************************************** +* Proof harness. +****************************************************************/ + +void harness() +{ + /* Buffer of nondeterministic size, allocated to exactly that size. */ + size_t buffer_size; + + __CPROVER_assume( buffer_size < ipconfigNETWORK_MTU ); + + uint8_t * pucPtr = malloc( buffer_size ); + + __CPROVER_assume( pucPtr != NULL ); + + /* uxIndex is nondeterministic within the caller-maintained invariant. + * uxIndex + 8 <= buffer_size is the minimal precondition for the eight + * option bytes to be in bounds; it also prevents pointer-offset + * overflow in &pucPtr[ uxIndex + 4U ]. */ + size_t uxIndex; + + /* Both bounds are required: `uxIndex <= buffer_size` prevents a huge + * uxIndex from making `uxIndex + 8U` wrap (unsigned overflow) and + * spuriously satisfy the second bound. This matches the caller, where + * uxIndex is a small positive int32 stepped in units of 8. */ + __CPROVER_assume( uxIndex <= buffer_size ); + __CPROVER_assume( uxIndex + 8U <= buffer_size ); + + /* A socket, initialized enough for the ulTCPWindowTxSack call graph. */ + FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); + + __CPROVER_assume( pxSocket != NULL ); + + pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) ); + __CPROVER_assume( pxSocket->u.xTCP.txStream != NULL ); + + vListInitialise( &pxSocket->u.xTCP.xTCPWindow.xWaitQueue ); + + if( nondet_bool() ) + { + TCPSegment_t * segment = malloc( sizeof( TCPSegment_t ) ); + __CPROVER_assume( segment != NULL ); + 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 ) ); + __CPROVER_assume( segment != NULL ); + 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 ); + + /* lSRTT is guaranteed to be always greater than or equal to minimum value. */ + __CPROVER_assume( pxSocket->u.xTCP.xTCPWindow.lSRTT >= ipconfigTCP_SRTT_MINIMUM_VALUE_MS ); + + __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvReadSackOption( pucPtr, uxIndex, pxSocket ); +} diff --git a/test/cbmc/proofs/SingleStepTCPHeaderOptions/Makefile.json b/test/cbmc/proofs/SingleStepTCPHeaderOptions/Makefile.json new file mode 100644 index 0000000000..49af10b64f --- /dev/null +++ b/test/cbmc/proofs/SingleStepTCPHeaderOptions/Makefile.json @@ -0,0 +1,33 @@ +{ + "ENTRY": "SingleStepTCPHeaderOptions", + "OPTION_BUFFER_BOUND": 40, + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOptions.0:6", + "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowTxCheckAck.0:2", + "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowFastRetransmit.0:2" + ], + "OPT": + [ + "--export-file-local-symbols" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Reception.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_WIN.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Stream_Buffer.goto", + "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto", + "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto" + ], + "DEF": + [ + "ipconfigUSE_TCP=1", + "ipconfigUSE_TCP_WIN=1", + "ipconfigNETWORK_MTU=586", + "OPTION_BUFFER_BOUND={OPTION_BUFFER_BOUND}" + ] +} diff --git a/test/cbmc/proofs/SingleStepTCPHeaderOptions/SingleStepTCPHeaderOptions_harness.c b/test/cbmc/proofs/SingleStepTCPHeaderOptions/SingleStepTCPHeaderOptions_harness.c new file mode 100644 index 0000000000..49c449a03b --- /dev/null +++ b/test/cbmc/proofs/SingleStepTCPHeaderOptions/SingleStepTCPHeaderOptions_harness.c @@ -0,0 +1,121 @@ +/* + * Minimal-assumptions memory-safety proof for + * prvSingleStepTCPHeaderOptions() in FreeRTOS_TCP_Reception.c. + * + * Unlike the CheckOptionsOuter proof (which STUBS prvReadSackOption and + * permits buffer_size > uxTotalLength), this harness: + * - links the REAL prvReadSackOption via the .goto objects, so the + * SACK-option index arithmetic is fully exercised, and + * - allocates the option buffer to EXACTLY uxTotalLength bytes, so any + * read past the modeled option length is a genuine out-of-bounds bug. + * + * Buffer contents are fully nondeterministic and uxTotalLength is left + * nondeterministic within the modeled bound (the real caller, + * prvCheckOptions, derives it from the TCP data-offset field, whose max + * option area is 40 bytes; it also guarantees uxTotalLength >= 1 because + * the calling loop breaks when the remaining length reaches 0). + */ + +/* Standard includes. */ +#include +#include + +/* 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. +****************************************************************/ + +int32_t __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr, + size_t uxTotalLength, + FreeRTOS_Socket_t * const pxSocket, + BaseType_t xHasSYNFlag ); + +/**************************************************************** +* Proof harness. +****************************************************************/ + +void harness() +{ + /* Modeled length of the TCP options area. Left nondeterministic; the + * real caller bounds it to at most 40 bytes (10 * 4-byte option words) + * and never calls with 0. */ + size_t uxTotalLength; + + __CPROVER_assume( uxTotalLength >= 1 ); + __CPROVER_assume( uxTotalLength <= OPTION_BUFFER_BOUND ); + + /* Allocate the option buffer to EXACTLY its modeled length so that any + * over-read is a real out-of-bounds access rather than a read into + * over-provisioned slack. Contents are fully nondeterministic. */ + uint8_t * pucPtr = malloc( uxTotalLength ); + + __CPROVER_assume( pucPtr != NULL ); + + /* A socket, initialized enough for the real prvReadSackOption / + * ulTCPWindowTxSack call graph reached through the SACK option. */ + FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); + + __CPROVER_assume( pxSocket != NULL ); + + pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) ); + __CPROVER_assume( pxSocket->u.xTCP.txStream != NULL ); + + vListInitialise( &pxSocket->u.xTCP.xTCPWindow.xWaitQueue ); + + if( nondet_bool() ) + { + TCPSegment_t * segment = malloc( sizeof( TCPSegment_t ) ); + __CPROVER_assume( segment != NULL ); + 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 ) ); + __CPROVER_assume( segment != NULL ); + 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 ); + + /* lSRTT is guaranteed to be always greater than or equal to minimum value. */ + __CPROVER_assume( pxSocket->u.xTCP.xTCPWindow.lSRTT >= ipconfigTCP_SRTT_MINIMUM_VALUE_MS ); + + BaseType_t xHasSYNFlag; + + int32_t index = __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOptions( pucPtr, + uxTotalLength, + pxSocket, + xHasSYNFlag ); + + /* Postcondition relied upon by the calling loop in prvCheckOptions: + * the returned advance is either an error (-1), a stop (0/1), or a + * positive step no larger than the remaining option length. */ + __CPROVER_assert( ( index == -1 ) || ( index == 0 ) || ( index == 1 ) || ( ( size_t ) index <= uxTotalLength ), + "prvSingleStepTCPHeaderOptions: index <= uxTotalLength" ); +} diff --git a/test/cbmc/proofs/parsing/ProcessIPPacket_IPv4/prvAllowIPPacketIPv4/Configurations.json b/test/cbmc/proofs/parsing/ProcessIPPacket_IPv4/prvAllowIPPacketIPv4/Configurations.json new file mode 100644 index 0000000000..b36147ba67 --- /dev/null +++ b/test/cbmc/proofs/parsing/ProcessIPPacket_IPv4/prvAllowIPPacketIPv4/Configurations.json @@ -0,0 +1,51 @@ +{ + "ENTRY": "prvAllowIPPacketIPv4", + "IPV4_MAC_LOOP": 7, + "MAX_IP4_SIZE_FIELDS_LOOP": 21, + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset memcmp.0:{IPV4_MAC_LOOP}", + "--unwindset __CPROVER_file_local_FreeRTOS_IPv4_c_xCheckIPv4SizeFields.0:{MAX_IP4_SIZE_FIELDS_LOOP}", + "--nondet-static" + ], + "OPT": + [ + "--export-file-local-symbols" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv4.goto" + ], + "DEF": + [ + { + "ChecksumIncluded": + [ + "ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM=1", + "ipconfigETHERNET_DRIVER_FILTERS_PACKETS=1", + "FREERTOS_TCP_ENABLE_VERIFICATION=1", + "ipconfigNETWORK_MTU=200", + "ipconfigTCP_MSS=586", + "ipconfigUSE_DHCP=0" + ] + }, + { + "ChecksumNotIncluded": + [ + "ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM=0", + "ipconfigETHERNET_DRIVER_FILTERS_PACKETS=0", + "FREERTOS_TCP_ENABLE_VERIFICATION=1", + "ipconfigNETWORK_MTU=200", + "ipconfigTCP_MSS=586", + "ipconfigUSE_DHCP=0" + ] + } + ], + "INC": + [ + "$(FREERTOS_PLUS_TCP)/test/cbmc/include" + ] +} diff --git a/test/cbmc/proofs/parsing/ProcessIPPacket_IPv4/prvAllowIPPacketIPv4/prvAllowIPPacketIPv4_harness.c b/test/cbmc/proofs/parsing/ProcessIPPacket_IPv4/prvAllowIPPacketIPv4/prvAllowIPPacketIPv4_harness.c new file mode 100644 index 0000000000..7016d3903e --- /dev/null +++ b/test/cbmc/proofs/parsing/ProcessIPPacket_IPv4/prvAllowIPPacketIPv4/prvAllowIPPacketIPv4_harness.c @@ -0,0 +1,85 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IPv4.h" +#include "FreeRTOS_IP_Private.h" + +/* CBMC includes. */ +#include "cbmc.h" + +/* prvAllowIPPacketIPv4() is a file-local (static) function, exported for + * verification via --export-file-local-symbols. */ +eFrameProcessingResult_t prvAllowIPPacketIPv4( const IPPacket_t * const pxIPPacket, + const NetworkBufferDescriptor_t * const pxNetworkBuffer, + UBaseType_t uxHeaderLength ); + +/* Return either pdTRUE or pdFALSE (nondeterministic) for endpoint state. */ +BaseType_t FreeRTOS_IsEndPointUp( const struct xNetworkEndPoint * pxEndPoint ) +{ + BaseType_t xReturn; + + return xReturn; +} + +/* The IP-header checksum generation is stubbed out; the actual checksum + * value does not matter. Returns an indeterminate value each time. */ +uint16_t usGenerateChecksum( uint16_t usSum, + const uint8_t * pucNextData, + size_t uxByteCount ) +{ + uint16_t usReturn; + + __CPROVER_assert( pucNextData != NULL, "Checksum input buffer cannot be NULL" ); + + return usReturn; +} + +/* The protocol checksum generation is stubbed out. Returns an indeterminate + * value each time. */ +uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer, + size_t uxBufferLength, + BaseType_t xOutgoingPacket ) +{ + uint16_t usReturn; + + __CPROVER_assert( pucEthernetBuffer != NULL, "Ethernet buffer cannot be NULL" ); + + return usReturn; +} + +void harness() +{ + NetworkBufferDescriptor_t * const pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); + uint8_t * pucEthernetBuffer = ( uint8_t * ) safeMalloc( ipTOTAL_ETHERNET_FRAME_SIZE + ipIP_TYPE_OFFSET ); + + /* Network buffer must be valid, it's checked in prvProcessEthernetPacket. */ + __CPROVER_assume( pxNetworkBuffer != NULL ); + + /* Ethernet buffer in network buffer must be valid, the data length is + * checked in prvProcessEthernetPacket. */ + __CPROVER_assume( pucEthernetBuffer != NULL ); + + /* Points to ethernet buffer offset by ipIP_TYPE_OFFSET, so the buffer + * allocation matches pxGetNetworkBufferWithDescriptor. */ + pxNetworkBuffer->pucEthernetBuffer = &( pucEthernetBuffer[ ipIP_TYPE_OFFSET ] ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + + /* Minimum length of pxNetworkBuffer->xDataLength is at least the size of + * an IPPacket_t. Contents are left fully nondeterministic. */ + __CPROVER_assume( ( pxNetworkBuffer->xDataLength >= sizeof( IPPacket_t ) ) && + ( pxNetworkBuffer->xDataLength <= ipTOTAL_ETHERNET_FRAME_SIZE ) ); + + pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoints != NULL ); + pxNetworkEndPoints->pxNext = NULL; + + /* The packet is assigned to an endpoint during pxEasyFit(); model that. */ + pxNetworkBuffer->pxEndPoint = pxNetworkEndPoints; + + IPPacket_t * const pxIPPacket = ( IPPacket_t * ) pxNetworkBuffer->pucEthernetBuffer; + + prvAllowIPPacketIPv4( pxIPPacket, pxNetworkBuffer, ipSIZE_OF_IPv4_HEADER ); +}