Add CBMC Proofs for the new APIs

source/include/core_mqtt.h

@@ -1228,7 +1228,7 @@ const char * MQTT_Status_strerror( MQTTStatus_t status );
 /**
  * @brief Get the bytes in a #MQTTVec pointer which can store the whole array as a an MQTT packet when calling MQTT_SerializeMQTTVec( void * pAllocatedMem, MQTTVec_t *pVec ) function.
  *
- * @param[in] pVec The #MQTTVec pointer.
+ * @param[in] pVec The #MQTTVec pointer given as input to the user defined #MQTTStorePacketForRetransmit callback function. Should not be NULL.
  *
  * @return The bytes in the provided #MQTTVec array which can then be used to set aside memory to be used with MQTT_SerializeMQTTVec( void * pAllocatedMem, MQTTVec_t *pVec ) function.
  */
@@ -1239,8 +1239,8 @@ size_t MQTT_GetBytesInMQTTVec( const MQTTVec_t * pVec );
 /**
  * @brief Serialize the bytes in an array of #MQTTVec in the provided \p pAllocatedMem
  *
- * @param[in] pAllocatedMem Memory in which to serialize the data in the #MQTTVec array. It must be of size provided by MQTT_GetBytesInMQTTVec( MQTTVec_t *pVec ).
- * @param[in] pVec The #MQTTVec pointer.
+ * @param[in] pAllocatedMem Memory in which to serialize the data in the #MQTTVec array. It must be of size provided by MQTT_GetBytesInMQTTVec( MQTTVec_t *pVec ). Should not be NULL.
+ * @param[in] pVec The #MQTTVec pointer given as input to the user defined #MQTTStorePacketForRetransmit callback function. Should not be NULL.
  */
 /* @[declare_mqtt_serializemqttvec] */
 void MQTT_SerializeMQTTVec( uint8_t * pAllocatedMem,

test/cbmc/include/mqtt_cbmc_state.h

@@ -165,4 +165,13 @@ MQTTContext_t * allocateMqttContext( MQTTContext_t * pContext );
  */
 bool isValidMqttContext( const MQTTContext_t * pContext );
 
+/**
+ * @brief Allocate a #MQTTVec_t object.
+ *
+ * @param[in] mqttVec #MQTTVec_t object information.
+ *
+ * @return NULL or allocated #MQTTContext_t memory.
+ */
+MQTTVec_t * allocateMqttVec( MQTTVec_t * mqttVec );
+
 #endif /* ifndef MQTT_CBMC_STATE_H_ */

test/cbmc/proofs/MQTT_GetBytesInMQTTVec/MQTT_GetBytesInMQTTVec_harness.c

@@ -0,0 +1,40 @@
+/*
+ * coreMQTT <DEVELOPMENT BRANCH>
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * SPDX-License-Identifier: MIT
+ *
+ * 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 MQTT_Disconnect_harness.c
+ * @brief Implements the proof harness for MQTT_Disconnect function.
+ */
+#include "core_mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTVec_t * mqttVec;
+    size_t memoryRequired;
+
+    mqttVec = allocateMqttVec( NULL );
+
+    memoryRequired = MQTT_GetBytesInMQTTVec( mqttVec );
+}

test/cbmc/proofs/MQTT_GetBytesInMQTTVec/Makefile

@@ -0,0 +1,39 @@
+#
+# 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.
+#
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=MQTT_GetBytesInMQTTVec_harness
+PROOF_UID=MQTT_GetBytesInMQTTVec
+
+PUBLISH_PACKET_VECTORS = 5
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += MQTT_GetBytesInMQTTVec.0:${PUBLISH_PACKET_VECTORS}
+UNWINDSET += allocateMqttVec.0:${PUBLISH_PACKET_VECTORS}
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c
+PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c
+
+include ../Makefile.common

test/cbmc/proofs/MQTT_GetBytesInMQTTVec/README.md

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

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

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

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

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

test/cbmc/proofs/MQTT_SerializeMQTTVec/MQTT_SerializeMQTTVec_harness.c

