MQTT CBMC Proofs (#1052)

CBMC proofs for:

MQTT_SerializeAck()
MQTT_SerializeDisconnect()
MQTT_SerializePingreq()
MQTT_SerializePublish()
MQTT_SerializePublishHeader
MQTT_SerializeSubscribe()
MQTT_SerializeUnsubscribe()

cbmc/include/mqtt_cbmc_state.h

@@ -50,6 +50,9 @@ MQTTPacketInfo_t * allocateMqttPacketInfo( MQTTPacketInfo_t * pPacketInfo );
  * @param[in] pPacketInfo #MQTTPacketInfo_t object to validate.
  *
  * @return True if the #MQTTPacketInfo_t object is valid, false otherwise.
+ *
+ * @note A NULL object is a valid object. This is for coverage of the NULL
+ * parameter checks in the function under proof.
  */
 bool isValidMqttPacketInfo( const MQTTPacketInfo_t * pPacketInfo );
 
@@ -68,6 +71,9 @@ MQTTPublishInfo_t * allocateMqttPublishInfo( MQTTPublishInfo_t * pPublishInfo );
  * @param[in] pPublishInfo #MQTTPublishInfo_t object to validate.
  *
  * @return True if the #MQTTPublishInfo_t object is valid, false otherwise.
+ *
+ * @note A NULL object is a valid object. This is for coverage of the NULL
+ * parameter checks in the function under proof.
  */
 bool isValidMqttPublishInfo( const MQTTPublishInfo_t * pPublishInfo );
 
@@ -86,6 +92,9 @@ MQTTConnectInfo_t * allocateMqttConnectInfo( MQTTConnectInfo_t * pConnectInfo );
  * @param[in] pConnectInfo #MQTTConnectInfo_t object to validate.
  *
  * @return True if the #MQTTConnectInfo_t object is valid, false otherwise.
+ *
+ * @note A NULL object is a valid object. This is for coverage of the NULL
+ * parameter checks in the function under proof.
  */
 bool isValidMqttConnectInfo( const MQTTConnectInfo_t * pConnectInfo );
 
@@ -96,7 +105,7 @@ bool isValidMqttConnectInfo( const MQTTConnectInfo_t * pConnectInfo );
  *
  * @return NULL or allocated #MQTTFixedBuffer_t memory.
  */
-MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pBuffer );
+MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pFixedBuffer );
 
 /**
  * @brief Validate a #MQTTFixedBuffer_t object.
@@ -104,7 +113,35 @@ MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pBuffer );
  * @param[in] pBuffer #MQTTFixedBuffer_t object to validate.
  *
  * @return True if the #MQTTFixedBuffer_t object is valid, false otherwise.
+ *
+ * @note A NULL object is a valid object. This is for coverage of the NULL
+ * parameter checks in the function under proof.
  */
-bool isValidMqttFixedBuffer( const MQTTFixedBuffer_t * pBuffer );
+bool isValidMqttFixedBuffer( const MQTTFixedBuffer_t * pFixedBuffer );
+
+/**
+ * @brief Allocate an array of #MQTTSubscribeInfo_t objects.
+ *
+ * @param[in] pSubscriptionList #MQTTSubscribeInfo_t object information.
+ * @param[in] subscriptionCount The amount of #MQTTSubscribeInfo_t objects to allocate.
+ *
+ * @return NULL or allocated #MQTTSubscribeInfo_t array.
+ */
+MQTTSubscribeInfo_t * allocateMqttSubscriptionList( MQTTSubscribeInfo_t * pSubscriptionList,
+                                                    size_t subscriptionCount );
+
+/**
+ * @brief Validate an array of #MQTTSubscribeInfo_t objects.
+ *
+ * @param[in] pSubscriptionList #MQTTSubscribeInfo_t object information.
+ * @param[in] subscriptionCount The length of #MQTTSubscribeInfo_t objects in the pSubscriptionList.
+ *
+ * @return True if the #MQTTSubscribeInfo_t is valid.
+ *
+ * @note A NULL object is a valid object. This is for coverage of the NULL
+ * parameter checks in the function under proof.
+ */
+bool isValidMqttSubscriptionList( MQTTSubscribeInfo_t * pSubscriptionList,
+                                  size_t subscriptionCount );
 
 #endif /* ifndef MQTT_CBMC_STATE_H_ */

cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c

@@ -28,11 +28,11 @@
 
 void harness()
 {
-    MQTTPacketInfo_t * pIncomingPacket = NULL;
+    MQTTPacketInfo_t * pIncomingPacket;
     uint16_t * pPacketId;
     bool * pSessionPresent;
 
-    pIncomingPacket = allocateMqttPacketInfo( pIncomingPacket );
+    pIncomingPacket = allocateMqttPacketInfo( NULL );
     __CPROVER_assume( isValidMqttPacketInfo( pIncomingPacket ) );
 
     MQTT_DeserializeAck( pIncomingPacket,

cbmc/proofs/MQTT_DeserializeAck/Makefile

@@ -11,7 +11,7 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(PROOFDIR)/../../sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
 PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
 
 include ../Makefile.common

cbmc/proofs/MQTT_DeserializeAck/README.md

@@ -5,6 +5,6 @@ This directory contains a memory safety proof for MQTT_DeserializeAck.
 
 To run the proof.
 * Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer
-  to your path
+  to your path.
-* Run "make"
+* Run "make".
 * Open html/index.html in a web browser.

cbmc/proofs/MQTT_DeserializePublish/MQTT_DeserializePublish_harness.c

@@ -29,14 +29,14 @@
 
 void harness()
 {
-    MQTTPacketInfo_t * pIncomingPacket = NULL;
+    MQTTPacketInfo_t * pIncomingPacket;
-    MQTTPublishInfo_t * pPublishInfo = NULL;
+    MQTTPublishInfo_t * pPublishInfo;
     uint16_t packetId;
 
-    pIncomingPacket = allocateMqttPacketInfo( pIncomingPacket );
+    pIncomingPacket = allocateMqttPacketInfo( NULL );
     __CPROVER_assume( isValidMqttPacketInfo( pIncomingPacket ) );
 
-    pPublishInfo = allocateMqttPublishInfo( pPublishInfo );
+    pPublishInfo = allocateMqttPublishInfo( NULL );
     __CPROVER_assume( isValidMqttPublishInfo( pPublishInfo ) );
 
     /* This function grabs the topic name, the topic name length, the

cbmc/proofs/MQTT_DeserializePublish/Makefile

@@ -11,7 +11,7 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(PROOFDIR)/../../sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
 PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
 
 include ../Makefile.common

cbmc/proofs/MQTT_DeserializePublish/README.md

@@ -5,6 +5,6 @@ This directory contains a memory safety proof for MQTT_DeserializePublish.
 
 To run the proof.
 * Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer
-  to your path
+  to your path.
-* Run "make"
+* Run "make".
 * Open html/index.html in a web browser.

cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/MQTT_GetIncomingPacketTypeAndLength_harness.c

@@ -36,9 +36,9 @@ void harness()
 
     /* MQTT_GetIncomingPacketTypeAndLength() will set only the remainingLength
      * field in the input MQTTPacketInfo_t structure. */
-    MQTTPacketInfo_t * pIncomingPacket = NULL;
+    MQTTPacketInfo_t * pIncomingPacket;
 
-    pIncomingPacket = allocateMqttPacketInfo( pIncomingPacket );
+    pIncomingPacket = allocateMqttPacketInfo( NULL );
     __CPROVER_assume( isValidMqttPacketInfo( pIncomingPacket ) );
 
     MQTT_GetIncomingPacketTypeAndLength( NetworkInterfaceReceiveStub,

cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/Makefile

@@ -7,8 +7,8 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET += getRemainingLength.0:5
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(PROOFDIR)/../../sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
-PROOF_SOURCES += $(PROOFDIR)/../../stubs/network_interface_stubs.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c
 PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
 
 include ../Makefile.common

cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/README.md

@@ -5,6 +5,6 @@ This directory contains a memory safety proof for MQTT_GetIncomingPacketTypeAndL
 
 To run the proof.
 * Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer
-  to your path
+  to your path.
-* Run "make"
+* Run "make".
 * Open html/index.html in a web browser.

cbmc/proofs/MQTT_GetPacketId/Makefile

@@ -8,7 +8,7 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(PROOFDIR)/../../sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
 PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c
 
 include ../Makefile.common

cbmc/proofs/MQTT_GetPacketId/README.md

@@ -5,6 +5,6 @@ This directory contains a memory safety proof for MQTT_GetPacketId.
 
 To run the proof.
 * Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer
-  to your path
+  to your path.
-* Run "make"
+* Run "make".
 * Open html/index.html in a web browser.

cbmc/proofs/MQTT_Init/MQTT_Init_harness.c

@@ -29,10 +29,10 @@
 
 void harness()
 {
-    MQTTContext_t * pContext = NULL;
+    MQTTContext_t * pContext;
-    TransportInterface_t * pTransportInterface = NULL;
+    TransportInterface_t * pTransportInterface;
-    MQTTApplicationCallbacks_t * pCallbacks = NULL;
+    MQTTApplicationCallbacks_t * pCallbacks;
-    MQTTFixedBuffer_t * pNetworkBuffer = NULL;
+    MQTTFixedBuffer_t * pNetworkBuffer;
 
     pContext = mallocCanFail( sizeof( MQTTContext_t ) );
     pTransportInterface = mallocCanFail( sizeof( MQTTContext_t ) );

cbmc/proofs/MQTT_Init/Makefile

@@ -8,7 +8,7 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(PROOFDIR)/../../sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
 PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c
 
 include ../Makefile.common

cbmc/proofs/MQTT_Init/README.md

@@ -5,6 +5,6 @@ This directory contains a memory safety proof for MQTT_Init.
 
 To run the proof.
 * Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer
-  to your path
+  to your path.
-* Run "make"
+* Run "make".
 * Open html/index.html in a web browser.

cbmc/proofs/MQTT_SerializeAck/MQTT_SerializeAck_harness.c

@@ -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.
+ */
+
+/**
+ * @file MQTT_SerializeAck_harness.c
+ * @brief Implements the proof harness for MQTT_SerializeAck function.
+ */
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTFixedBuffer_t * pFixedBuffer;
+    uint8_t packetType;
+    uint16_t packetId;
+
+    pFixedBuffer = allocateMqttFixedBuffer( NULL );
+    __CPROVER_ASSUME( isValidMqttFixedBuffer( pFixedBuffer ) );
+
+    MQTT_SerializeAck( pFixedBuffer, packetType, packetId );
+}

cbmc/proofs/MQTT_SerializeAck/Makefile

@@ -0,0 +1,17 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=MQTT_SerializeAck_harness
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_SerializeAck/README.md

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

cbmc/proofs/MQTT_SerializeAck/cbmc-batch.yaml

@@ -0,0 +1,2 @@
+# This file marks this directory as containing a CBMC proof.
+# The contents of this file will be generated by continuous integration.

cbmc/proofs/MQTT_SerializeAck/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "MQTT_SerializeAck",
+  "proof-root": "libraries/standard/mqtt/cbmc/proofs"
+}

cbmc/proofs/MQTT_SerializeConnect/MQTT_SerializeConnect_harness.c

@@ -28,35 +28,43 @@
 
 void harness()
 {
-    MQTTConnectInfo_t * pConnectInfo = NULL;
+    MQTTConnectInfo_t * pConnectInfo;
-    MQTTPublishInfo_t * pWillInfo = NULL;
+    MQTTPublishInfo_t * pWillInfo;
-    size_t remainingLength = 0;
+    size_t remainingLength;
-    MQTTFixedBuffer_t * pBuffer = NULL;
+    MQTTFixedBuffer_t * pFixedBuffer;
-    size_t packetSize = 0;
+    size_t packetSize;
     MQTTStatus_t status = MQTTSuccess;
 
-    pConnectInfo = allocateMqttConnectInfo( pConnectInfo );
+    pConnectInfo = allocateMqttConnectInfo( NULL );
     __CPROVER_assume( isValidMqttConnectInfo( pConnectInfo ) );
 
-    pWillInfo = allocateMqttPublishInfo( pWillInfo );
+    pWillInfo = allocateMqttPublishInfo( NULL );
     __CPROVER_assume( isValidMqttPublishInfo( pWillInfo ) );
 
-    pBuffer = allocateMqttFixedBuffer( pBuffer );
+    pFixedBuffer = allocateMqttFixedBuffer( NULL );
-    __CPROVER_assume( isValidMqttFixedBuffer( pBuffer ) );
+    __CPROVER_assume( isValidMqttFixedBuffer( pFixedBuffer ) );
 
     /* Before calling MQTT_SerializeConnect() it is up to the application to make
-    * sure that the information in MQTTConnectInfo_t and MQTTPublishInfo_t can
+     * sure that the information in MQTTConnectInfo_t and MQTTPublishInfo_t can
-    * fit into the MQTTFixedBuffer_t. It is a violation of the API to call
+     * fit into the MQTTFixedBuffer_t. It is a violation of the API to call
-    * MQTT_SerializeConnect without first calling MQTT_GetConnectPacketSize(). */
+     * MQTT_SerializeConnect() without first calling MQTT_GetConnectPacketSize(). */
     if( pConnectInfo != NULL )
     {
-        status = MQTT_GetConnectPacketSize( pConnectInfo, pWillInfo, &remainingLength, &packetSize );
+        /* The output parameter pPacketSize of the function MQTT_GetConnectPacketSize()
+         * must not be NULL. packetSize returned is not used in this proof, but 
+         * is used normally by the application to verify the size of their 
+         * MQTTFixedBuffer_t. MQTT_SerializeConnect() will use the remainingLength 
+         * to recalculate the packetSize. */
+        status = MQTT_GetConnectPacketSize( pConnectInfo,
+                                            pWillInfo,
+                                            &remainingLength,
+                                            &packetSize );
     }
 
     if( status == MQTTSuccess )
     {
         /* For coverage, it is expected that a NULL pConnectInfo will reach this
          * function. */
-        MQTT_SerializeConnect( pConnectInfo, pWillInfo, remainingLength, pBuffer );
+        MQTT_SerializeConnect( pConnectInfo, pWillInfo, remainingLength, pFixedBuffer );
     }
 }

cbmc/proofs/MQTT_SerializeConnect/Makefile

@@ -11,7 +11,7 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET += encodeRemainingLength.0:3
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(PROOFDIR)/../../sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
 PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
 
 include ../Makefile.common

cbmc/proofs/MQTT_SerializeConnect/README.md

@@ -5,6 +5,6 @@ This directory contains a memory safety proof for MQTT_SerializeConnect.
 
 To run the proof.
 * Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer
-  to your path
+  to your path.
-* Run "make"
+* Run "make".
 * Open html/index.html in a web browser.

cbmc/proofs/MQTT_SerializeDisconnect/MQTT_SerializeDisconnect_harness.c

@@ -0,0 +1,37 @@
+/*
+ * 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 MQTT_SerializeDisconnect_harness.c
+ * @brief Implements the proof harness for MQTT_SerializeDisconnect function.
+ */
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTFixedBuffer_t * pFixedBuffer;
+
+    pFixedBuffer = allocateMqttFixedBuffer( NULL );
+    __CPROVER_ASSUME( isValidMqttFixedBuffer( pFixedBuffer ) );
+
+    MQTT_SerializeDisconnect( pFixedBuffer );
+}

cbmc/proofs/MQTT_SerializeDisconnect/Makefile

@@ -0,0 +1,17 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=MQTT_SerializeDisconnect_harness
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_SerializeDisconnect/README.md

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

cbmc/proofs/MQTT_SerializeDisconnect/cbmc-batch.yaml

@@ -0,0 +1,2 @@
+# This file marks this directory as containing a CBMC proof.
+# The contents of this file will be generated by continuous integration.

cbmc/proofs/MQTT_SerializeDisconnect/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "MQTT_SerializeDisconnect",
+  "proof-root": "libraries/standard/mqtt/cbmc/proofs"
+}

cbmc/proofs/MQTT_SerializePingreq/MQTT_SerializePingreq_harness.c

@@ -0,0 +1,37 @@
+/*
+ * 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 MQTT_SerializePingreq_harness.c
+ * @brief Implements the proof harness for MQTT_SerializePingreq function.
+ */
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTFixedBuffer_t * pFixedBuffer;
+
+    pFixedBuffer = allocateMqttFixedBuffer( NULL );
+    __CPROVER_ASSUME( isValidMqttFixedBuffer( pFixedBuffer ) );
+
+    MQTT_SerializePingreq( pFixedBuffer );
+}

