CBMC proofs for MQTTAgent_Init (#5)

.gitmodules

@@ -4,3 +4,9 @@
 [submodule "test/unit-test/CMock"]
 	path = test/unit-test/CMock
 	url = https://github.com/ThrowTheSwitch/CMock.git
+[submodule "test/cbmc/aws-templates-for-cbmc-proofs"]
+	path = test/cbmc/aws-templates-for-cbmc-proofs
+	url = https://github.com/awslabs/aws-templates-for-cbmc-proofs.git
+[submodule "test/cbmc/litani"]
+	path = test/cbmc/litani
+	url = https://github.com/awslabs/aws-build-accumulator

test/cbmc/.gitignore

@@ -0,0 +1,23 @@
+# Emitted when running CBMC proofs
+proofs/**/logs
+proofs/**/gotos
+proofs/**/report
+proofs/**/html
+
+# Emitted by CBMC Viewer
+TAGS-*
+
+# Emitted by Arpa
+arpa_cmake/
+arpa-validation-logs/
+Makefile.arpa
+
+# Emitted by litani
+.ninja_deps
+.ninja_log
+.litani_cache_dir
+
+# These files should be overwritten whenever prepare.py runs
+cbmc-batch.yaml
+
+__pycache__/

test/cbmc/include/README.md

@@ -0,0 +1 @@
+../aws-templates-for-cbmc-proofs/template-for-repository/include/README.md

test/cbmc/include/core_mqtt_config.h

@@ -0,0 +1,91 @@
+/*
+ * coreMQTT-Agent v1.0.0
+ * Copyright (C) 2020 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.
+ */
+
+/**
+ * @file core_mqtt_config.h
+ * @brief This header sets configuration macros for the MQTT library.
+ */
+#ifndef CORE_MQTT_CONFIG_H_
+#define CORE_MQTT_CONFIG_H_
+
+/* Mock a network context for the CBMC proofs. */
+struct NetworkContext
+{
+    int NetworkContext;
+};
+
+/**
+ * @brief Determines the maximum number of MQTT PUBLISH messages, pending
+ * acknowledgement at a time, that are supported for incoming and outgoing
+ * direction of messages, separately.
+ *
+ * QoS 1 and 2 MQTT PUBLISHes require acknowledgement from the server before
+ * they can be completed. While they are awaiting the acknowledgement, the
+ * client must maintain information about their state. The value of this
+ * macro sets the limit on how many simultaneous PUBLISH states an MQTT
+ * context maintains, separately, for both incoming and outgoing direction of
+ * PUBLISHes.
+ *
+ * @note This definition must exist in order to compile. 10U is a typical value
+ * used in the MQTT demos.
+ */
+#define MQTT_STATE_ARRAY_MAX_COUNT              ( 10U )
+
+/**
+ * @brief Retry count for reading CONNACK from network.
+ *
+ * The MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT will be used only when the
+ * timeoutMs parameter of #MQTT_Connect() is passed as 0 . The transport
+ * receive for CONNACK will be retried MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT
+ * times before timing out. A value of 0 for this config will cause the
+ * transport receive for CONNACK  to be invoked only once.
+ */
+#define MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT    ( 2U )
+
+/**
+ * @brief Number of milliseconds to wait for a ping response to a ping
+ * request as part of the keep-alive mechanism.
+ *
+ * If a ping response is not received before this timeout, then
+ * #MQTT_ProcessLoop will return #MQTTKeepAliveTimeout.
+ */
+#define MQTT_PINGRESP_TIMEOUT_MS                ( 500U )
+
+/**
+ * @brief The maximum duration of receiving no data over network when
+ * attempting to read an incoming MQTT packet by the #MQTT_ProcessLoop or
+ * #MQTT_ReceiveLoop API functions.
+ *
+ * When an incoming MQTT packet is detected, the transport receive function
+ * may be called multiple times until all the expected number of bytes for the
+ * packet are received. This timeout represents the maximum duration of polling
+ * for any data to be received over the network for the incoming.
+ * If the timeout expires, the #MQTT_ProcessLoop or #MQTT_ReceiveLoop functions
+ * return #MQTTRecvFailed.
+ *
+ * This is set to 1 to exit right away after a zero is received in the transport
+ * receive stub. There is no added value, in proving memory safety, to repeat
+ * the logic that checks if the polling timeout is reached.
+ */
+#define MQTT_RECV_POLLING_TIMEOUT_MS            ( 1U )
+
+#endif /* ifndef CORE_MQTT_CONFIG_H_ */

test/cbmc/negative_tests/README.md

@@ -0,0 +1 @@
+../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/README.md

test/cbmc/negative_tests/assert/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/assert/Makefile

test/cbmc/negative_tests/assert/assert_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/assert/assert_harness.c

test/cbmc/negative_tests/bounds_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/bounds_check/Makefile

test/cbmc/negative_tests/bounds_check/bounds_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/bounds_check/bounds_check_harness.c

test/cbmc/negative_tests/conversion_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/conversion_check/Makefile

test/cbmc/negative_tests/conversion_check/conversion_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/conversion_check/conversion_check_harness.c

test/cbmc/negative_tests/div_by_zero_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/div_by_zero_check/Makefile

test/cbmc/negative_tests/div_by_zero_check/div_by_zero_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/div_by_zero_check/div_by_zero_check_harness.c

test/cbmc/negative_tests/float_overflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_overflow_check/Makefile

test/cbmc/negative_tests/float_overflow_check/float_overflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_overflow_check/float_overflow_check_harness.c

test/cbmc/negative_tests/float_underflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_underflow_check/Makefile

test/cbmc/negative_tests/float_underflow_check/float_underflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_underflow_check/float_underflow_check_harness.c

test/cbmc/negative_tests/nan_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/nan_check/Makefile

test/cbmc/negative_tests/nan_check/nan_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/nan_check/nan_check_harness.c

test/cbmc/negative_tests/pointer_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_check/Makefile

test/cbmc/negative_tests/pointer_check/pointer_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_check/pointer_check_harness.c

test/cbmc/negative_tests/pointer_overflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_overflow_check/Makefile

test/cbmc/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c

test/cbmc/negative_tests/pointer_primitive_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_primitive_check/Makefile

test/cbmc/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c

test/cbmc/negative_tests/pointer_underflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_underflow_check/Makefile

test/cbmc/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c

test/cbmc/negative_tests/signed_overflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_overflow_check/Makefile

test/cbmc/negative_tests/signed_overflow_check/signed_overflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_overflow_check/signed_overflow_check_harness.c

test/cbmc/negative_tests/signed_underflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_underflow_check/Makefile

test/cbmc/negative_tests/signed_underflow_check/signed_underflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_underflow_check/signed_underflow_check_harness.c

test/cbmc/negative_tests/undefined_shift_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/undefined_shift_check/Makefile

test/cbmc/negative_tests/undefined_shift_check/undefined_shift_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/undefined_shift_check/undefined_shift_check_harness.c

test/cbmc/negative_tests/unsigned_overflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_overflow_check/Makefile

test/cbmc/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c

test/cbmc/negative_tests/unsigned_underflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_underflow_check/Makefile

test/cbmc/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c

test/cbmc/proofs/MQTTAgent_Init/MQTTAgent_Init_harness.c

@@ -0,0 +1,49 @@
+/*
+ * coreMQTT-Agent v1.0.0
+ * Copyright (C) 2020 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.
+ */
+
+/* MQTT agent include. */
+#include "mqtt_agent.h"
+
+void harness()
+{
+
+  MQTTAgentContext_t * pMqttAgentContext;
+  AgentMessageInterface_t * pMsgInterface;
+  MQTTFixedBuffer_t * pNetworkBuffer;
+  TransportInterface_t * pTransportInterface;
+  MQTTGetCurrentTimeFunc_t getCurrentTimeMs;
+  IncomingPublishCallback_t incomingCallback;
+  void * pIncomingPacketContext;
+
+  pMqttAgentContext = malloc( sizeof( MQTTAgentContext_t ) );
+  pMsgInterface = malloc( sizeof( AgentMessageInterface_t ) );
+  pNetworkBuffer = malloc( sizeof( MQTTFixedBuffer_t ) );
+  pTransportInterface = malloc( sizeof( TransportInterface_t ) );
+
+  MQTTAgent_Init( pMqttAgentContext,
+                  pMsgInterface,
+                  pNetworkBuffer,
+                  pTransportInterface,
+                  getCurrentTimeMs,
+                  incomingCallback,
+                  pIncomingPacketContext );
+}

test/cbmc/proofs/MQTTAgent_Init/Makefile

@@ -0,0 +1,21 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = MQTTAgent_Init_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = MQTTAgent_Init
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+
+PROJECT_SOURCES += $(SRCDIR)/source/mqtt_agent.c
+
+include ../Makefile.common

test/cbmc/proofs/MQTTAgent_Init/README.md

@@ -0,0 +1,20 @@
+MQTTAgent_Init proof
+==============
+
+This directory contains a memory safety proof for MQTTAgent_Init.
+
+To run the proof.
+-------------
+
+* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
+  to your path.
+* Run `make`.
+* Open html/index.html in a web browser.
+
+To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles.
+-------------
+
+* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof.
+* Use Makefile.arpa as the starting point for your proof Makefile by:
+  1. Modifying Makefile.arpa (if required).
+  2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`).

test/cbmc/proofs/MQTTAgent_Init/cbmc-proof.txt

@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.

test/cbmc/proofs/MQTTAgent_Init/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "MQTTAgent_Init",
+  "proof-root": "test/cbmc/proofs"
+}

test/cbmc/proofs/Makefile-project-defines

@@ -0,0 +1,36 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+################################################################
+# Use this file to give project-specific definitions of the command
+# line arguments to pass to CBMC tools like goto-cc to build the goto
+# binaries and cbmc to do the property and coverage checking.
+#
+# Use this file to override most default definitions of variables in
+# Makefile.common.
+################################################################
+
+# Flags to pass to goto-cc for compilation (typically those passed to gcc -c)
+COMPILE_FLAGS += -fPIC
+COMPILE_FLAGS += -std=gnu90
+
+# Flags to pass to goto-cc for linking (typically those passed to gcc)
+# LINK_FLAGS =
+
+# Preprocessor include paths -I...
+INCLUDES += -I$(SRCDIR)/test/cbmc/include
+INCLUDES += -I$(SRCDIR)/source/include
+INCLUDES += -I$(SRCDIR)/source/dependency/coreMQTT/source/include
+INCLUDES += -I$(SRCDIR)/source/dependency/coreMQTT/source/interface
+
+# Preprocessor definitions -D...
+# DEFINES =
+
+# Path to arpa executable
+# ARPA =
+
+# Flags to pass to cmake for building the project
+# ARPA_CMAKE_FLAGS =

test/cbmc/proofs/Makefile-project-targets

@@ -0,0 +1,10 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+################################################################
+# Use this file to give project-specific targets, including targets
+# that may depend on targets defined in Makefile.common.
+################################################################

test/cbmc/proofs/Makefile-project-testing

@@ -0,0 +1,11 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+################################################################
+# Use this file to define project-specific targets and definitions for
+# unit testing or continuous integration that may depend on targets
+# defined in Makefile.common
+################################################################