Add CBMC proofs for additional receive-path parsing functions

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 <stdint.h>
+
+/* 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 );
+}

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

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 <stdint.h>
+
+/* 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 );
+}

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

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 <stdint.h>
+
+/* 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 );
+}

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

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 <stdint.h>
+
+/* 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 );
+}

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