cbmc/proofs/MQTT_SerializePingreq/Makefile

@@ -0,0 +1,17 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=MQTT_SerializePingreq_harness
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_SerializePingreq/README.md

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

cbmc/proofs/MQTT_SerializePingreq/cbmc-batch.yaml

@@ -0,0 +1,2 @@
+# This file marks this directory as containing a CBMC proof.
+# The contents of this file will be generated by continuous integration.

cbmc/proofs/MQTT_SerializePingreq/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "MQTT_SerializePingreq",
+  "proof-root": "libraries/standard/mqtt/cbmc/proofs"
+}

cbmc/proofs/MQTT_SerializePublish/MQTT_SerializePublish_harness.c

@@ -0,0 +1,67 @@
+/*
+ * 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 MQTT_SerializePublish_harness.c
+ * @brief Implements the proof harness for MQTT_SerializePublish function.
+ */
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTPublishInfo_t * pPublishInfo;
+    uint16_t packetId;
+    size_t remainingLength;
+    size_t packetSize;
+    const MQTTFixedBuffer_t * pFixedBuffer;
+    MQTTStatus_t status = MQTTSuccess;
+
+    pPublishInfo = allocateMqttPublishInfo( NULL );
+    __CPROVER_assume( isValidMqttPublishInfo( pPublishInfo ) );
+
+    pFixedBuffer = allocateMqttFixedBuffer( NULL );
+    __CPROVER_assume( isValidMqttFixedBuffer( pFixedBuffer ) );
+
+    /* Before calling MQTT_SerializePublish() it is up to the application to
+     * make sure that the information in MQTTPublishInfo_t can fit into the
+     * MQTTFixedBuffer_t. It is a violation of the API to call
+     * MQTT_SerializePublish() without first calling MQTT_GetPublishPacketSize(). */
+    if( pPublishInfo != NULL )
+    {
+        /* The output parameter pPacketSize of the function MQTT_GetConnectPacketSize()
+         * must not be NULL. packetSize returned is not used in this proof, but 
+         * is used normally by the application to verify the size of their 
+         * MQTTFixedBuffer_t. MQTT_SerializeConnect() will use the remainingLength 
+         * to recalculate the packetSize. */
+        status = MQTT_GetPublishPacketSize( pPublishInfo, &remainingLength, &packetSize );
+    }
+
+    if( status == MQTTSuccess )
+    {
+        /* For coverage it is expected that a NULL pPublishInfo could
+         * reach this function. */
+        MQTT_SerializePublish( pPublishInfo,
+                               packetId,
+                               remainingLength,
+                               pFixedBuffer );
+    }
+}