@@ -0,0 +1,52 @@
+/*
+ * coreMQTT <DEVELOPMENT BRANCH>
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * SPDX-License-Identifier: MIT
+ *
+ * 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 MQTT_Disconnect_harness.c
+ * @brief Implements the proof harness for MQTT_Disconnect function.
+ */
+#include "core_mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTVec_t * mqttVec;
+    size_t memoryRequired;
+    uint8_t * memoryBuffer;
+
+    mqttVec = allocateMqttVec( NULL );
+
+    memoryRequired = MQTT_GetBytesInMQTTVec( mqttVec );
+
+    /* It is a part of the API contract that #MQTT_SerializeMQTTVec will be called with
+     * a memory buffer of size output by #MQTT_GetBytesInMQTTVec function and the
+     * #MQTTVec_t pointer given by the library as an input to the user defined
+     * #MQTTStorePacketForRetransmit callback function. Hence the memory buffer should
+     * not be NULL.
+     */
+    memoryBuffer = malloc( memoryRequired );
+    __CPROVER_assume( memoryBuffer != NULL );
+
+    MQTT_SerializeMQTTVec( memoryBuffer, mqttVec );
+}

test/cbmc/proofs/MQTT_SerializeMQTTVec/Makefile

@@ -0,0 +1,40 @@
+#
+# 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.
+#
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=MQTT_SerializeMQTTVec_harness
+PROOF_UID=MQTT_SerializeMQTTVec
+
+PUBLISH_PACKET_VECTORS = 5
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += MQTT_GetBytesInMQTTVec.0:${PUBLISH_PACKET_VECTORS}
+UNWINDSET += allocateMqttVec.0:${PUBLISH_PACKET_VECTORS}
+UNWINDSET += MQTT_SerializeMQTTVec.0:${PUBLISH_PACKET_VECTORS}
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c
+PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c
+
+include ../Makefile.common

test/cbmc/proofs/MQTT_SerializeMQTTVec/README.md

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

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

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

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

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

test/cbmc/sources/mqtt_cbmc_state.c

@@ -67,7 +67,27 @@
  * @note This definition must exist in order to compile. 10U is a typical value
  * used in the MQTT demos.
  */
-#define MAX_UNACKED_PACKETS    ( 20U )
+#define MAX_UNACKED_PACKETS       ( 20U )
+
+/**
+ * @brief Gives the maximum number of transport vectors required to encode
+ * a publish packet to send over the network interface.
+ */
+#define PUBLISH_PACKET_VECTORS    ( 4U )
+
+/**
+ * @brief Definition of the MQTTVec_t struct that is used to pass the outgoing
+ * publish packet content to the user callback function to store the packet for
+ * retransmission purposes
+ *
+ * @note The definition of this struct is hidden from the application code. The intent
+ * behind defining the struct here is to simulate the actual process flow.
+ */
+struct MQTTVec
+{
+    TransportOutVector_t * pVector; /**< Pointer to transport vector. USER SHOULD NOT ACCESS THIS DIRECTLY - IT IS AN INTERNAL DETAIL AND CAN CHANGE. */
+    size_t vectorLen;               /**< Length of the transport vector. USER SHOULD NOT ACCESS THIS DIRECTLY - IT IS AN INTERNAL DETAIL AND CAN CHANGE. */
+};
 
 MQTTPacketInfo_t * allocateMqttPacketInfo( MQTTPacketInfo_t * pPacketInfo )
 {
@@ -284,3 +304,50 @@ bool isValidMqttContext( const MQTTContext_t * pContext )
 
     return isValid;
 }
