Add cbmc proof of publishStatusMessage function (#259)

* Add CBMC-proofs infrastructure * Add CBMC-proofs infrastructure (#242) * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Update ci.yml * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Addition to CBMC infrastructure (#243) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace Co-authored-by: Aniruddha Kanhere <[email protected]> * Added CBMC proof of setDataInterface function (#245) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for setDataInterface function * removed unnecessary variables * Updated documentation * Uncrustified * Updated year in copyright notice Co-authored-by: Aniruddha Kanhere <[email protected]> * Added template inside proof directory * Added CBMC-proof files for publishStatusMessage function * Added CBMC proof of OTA_HTTP_strerror function (#252) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Add CBMC proof of OTA_HTTP_strerror function * Removed extra line and updated error log * Updated error log Co-authored-by: Aniruddha Kanhere <[email protected]> * Add CBMC proofs for RequestdataBlock_Http function (#248) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC Proof of requestDataBlock_Http function * Removed extra line * Update Comments Co-authored-by: Aniruddha Kanhere <[email protected]> * Added CBMC proofs for OTA_MQTT_strerror function (#247) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for OTA_MQTT_strerror function * Removed extra line * Updated comments * Fixed formatting errors * Updated error log Co-authored-by: Aniruddha Kanhere <[email protected]> * Added CBMC proofs for setControlInterface function (#246) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for setControlInterface function * Removed extra line * Added macro for the function * Fix formating errors * Fix spell check errors * Added preprocessor definition for setControlInterface function Co-authored-by: Aniruddha Kanhere <[email protected]> * Fix cbmc failures and updated comments * Update source directory * update source directory * fix spell check errors * Updated comments and removed unnecessary variables Co-authored-by: Aniruddha Kanhere <[email protected]>
aws · Sep 9, 2021 · 47fb59f · 47fb59f
1 parent 7e145b6
commit 47fb59f
Show file tree

Hide file tree

Showing 5 changed files with 125 additions and 0 deletions.
diff --git a/test/cbmc/proofs/publishStatusMessage/Makefile b/test/cbmc/proofs/publishStatusMessage/Makefile
@@ -0,0 +1,20 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY = publishStatusMessage_harness
+HARNESS_FILE = $(HARNESS_ENTRY)
+
+# 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 = publishStatusMessage
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/source/ota_mqtt.c
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+include ../Makefile.common
diff --git a/test/cbmc/proofs/publishStatusMessage/README.md b/test/cbmc/proofs/publishStatusMessage/README.md
@@ -0,0 +1,20 @@
+publishStatusMessage proof
+==============
+
+This directory contains a memory safety proof for publishStatusMessage.
+
+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`).
diff --git a/test/cbmc/proofs/publishStatusMessage/cbmc-proof.txt b/test/cbmc/proofs/publishStatusMessage/cbmc-proof.txt
@@ -0,0 +1,2 @@
+# This file marks this directory as containing a CBMC proof.
+# This file is required by the run-cbmc-proofs.py to differentiate between a proof directory from a normal directory.
diff --git a/test/cbmc/proofs/publishStatusMessage/cbmc-viewer.json b/test/cbmc/proofs/publishStatusMessage/cbmc-viewer.json
@@ -0,0 +1,6 @@
+{ "expected-missing-functions":
+  [
+  ],
+  "proof-name": "publishStatusMessage",
+  "proof-root": "test/cbmc/proofs"
+}
diff --git a/test/cbmc/proofs/publishStatusMessage/publishStatusMessage_harness.c b/test/cbmc/proofs/publishStatusMessage/publishStatusMessage_harness.c
@@ -0,0 +1,77 @@
+/* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. */
+/* SPDX-License-Identifier: Apache-2.0 */
+
+/**
+ * @file publishStatusMessage_harness.c
+ * @brief Implements the proof harness for publishStatusMessage function.
+ */
+/* Include headers for mqtt interface. */
+#include "ota_mqtt_private.h"
+
+#define TOPIC_JOB_STATUS_BUFFER_SIZE    222U            /*!< Max buffer size of pBuffer in publishStatusMessage function. */
+#define OTA_STATUS_MSG_MAX_SIZE         128U            /*!< Max length of a job status message to the service. */
+
+/* Declaration of the test function with the mangled name. */
+OtaMqttStatus_t __CPROVER_file_local_ota_mqtt_c_publishStatusMessage( OtaAgentContext_t * pAgentCtx,
+                                                                      const char * pMsg,
+                                                                      uint32_t msgSize,
+                                                                      uint8_t qos );
+
+/* Stub required to combine a set of strings(to form a topic). */
+size_t __CPROVER_file_local_ota_mqtt_c_stringBuilder( char * pBuffer,
+                                                      size_t bufferSizeBytes,
+                                                      const char * strings[] )
+{
+    size_t stringSize;
+
+    /* pBuffer is initialized in publishStatusMessage function before passing it to the
+     * stringBuilder function and thus cannot be NULL. */
+    __CPROVER_assert( pBuffer != NULL,
+                      "Unable to use pBuffer: passed pointer value is NULL." );
+
+    /* strings is initialized publishStatusMessage function before passing it to the
+     * stringBuilder function and thus cannot be NULL. */
+    __CPROVER_assert( strings != NULL,
+                      "Unable to use strings: passed pointer value is NULL." );
+
+    /* The static size of the pBuffer in the publishStatusMessage function is
+     * defined by TOPIC_GET_STREAM_BUFFER_SIZE. Hence, the value stringSize can
+     * never exceed TOPIC_GET_STREAM_BUFFER_SIZE. */
+    __CPROVER_assume( stringSize > 0 && stringSize < TOPIC_JOB_STATUS_BUFFER_SIZE );
+
+    return stringSize;
+}
+
+/* Stub to user defined MQTT-publish operation. */
+OtaMqttStatus_t publish( const char * const pacTopic,
+                         uint16_t usTopicLen,
+                         const char * pcMsg,
+                         uint32_t ulMsgSize,
+                         uint8_t ucQoS )
+{
+    OtaMqttStatus_t status;
+
+    return status;
+}
+
+/*****************************************************************************/
+
+void publishStatusMessage_harness()
+{
+    OtaAgentContext_t agent;
+    OtaInterfaces_t otaInterface;
+
+    /* pMsg is declared statically in the updateJobStatus_Mqtt and passed to publishStatusMessage function. */
+    char pMsg[ OTA_STATUS_MSG_MAX_SIZE ];
+    uint32_t msgSize;
+    uint8_t qos;
+
+    /* publish reference to the mqtt function is expected to be assigned by the user and thus
+     * assumed not to be NULL. */
+    otaInterface.mqtt.publish = publish;
+
+    agent.pOtaInterface = &otaInterface;
+
+    /* The agent can never be NULL as it is defined as a global variable. */
+    ( void ) __CPROVER_file_local_ota_mqtt_c_publishStatusMessage( &agent, pMsg, msgSize, qos );
+}
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		# This file marks this directory as containing a CBMC proof.
		# This file is required by the run-cbmc-proofs.py to differentiate between a proof directory from a normal directory.