cbmc/proofs/MQTT_SerializePublish/Makefile

@@ -0,0 +1,17 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=MQTT_SerializePublish_harness
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += encodeRemainingLength.0:4
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_SerializePublish/README.md

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

cbmc/proofs/MQTT_SerializePublish/cbmc-batch.yaml

@@ -0,0 +1,2 @@
+# This file marks this directory as containing a CBMC proof.
+# The contents of this file will be generated by continuous integration.

cbmc/proofs/MQTT_SerializePublish/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "MQTT_SerializePublish",
+  "proof-root": "libraries/standard/mqtt/cbmc/proofs"
+}

cbmc/proofs/MQTT_SerializePublishHeader/MQTT_SerializePublishHeader_harness.c

@@ -0,0 +1,75 @@
+/*
+ * 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 MQTT_SerializePublishHeader_harness.c
+ * @brief Implements the proof harness for MQTT_SerializePublishHeader function.
+ */
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTPublishInfo_t * pPublishInfo;
+    uint16_t packetId;
+    size_t remainingLength;
+    size_t packetSize;
+    MQTTFixedBuffer_t * pFixedBuffer;
+    size_t * pHeaderSize;
+    MQTTStatus_t status = MQTTSuccess;
+
+    pPublishInfo = allocateMqttPublishInfo( NULL );
+    __CPROVER_assume( isValidMqttPublishInfo( pPublishInfo ) );
+
+    pFixedBuffer = allocateMqttFixedBuffer( NULL );
+    __CPROVER_assume( isValidMqttFixedBuffer( pFixedBuffer ) );
+
+    /* Allocate space for a returned header size to get coverage of a possibly
+     * NULL input. */
+    pHeaderSize = mallocCanFail( sizeof( size_t ) );
+
+    /* Before calling MQTT_SerializePublishHeader() it is up to the application
+     * to verify that the information in MQTTPublishInfo_t can fit into the
+     * MQTTFixedBuffer_t. It is a violation of the API to call
+     * MQTT_SerializePublishHeader() without first calling MQTT_GetPublishPacketSize(). */
+    if( pPublishInfo != NULL )
+    {
+        /* The output parameter pPacketSize of the function MQTT_GetConnectPacketSize()
+         * must not be NULL. packetSize returned is not used in this proof, but 
+         * is used normally by the application to verify the size of their 
+         * MQTTFixedBuffer_t. MQTT_SerializeConnect() will use the remainingLength 
+         * to recalculate the packetSize. */
+        status = MQTT_GetPublishPacketSize( pPublishInfo,
+                                            &remainingLength,
+                                            &packetSize );
+    }
+
+    if( status == MQTTSuccess )
+    {
+        /* For coverage it is expected that a NULL pPublishInfo could
+         * reach this function. */
+        MQTT_SerializePublishHeader( pPublishInfo,
+                                     packetId,
+                                     remainingLength,
+                                     pFixedBuffer,
+                                     pHeaderSize );
+    }
+}