+
+MQTTVec_t * allocateMqttVec( MQTTVec_t * mqttVec )
+{
+    size_t vecLen;
+    TransportOutVector_t * pVector;
+
+    if( mqttVec == NULL )
+    {
+        mqttVec = malloc( sizeof( MQTTVec_t ) );
+    }
+
+    /* It is a part of the API contract that the #MQTT_GetBytesInMQTTVec API will be called
+     * with the #MQTTVec_t pointer given by the library as an input to the user defined
+     * #MQTTStorePacketForRetransmit callback function. The library would never provide with
+     * a NULL pointer. As this is a simulation of the real flow, it can be assumed that the
+     * mqttVec pointer is non-NULL.
+     */
+    __CPROVER_assume( mqttVec != NULL );
+    __CPROVER_assume( vecLen <= PUBLISH_PACKET_VECTORS );
+    __CPROVER_assume( vecLen > 0U );
+
+    pVector = malloc( vecLen * sizeof( TransportOutVector_t ) );
+
+    /* The library is responsible with providing the memory for pVector within the mqttVec. Hence
+     * it can be assumed that pVector is also non-NULL
+     */
+    __CPROVER_assume( pVector != NULL );
+
+    for( int i = 0; i < vecLen; i++ )
+    {
+        /* One of there vectors will also hold the buffer pointing to the publish payload. The
+         * maximum size of thepublish payload is limited by the remaining length field. Hence the maximum
+         * size of the buffer in the vector can be 268435455 B.
+         */
+        __CPROVER_assume( pVector[ i ].iov_len <= 268435455 );
+        __CPROVER_assume( pVector[ i ].iov_len >= 0U );
+
+        pVector[ i ].iov_base = malloc( pVector[ i ].iov_len * sizeof( uint8_t ) );
+
+        __CPROVER_assume( pVector[ i ].iov_base != NULL );
+    }
+
+    mqttVec->pVector = pVector;
+    mqttVec->vectorLen = vecLen;
+
+    return mqttVec;
+}

tools/coverity/README.md

@@ -25,32 +25,36 @@ To compile and run the Coverity target successfully, you must have the following
 
 ### To build and run coverity:
 Go to the root directory of the library and run the following commands in terminal:
-1. Update the compiler configuration in Coverity
+1. Create a local directory for the configuration files
   ~~~
-  cov-configure --force --compiler cc --comptype gcc
+  mkdir covConfig
   ~~~
-2. Create the build files using CMake in a `build` directory
+2. Update the compiler configuration in Coverity
+  ~~~
+  cov-configure --config covConfig/coverity.xml --compiler cc --comptype gcc --template
+  ~~~
+3. Create the build files using CMake in a `build` directory
   ~~~
   cmake -B build -S test
   ~~~
-3. Go to the build directory and copy the coverity configuration file
+4. Go to the build directory and copy the coverity configuration file
   ~~~
   cd build/
   ~~~
-4. Build the static analysis target
+5. Build the static analysis target
   ~~~
-  cov-build --emit-complementary-info --dir cov-out make coverity_analysis
+  cov-build --config ../covConfig/coverity.xml --emit-complementary-info --dir cov-out make coverity_analysis
   ~~~
-5. Go to the Coverity output directory (`cov-out`) and begin Coverity static analysis
+6. Go to the Coverity output directory (`cov-out`) and begin Coverity static analysis
   ~~~
   cd cov-out/
   cov-analyze --dir . --coding-standard-config ../../tools/coverity/misra.config --tu-pattern "file('.*/source/.*')"
   ~~~
-6. Format the errors in HTML format so that it is more readable while removing the test and build directory from the report
+7. Format the errors in HTML format so that it is more readable while removing the test and build directory from the report
   ~~~
   cov-format-errors --dir . --file "source" --exclude-files '(/build/|/test/)' --html-output html-out;
   ~~~
-7. Format the errors in JSON format to perform a jq query to get a simplified list of any exceptions.
+8. Format the errors in JSON format to perform a jq query to get a simplified list of any exceptions.
   NOTE: A blank output means there are no defects that aren't being suppressed by the config or inline comments.
   ~~~
   cov-format-errors --dir . --file "source" --exclude-files '(/build/|/test/)' --json-output-v2 defects.json;
@@ -61,10 +65,11 @@ Go to the root directory of the library and run the following commands in termin
 
 For your convenience the commands above are below to be copy/pasted into a UNIX command friendly terminal.
  ~~~
- cov-configure --force --compiler cc --comptype gcc;
+ mkdir covConfig
+ cov-configure --config covConfig/coverity.xml --compiler cc --comptype gcc --template
  cmake -B build -S test;
  cd build/;
- cov-build --emit-complementary-info --dir cov-out make coverity_analysis;
+ cov-build --config ../covConfig/coverity.xml --emit-complementary-info --dir cov-out make coverity_analysis
  cd cov-out/
  cov-analyze --dir . --coding-standard-config ../../tools/coverity/misra.config --tu-pattern "file('.*/source/.*')";
  cov-format-errors --dir . --file "source" --exclude-files '(/build/|/test/)' --html-output html-out;