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]>

test/cbmc/proofs/Makefile-template-defines

@@ -1,8 +1,7 @@
 
 # Absolute path to the root of the source tree.
 #
-SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../../ota-for-aws-iot-embedded-sdk/)
-
+SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../)
 
 # Absolute path to the litani script.
 #

test/cbmc/proofs/setDataInterface/Makefile

@@ -0,0 +1,25 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY = setDataInterface_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 = setDataInterface
+
+DEFINES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/source/ota_interface.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

test/cbmc/proofs/setDataInterface/README.md

@@ -0,0 +1,20 @@
+setDataInterface proof
+==============
+
+This directory contains a memory safety proof for setDataInterface.
+
+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/setDataInterface/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.

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

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

test/cbmc/proofs/setDataInterface/setDataInterface_harness.c

@@ -0,0 +1,49 @@
+/*
+ * AWS IoT Over-the-air Update v3.0.0
+ * Copyright (C) 2021 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 setDataInterface_harness.c
+ * @brief Implements the proof harness for setDataInterface function.
+ */
+/* Ota interface includes. */
+#include "ota_interface_private.h"
+
+void setDataInterface_harness()
+{
+    OtaDataInterface_t * pDataInterface;
+    OtaDataInterface_t dataInterface;
+    OtaErr_t err;
+
+    /* The input to the setDataInterface is a buffer statically initialized in the
+     *  source code with its size defined by OTA_PROTOCOL_BUFFER_SIZE. This macro is
+     *  not user configurable and thus the input does not require any constraint. */
+    uint8_t pProtocol[ OTA_PROTOCOL_BUFFER_SIZE ];
+
+    pDataInterface = &dataInterface;
+
+    err = setDataInterface( pDataInterface, pProtocol );
+
+    /* The function return can only be either of two values i.e OtaErrNone or
+     *  OtaErrInvalidDataProtocol. */
+    __CPROVER_assert( ( err == OtaErrInvalidDataProtocol ) || ( err == OtaErrNone ),
+                      "The function return can be either of those values." );
+}