cbmc/proofs/MQTT_SerializePublishHeader/Makefile

@@ -0,0 +1,17 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=MQTT_SerializePublishHeader_harness
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += encodeRemainingLength.0:4
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_SerializePublishHeader/README.md

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

cbmc/proofs/MQTT_SerializePublishHeader/cbmc-batch.yaml

@@ -0,0 +1,2 @@
+# This file marks this directory as containing a CBMC proof.
+# The contents of this file will be generated by continuous integration.

cbmc/proofs/MQTT_SerializePublishHeader/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "MQTT_SerializePublishHeader",
+  "proof-root": "libraries/standard/mqtt/cbmc/proofs"
+}

cbmc/proofs/MQTT_SerializeSubscribe/MQTT_SerializeSubscribe_harness.c

@@ -0,0 +1,74 @@
+/*
+ * 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 MQTT_SerializeSubscribe_harness.c
+ * @brief Implements the proof harness for MQTT_SerializeSubscribe function.
+ */
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTSubscribeInfo_t * pSubscriptionList;
+    size_t subscriptionCount;
+    size_t remainingLength;
+    uint16_t packetId;
+    size_t packetSize;
+    MQTTFixedBuffer_t * pFixedBuffer;
+    MQTTStatus_t status = MQTTSuccess;
+
+    __CPROVER_assume( subscriptionCount < SUBSCRIPTION_COUNT_MAX );
+
+    pSubscriptionList = allocateMqttSubscriptionList( NULL, subscriptionCount );
+    __CPROVER_assume( isValidMqttSubscriptionList( pSubscriptionList, subscriptionCount ) );
+
+    pFixedBuffer = allocateMqttFixedBuffer( NULL );
+    __CPROVER_assume( isValidMqttFixedBuffer( pFixedBuffer ) );
+
+    /* Before calling MQTT_SerializeSubscribe() it is up to the application to
+     * make sure that the information in the list of MQTTSubscribeInfo_t can fit
+     * into the MQTTFixedBuffer_t. It is a violation of the API to call
+     * MQTT_SerializeSubscribe() without first calling MQTT_GetSubscribePacketSize(). */
+    if( pSubscriptionList != NULL )
+    {
+        /* The output parameter pPacketSize of the function MQTT_GetConnectPacketSize()
+         * must not be NULL. packetSize returned is not used in this proof, but 
+         * is used normally by the application to verify the size of their 
+         * MQTTFixedBuffer_t. MQTT_SerializeConnect() will use the remainingLength 
+         * to recalculate the packetSize. */
+        status = MQTT_GetSubscribePacketSize( pSubscriptionList,
+                                              subscriptionCount,
+                                              &remainingLength,
+                                              &packetSize );
+    }
+
+    if( status == MQTTSuccess )
+    {
+        /* For coverage it is expected that a NULL pSubscriptionList could
+         * reach this function. */
+        MQTT_SerializeSubscribe( pSubscriptionList,
+                                 subscriptionCount,
+                                 packetId,
+                                 remainingLength,
+                                 pFixedBuffer );
+    }
+}

cbmc/proofs/MQTT_SerializeSubscribe/Makefile

@@ -0,0 +1,25 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=MQTT_SerializeSubscribe_harness
+
+# Bind the subscription count. Please see the default value in mqtt_cbmc_state.c
+# for more information on this bound. This is set to 2 currently to have the proof
+# run quickly.
+SUBSCRIPTION_COUNT_MAX=2
+DEFINES += -DSUBSCRIPTION_COUNT_MAX=$(SUBSCRIPTION_COUNT_MAX)
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += allocateMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX)
+UNWINDSET += isValidMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX)
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX)
+UNWINDSET += MQTT_SerializeSubscribe.0:$(SUBSCRIPTION_COUNT_MAX)
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:4
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_SerializeSubscribe/README.md

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

cbmc/proofs/MQTT_SerializeSubscribe/cbmc-batch.yaml

@@ -0,0 +1,2 @@
+# This file marks this directory as containing a CBMC proof.
+# The contents of this file will be generated by continuous integration.

cbmc/proofs/MQTT_SerializeSubscribe/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "MQTT_SerializeSubscribe",
+  "proof-root": "libraries/standard/mqtt/cbmc/proofs"
+}

cbmc/proofs/MQTT_SerializeUnsubscribe/MQTT_SerializeUnsubscribe_harness.c

@@ -0,0 +1,77 @@
+/*
+ * 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 MQTT_SerializeUnsubscribe_harness.c
+ * @brief Implements the proof harness for MQTT_SerializeUnsubscribe function.
+ */
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTSubscribeInfo_t * pSubscriptionList;
+    size_t subscriptionCount;
+    size_t remainingLength;
+    uint16_t packetId;
+
+    /* This variable is not used but is needed for MQTT_GetUnsubscribePacketSize()
+     * to verify the pSubscriptionList. */
+    size_t packetSize;
+    MQTTFixedBuffer_t * pFixedBuffer;
+    MQTTStatus_t status = MQTTSuccess;
+
+    __CPROVER_assume( subscriptionCount < SUBSCRIPTION_COUNT_MAX );
+
+    pSubscriptionList = allocateMqttSubscriptionList( NULL, subscriptionCount );
+    __CPROVER_assume( isValidMqttSubscriptionList( pSubscriptionList, subscriptionCount ) );
+
+    pFixedBuffer = allocateMqttFixedBuffer( NULL );
+    __CPROVER_assume( isValidMqttFixedBuffer( pFixedBuffer ) );
+
+    /* Before calling MQTT_SerializeUnsubscribe() it is up to the application to
+     * make sure that the information in the list of MQTTSubscribeInfo_t can fit
+     * into the MQTTFixedBuffer_t. It is a violation of the API to call
+     * MQTT_SerializeUnsubscribe() without first calling MQTT_GetUnsubscribePacketSize(). */
+    if( pSubscriptionList != NULL )
+    {
+        /* The output parameter pPacketSize of the function MQTT_GetConnectPacketSize()
+         * must not be NULL. packetSize returned is not used in this proof, but 
+         * is used normally by the application to verify the size of their 
+         * MQTTFixedBuffer_t. MQTT_SerializeConnect() will use the remainingLength 
+         * to recalculate the packetSize. */
+        status = MQTT_GetUnsubscribePacketSize( pSubscriptionList,
+                                                subscriptionCount,
+                                                &remainingLength,
+                                                &packetSize );
+    }
+
+    if( status == MQTTSuccess )
+    {
+        /* For coverage it is expected that a NULL pSubscriptionList could
+         * reach this function. */
+        MQTT_SerializeUnsubscribe( pSubscriptionList,
+                                   subscriptionCount,
+                                   packetId,
+                                   remainingLength,
+                                   pFixedBuffer );
+    }
+}

cbmc/proofs/MQTT_SerializeUnsubscribe/Makefile

@@ -0,0 +1,25 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=MQTT_SerializeUnsubscribe_harness
+
+# Bind the subscription count. Please see the default value in mqtt_cbmc_state.c
+# for more information on this bound. This is set to 2 currently to have the proof
+# run quickly.
+SUBSCRIPTION_COUNT_MAX=2
+DEFINES += -DSUBSCRIPTION_COUNT_MAX=$(SUBSCRIPTION_COUNT_MAX)
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += allocateMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX)
+UNWINDSET += isValidMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX)
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX)
+UNWINDSET += MQTT_SerializeUnsubscribe.0:$(SUBSCRIPTION_COUNT_MAX)
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:4
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_SerializeUnsubscribe/README.md

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

cbmc/proofs/MQTT_SerializeUnsubscribe/cbmc-batch.yaml

@@ -0,0 +1,2 @@
+# This file marks this directory as containing a CBMC proof.
+# The contents of this file will be generated by continuous integration.

cbmc/proofs/MQTT_SerializeUnsubscribe/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "MQTT_SerializeUnsubscribe",
+  "proof-root": "libraries/standard/mqtt/cbmc/proofs"
+}

cbmc/sources/mqtt_cbmc_state.c

@@ -22,6 +22,15 @@
 #include <stdlib.h>
 #include "mqtt_cbmc_state.h"
 
+/* A default bound on the subscription count. Iterating over possibly SIZE_MAX
+ * number of subscriptions does not add any value to the proofs. An application
+ * can allocate memory for as many subscriptions as their system can handle.
+ * The proofs verify that the code can handle the maximum topicFilterLength in
+ * each subscription. */
+#ifndef SUBSCRIPTION_COUNT_MAX
+    #define SUBSCRIPTION_COUNT_MAX    1U
+#endif
+
 void * mallocCanFail( size_t size )
 {
     __CPROVER_assert( size < CBMC_MAX_OBJECT_SIZE, "mallocCanFail size is too big" );
@@ -126,29 +135,66 @@ bool isValidMqttConnectInfo( const MQTTConnectInfo_t * pConnectInfo )
     return isValid;
 }
 
-MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pBuffer )
+MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pFixedBuffer )
 {
-    if( pBuffer == NULL )
+    if( pFixedBuffer == NULL )
     {
-        pBuffer = mallocCanFail( sizeof( MQTTFixedBuffer_t ) );
+        pFixedBuffer = mallocCanFail( sizeof( MQTTFixedBuffer_t ) );
     }
 
-    if( pBuffer != NULL )
+    if( pFixedBuffer != NULL )
     {
-        __CPROVER_assume( pBuffer->size < CBMC_MAX_OBJECT_SIZE );
+        __CPROVER_assume( pFixedBuffer->size < CBMC_MAX_OBJECT_SIZE );
-        pBuffer->pBuffer = mallocCanFail( pBuffer->size );
+        pFixedBuffer->pBuffer = mallocCanFail( pFixedBuffer->size );
     }
 
-    return pBuffer;
+    return pFixedBuffer;
 }
 
-bool isValidMqttFixedBuffer( const MQTTFixedBuffer_t * pBuffer )
+bool isValidMqttFixedBuffer( const MQTTFixedBuffer_t * pFixedBuffer )
 {
     bool isValid = true;
 
-    if( pBuffer != NULL )
+    if( pFixedBuffer != NULL )
     {
-        isValid = pBuffer->size < CBMC_MAX_OBJECT_SIZE;
+        isValid = pFixedBuffer->size < CBMC_MAX_OBJECT_SIZE;
+    }
+
+    return isValid;
+}
+
+MQTTSubscribeInfo_t * allocateMqttSubscriptionList( MQTTSubscribeInfo_t * pSubscriptionList,
+                                                    size_t subscriptionCount )
+{
+    if( pSubscriptionList == NULL )
+    {
+        __CPROVER_assume( sizeof( MQTTSubscribeInfo_t ) * subscriptionCount < CBMC_MAX_OBJECT_SIZE );
+        pSubscriptionList = mallocCanFail( sizeof( MQTTSubscribeInfo_t ) * subscriptionCount );
+    }
+
+    if( pSubscriptionList != NULL )
+    {
+        for( int i = 0; i < subscriptionCount; i++ )
+        {
+            __CPROVER_assume( pSubscriptionList[ i ].topicFilterLength < CBMC_MAX_OBJECT_SIZE );
+            pSubscriptionList[ i ].pTopicFilter = mallocCanFail( pSubscriptionList[ i ].topicFilterLength );
+        }
+    }
+
+    return pSubscriptionList;
+}
+
+bool isValidMqttSubscriptionList( MQTTSubscribeInfo_t * pSubscriptionList,
+                                  size_t subscriptionCount )
+{
+    bool isValid = true;
+
+    if( pSubscriptionList != NULL )
+    {
+        for( int i = 0; i < subscriptionCount; i++ )
+        {
+            isValid = isValid && ( pSubscriptionList[ i ].topicFilterLength < CBMC_MAX_OBJECT_SIZE );
+        }
     }
 
     return isValid;