CBMC Proofs for MQTT and Some HTTPClient_Send proof updates (#1079)

* Add MQTT proofs:

MQTT_Connect
MQTT_Disconnect Proof
MQTT_Publish
MQTT_Subscribe harness
MQTT_Unsubscribe
MQTT_ReceiveLoop proof

* Add some clarification comments.

cbmc/.gitignore

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

cbmc/include/mqtt_config.h

@@ -41,6 +41,17 @@ struct NetworkContext
  * @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 )
+#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 )
 
 #endif /* ifndef MQTT_CONFIG_H_ */

cbmc/proofs/MQTT_Connect/MQTT_Connect_harness.c

@@ -0,0 +1,54 @@
+/*
+ * 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_Connect_harness.c
+ * @brief Implements the proof harness for MQTT_Connect function.
+ */
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTContext_t * pContext;
+    MQTTConnectInfo_t * pConnectInfo;
+    MQTTPublishInfo_t * pWillInfo;
+    uint32_t timeoutMs;
+    bool * pSessionPresent;
+
+    pContext = allocateMqttContext( NULL );
+    __CPROVER_assume( isValidMqttContext( pContext ) );
+
+    pConnectInfo = allocateMqttConnectInfo( NULL );
+    __CPROVER_assume( isValidMqttConnectInfo( pConnectInfo ) );
+
+    pWillInfo = allocateMqttPublishInfo( NULL );
+    __CPROVER_assume( isValidMqttPublishInfo( pWillInfo ) );
+
+    pSessionPresent = mallocCanFail( sizeof( bool ) );
+
+    /* The MQTT_RECEIVE_TIMEOUT is used here to control the number of loops
+     * when receiving on the network. The default is used here because memory
+     * safety can be proven in only a few iterations. */
+    __CPROVER_assume( timeoutMs < MQTT_RECEIVE_TIMEOUT );
+
+    MQTT_Connect( pContext, pConnectInfo, pWillInfo, timeoutMs, pSessionPresent );
+}

cbmc/proofs/MQTT_Connect/Makefile

@@ -0,0 +1,83 @@
+#
+# 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_Connect_harness
+
+# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for
+# more information on MAX_NETWORK_SEND_TRIES.
+MAX_NETWORK_SEND_TRIES=3
+# Bound on the timeout in receiveConnack. This timeout is bounded because
+# memory saftey can be proven in a only a few iteration of the MQTT operations.
+# Each iteration will try to receive a single packet in its entirety. With a
+# time out of 3 we can get coverage of the entire function. Another iteration
+# performed will unnecessarily duplicate the proof.
+MQTT_RECEIVE_TIMEOUT=3
+# Please see libraries/standard/mqtt/cbmc/include/mqtt_config.h for more
+# information on these defines.
+MQTT_STATE_ARRAY_MAX_COUNT=11
+MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT=3
+DEFINES += -DMQTT_RECEIVE_TIMEOUT=$(MQTT_RECEIVE_TIMEOUT)
+DEFINES += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES)
+INCLUDES +=
+
+# These functions do not coincide with the call graph of MQTT_Connect, but are
+# found by CBMC during processing in logs/MQTT_Connect_harness3.txt. We remove
+# the function bodies to improve coverage accuracy.
+REMOVE_FUNCTION_BODY += MQTT_ProcessLoop
+REMOVE_FUNCTION_BODY += MQTT_ReceiveLoop
+REMOVE_FUNCTION_BODY += __CPROVER_file_local_mqtt_c_handleIncomingPublish
+REMOVE_FUNCTION_BODY += __CPROVER_file_local_mqtt_c_handleKeepAlive
+
+# The loops below are unwound once more than the timeout. The loops below use
+# the user passed in timeout to break the loop.
+UNWINDSET += __CPROVER_file_local_mqtt_c_recvExact.0:$(MQTT_RECEIVE_TIMEOUT)
+UNWINDSET += __CPROVER_file_local_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT)
+# If the user passed in timeout is zero, then the loop will run until the
+# MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT is reached.
+UNWINDSET += __CPROVER_file_local_mqtt_c_receiveConnack.0:$(MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT)
+# Unlike recvExact, sendPacket is not bounded by the timeout. The loop in
+# sendPacket will continue until all the bytes are sent or a network error
+# occurs. Please see NetworkInterfaceReceiveStub in
+# libraries\standard\mqtt\cbmc\stubs\network_interface_stubs.c for more
+# information.
+UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES)
+# The loops are unwound 5 times because these functions divides a size_t 
+# variable by 128 until it reaches zero to stop the loop.
+# log128(SIZE_MAX) = 4.571...
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_getRemainingLength.0:5
+# This loop will run for the maximum number of publishes pending
+# acknowledgements plus one. This value is set in
+# libraries/standard/mqtt/cbmc/include/mqtt_config.h.
+UNWINDSET += __CPROVER_file_local_mqtt_state_c_stateSelect.0:$(MQTT_STATE_ARRAY_MAX_COUNT)
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/event_callback_stub.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/memcpy.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_state.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_Connect/README.md

@@ -0,0 +1,10 @@
+MQTT_Connect proof
+==============
+
+This directory contains a memory safety proof for MQTT_Connect.
+
+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_Connect/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_Connect/cbmc-viewer.json

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

cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_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_Disconnect_harness.c
+ * @brief Implements the proof harness for MQTT_Disconnect function.
+ */
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTContext_t * pContext;
+
+    pContext = allocateMqttContext( NULL );
+    __CPROVER_assume( isValidMqttContext( pContext ) );
+
+    MQTT_Disconnect( pContext );
+}

cbmc/proofs/MQTT_Disconnect/Makefile

@@ -0,0 +1,48 @@
+#
+# 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_Disconnect_harness
+
+# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for
+# more information on MAX_NETWORK_SEND_TRIES.
+MAX_NETWORK_SEND_TRIES=3
+DEFINES += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES)
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+# Unlike recvExact, sendPacket is not bounded by the timeout. The loop in
+# sendPacket will continue until all the bytes are sent or a network error
+# occurs. Please see NetworkInterfaceReceiveStub in 
+# libraries\standard\mqtt\cbmc\stubs\network_interface_stubs.c for more 
+# information.
+UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES)
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/event_callback_stub.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_state.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_Disconnect/README.md

@@ -0,0 +1,10 @@
+MQTT_Disconnect proof
+==============
+
+This directory contains a memory safety proof for MQTT_Disconnect.
+
+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_Disconnect/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_Disconnect/cbmc-viewer.json

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

cbmc/proofs/MQTT_Ping/Makefile

@@ -23,7 +23,7 @@ HARNESS_ENTRY=harness
 HARNESS_FILE=MQTT_Ping_harness
 
 # Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for
-# more information on the MAX_NETWORK_SEND_TRIES.
+# more information on MAX_NETWORK_SEND_TRIES.
 MAX_NETWORK_SEND_TRIES=3
 DEFINES += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES)
 INCLUDES +=

cbmc/proofs/MQTT_ProcessLoop/MQTT_ProcessLoop_harness.c

@@ -25,9 +25,6 @@
  */
 #include "mqtt.h"
 #include "mqtt_cbmc_state.h"
-#include "network_interface_stubs.h"
-#include "get_time_stub.h"
-#include "event_callback_stub.h"
 
 void harness()
 {
@@ -37,10 +34,11 @@ void harness()
     pContext = allocateMqttContext( NULL );
     __CPROVER_assume( isValidMqttContext( pContext ) );
 
-    __CPROVER_assume( timeoutMs < MQTT_PROCESS_LOOP_TIMEOUT );
-
-    /* The MQTT_PROCESS_LOOP_TIMEOUT is used here to control the number of loops
+    /* The MQTT_RECEIVE_TIMEOUT is used here to control the number of loops
      * when receiving on the network. The default is used here because memory
-     * safety can be proven in only a few iterations. */
+     * safety can be proven in only a few iterations. Please see this proof's
+     * Makefile for more information. */
+    __CPROVER_assume( timeoutMs < MQTT_RECEIVE_TIMEOUT );
+
     MQTT_ProcessLoop( pContext, timeoutMs );
 }

cbmc/proofs/MQTT_ProcessLoop/Makefile

@@ -27,14 +27,14 @@ HARNESS_FILE=MQTT_ProcessLoop_harness
 # Each iteration will try to receive a single packet in its entirey. With a time
 # out of 2 we can get coverage of the entire function. Another iteration will
 # performed unnecessarily duplicating of the proof.
-MQTT_PROCESS_LOOP_TIMEOUT=3
-# Please see libraries/mqtt/cbmc/stubs/network_interface_subs.c for more
-# information on the MAX_NETWORK_SEND_TRIES.
+MQTT_RECEIVE_TIMEOUT=3
+# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for
+# more information on MAX_NETWORK_SEND_TRIES.
 MAX_NETWORK_SEND_TRIES=3
 # Please see libraries/standard/mqtt/cbmc/include/mqtt_config.h for more
 # information.
 MQTT_STATE_ARRAY_MAX_COUNT=11
-DEFINES += -DMQTT_PROCESS_LOOP_TIMEOUT=$(MQTT_PROCESS_LOOP_TIMEOUT)
+DEFINES += -DMQTT_RECEIVE_TIMEOUT=$(MQTT_RECEIVE_TIMEOUT)
 DEFINES += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES)
 INCLUDES +=
 
@@ -43,9 +43,9 @@ REMOVE_FUNCTION_BODY += MQTT_Ping
 REMOVE_FUNCTION_BODY += MQTT_DeserializeAck
 REMOVE_FUNCTION_BODY += MQTT_SerializeAck
 
-UNWINDSET += MQTT_ProcessLoop.0:$(MQTT_PROCESS_LOOP_TIMEOUT)
-UNWINDSET += __CPROVER_file_local_mqtt_c_discardPacket.0:$(MQTT_PROCESS_LOOP_TIMEOUT)
-UNWINDSET += __CPROVER_file_local_mqtt_c_recvExact.0:$(MQTT_PROCESS_LOOP_TIMEOUT)
+UNWINDSET += MQTT_ProcessLoop.0:$(MQTT_RECEIVE_TIMEOUT)
+UNWINDSET += __CPROVER_file_local_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT)
+UNWINDSET += __CPROVER_file_local_mqtt_c_recvExact.0:$(MQTT_RECEIVE_TIMEOUT)
 # Unlike recvExact, sendPacket is not bounded by the timeout. The loop in
 # sendPacket will continue until all the bytes are sent or a network error
 # occurs. Please see NetworkInterfaceReceiveStub in

cbmc/proofs/MQTT_Publish/MQTT_Publish_harness.c

@@ -0,0 +1,42 @@
+/*
+ * 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_Publish_harness.c
+ * @brief Implements the proof harness for MQTT_Publish function.
+ */
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTContext_t * pContext;
+    MQTTPublishInfo_t * pPublishInfo;
+    uint16_t packetId;
+
+    pContext = allocateMqttContext( NULL );
+    __CPROVER_assume( isValidMqttContext( pContext ) );
+
+    pPublishInfo = allocateMqttPublishInfo( NULL );
+    __CPROVER_assume( isValidMqttPublishInfo( pPublishInfo ) );
+
+    MQTT_Publish( pContext, pPublishInfo, packetId );
+}

cbmc/proofs/MQTT_Publish/Makefile

@@ -0,0 +1,60 @@
+#
+# 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_Publish_harness
+
+# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for
+# more information on MAX_NETWORK_SEND_TRIES.
+MAX_NETWORK_SEND_TRIES=3
+# Please see libraries/standard/mqtt/cbmc/include/mqtt_config.h for more
+# information.
+MQTT_STATE_ARRAY_MAX_COUNT=11
+DEFINES += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES)
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+REMOVE_FUNCTION_BODY +=
+# Unlike recvExact, sendPacket is not bounded by the timeout. The loop in
+# sendPacket will continue until all the bytes are sent or a network error
+# occurs. Please see NetworkInterfaceReceiveStub in 
+# libraries\standard\mqtt\cbmc\stubs\network_interface_stubs.c for more 
+# information.
+UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES)
+# These loops will run for the maximum number of publishes pending acknowledgement.
+# This is set in libraries/standard/mqtt/cbmc/include/mqtt_config.h.
+UNWINDSET += __CPROVER_file_local_mqtt_state_c_addRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT)
+UNWINDSET += __CPROVER_file_local_mqtt_state_c_findInRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT)
+# The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength()
+# divides a size_t variable by 128 until it reaches zero to stop the loop.
+# log128(SIZE_MAX) = 4.571...
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/event_callback_stub.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_state.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_Publish/README.md

@@ -0,0 +1,10 @@
+MQTT_Publish proof
+==============
+
+This directory contains a memory safety proof for MQTT_Publish.
+
+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_Publish/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_Publish/cbmc-viewer.json

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

cbmc/proofs/MQTT_ReceiveLoop/MQTT_ReceiveLoop_harness.c

@@ -0,0 +1,44 @@
+/*
+ * 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_ReceiveLoop_harness.c
+ * @brief Implements the proof harness for MQTT_ReceiveLoop function.
+ */
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTContext_t * pContext;
+    uint32_t timeoutMs;
+
+    pContext = allocateMqttContext( NULL );
+    __CPROVER_assume( isValidMqttContext( pContext ) );
+
+    /* The MQTT_RECEIVE_TIMEOUT is used here to control the number of loops
+     * when receiving on the network. The default is used here because memory
+     * safety can be proven in only a few iterations. Please see this proof's
+     * Makefile for more information. */
+    __CPROVER_assume( timeoutMs < MQTT_RECEIVE_TIMEOUT );
+
+    MQTT_ReceiveLoop( pContext, timeoutMs );
+}

cbmc/proofs/MQTT_ReceiveLoop/Makefile

@@ -0,0 +1,55 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=MQTT_ReceiveLoop_harness
+
+# Bound on the timeout in MQTT_ProcessLoop. This timeout is bounded because 
+# memory saftey can be proven in a only a few iteration of the MQTT operations.
+# Each iteration will try to receive a single packet in its entirety. With a time
+# out of 2 we can get coverage of the entire function. Another iteration will 
+# performed unnecessarily duplicating of the proof.
+MQTT_RECEIVE_TIMEOUT=3
+# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for
+# more information on MAX_NETWORK_SEND_TRIES.
+MAX_NETWORK_SEND_TRIES=3
+# Please see libraries/standard/mqtt/cbmc/include/mqtt_config.h for more
+# information.
+MQTT_STATE_ARRAY_MAX_COUNT=11
+DEFINES += -DMQTT_RECEIVE_TIMEOUT=$(MQTT_RECEIVE_TIMEOUT)
+DEFINES += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES)
+INCLUDES +=
+
+# These functions have their memory saftey proven in other harnesses.
+REMOVE_FUNCTION_BODY += MQTT_DeserializeAck
+REMOVE_FUNCTION_BODY += MQTT_SerializeAck
+
+# The loops below are unwound once more than the exclusive timeout bound.
+UNWINDSET += MQTT_ReceiveLoop.0:$(MQTT_RECEIVE_TIMEOUT)
+UNWINDSET += __CPROVER_file_local_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT)
+UNWINDSET += __CPROVER_file_local_mqtt_c_recvExact.0:$(MQTT_RECEIVE_TIMEOUT)
+# Unlike recvExact, sendPacket is not bounded by the timeout. The loop in
+# sendPacket will continue until all the bytes are sent or a network error
+# occurs. Please see NetworkInterfaceReceiveStub in 
+# libraries\standard\mqtt\cbmc\stubs\network_interface_stubs.c for more 
+# information.
+UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES)
+# The getRemainingLength loop is unwound 5 times because getRemainingLength()
+# divides a size_t variable by 128 until it reaches zero to stop the loop.
+# log128(SIZE_MAX) = 4.571...
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_getRemainingLength.0:5
+# These loops will run for the maximum number of publishes pending acknowledgement.
+# This is set in libraries/standard/mqtt/cbmc/include/mqtt_config.h.
+UNWINDSET += __CPROVER_file_local_mqtt_state_c_addRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT)
+UNWINDSET += __CPROVER_file_local_mqtt_state_c_findInRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT)
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/event_callback_stub.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_state.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_ReceiveLoop/README.md

@@ -0,0 +1,10 @@
+MQTT_ReceiveLoop proof
+==============
+
+This directory contains a memory safety proof for MQTT_ReceiveLoop.
+
+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_ReceiveLoop/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_ReceiveLoop/cbmc-viewer.json

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

cbmc/proofs/MQTT_SerializeConnect/Makefile

@@ -25,11 +25,19 @@ HARNESS_FILE=MQTT_SerializeConnect_harness
 DEFINES +=
 INCLUDES +=
 
-REMOVE_FUNCTION_BODY +=
-UNWINDSET += encodeRemainingLength.0:3
+# This function does not coincide with the call graph of MQTT_Serialize, but are
+# found by CBMC during processing in logs/MQTT_Connect_harness3.txt. We remove
+# the function body to improve coverage accuracy.
+REMOVE_FUNCTION_BODY += MQTT_GetIncomingPacketTypeAndLength
+
+# The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength()
+# divides a size_t variable by 128 until it reaches zero to stop the loop.
+# log128(SIZE_MAX) = 4.571...
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/memcpy.c
 PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
 
 include ../Makefile.common

cbmc/proofs/MQTT_SerializePublish/Makefile

@@ -26,7 +26,10 @@ DEFINES +=
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
-UNWINDSET += encodeRemainingLength.0:4
+# The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength()
+# divides a size_t variable by 128 until it reaches zero to stop the loop.
+# log128(SIZE_MAX) = 4.571...
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c

cbmc/proofs/MQTT_SerializePublishHeader/Makefile

@@ -26,7 +26,10 @@ DEFINES +=
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
-UNWINDSET += encodeRemainingLength.0:4
+# The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength()
+# divides a size_t variable by 128 until it reaches zero to stop the loop.
+# log128(SIZE_MAX) = 4.571...
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c

cbmc/proofs/MQTT_SerializeSubscribe/MQTT_SerializeSubscribe_harness.c

@@ -36,6 +36,8 @@ void harness()
     MQTTFixedBuffer_t * pFixedBuffer;
     MQTTStatus_t status = MQTTSuccess;
 
+    /* Please see the default bound description on SUBSCRIPTION_COUNT_MAX in
+     * mqtt_cbmc_state.c for more information. */
     __CPROVER_assume( subscriptionCount < SUBSCRIPTION_COUNT_MAX );
 
     pSubscriptionList = allocateMqttSubscriptionList( NULL, subscriptionCount );

cbmc/proofs/MQTT_SerializeSubscribe/Makefile

@@ -34,7 +34,10 @@ 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
+# The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength()
+# divides a size_t variable by 128 until it reaches zero to stop the loop.
+# log128(SIZE_MAX) = 4.571...
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c

cbmc/proofs/MQTT_SerializeUnsubscribe/MQTT_SerializeUnsubscribe_harness.c

@@ -39,6 +39,8 @@ void harness()
     MQTTFixedBuffer_t * pFixedBuffer;
     MQTTStatus_t status = MQTTSuccess;
 
+    /* Please see the default bound description on SUBSCRIPTION_COUNT_MAX in
+     * mqtt_cbmc_state.c for more information. */
     __CPROVER_assume( subscriptionCount < SUBSCRIPTION_COUNT_MAX );
 
     pSubscriptionList = allocateMqttSubscriptionList( NULL, subscriptionCount );

cbmc/proofs/MQTT_SerializeUnsubscribe/Makefile

@@ -34,7 +34,10 @@ 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
+# The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength()
+# divides a size_t variable by 128 until it reaches zero to stop the loop.
+# log128(SIZE_MAX) = 4.571...
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c

cbmc/proofs/MQTT_Subscribe/MQTT_Subscribe_harness.c

@@ -0,0 +1,47 @@
+/*
+ * 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_Subscribe_harness.c
+ * @brief Implements the proof harness for MQTT_Subscribe function.
+ */
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTContext_t * pContext;
+    MQTTSubscribeInfo_t * pSubscriptionList;
+    size_t subscriptionCount;
+    uint16_t packetId;
+
+    pContext = allocateMqttContext( NULL );
+    __CPROVER_assume( isValidMqttContext( pContext ) );
+
+    /* Please see the default bound description on SUBSCRIPTION_COUNT_MAX in
+     * mqtt_cbmc_state.c for more information. */
+    __CPROVER_assume( subscriptionCount < SUBSCRIPTION_COUNT_MAX );
+
+    pSubscriptionList = allocateMqttSubscriptionList( NULL, subscriptionCount );
+    __CPROVER_assume( isValidMqttSubscriptionList( pSubscriptionList, subscriptionCount ) );
+
+    MQTT_Subscribe( pContext, pSubscriptionList, subscriptionCount, packetId );
+}

cbmc/proofs/MQTT_Subscribe/Makefile

@@ -0,0 +1,62 @@
+#
+# 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_Subscribe_harness
+
+# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for
+# more information on MAX_NETWORK_SEND_TRIES.
+MAX_NETWORK_SEND_TRIES=3
+# Bound on the 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 += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES)
+DEFINES += -DSUBSCRIPTION_COUNT_MAX=$(SUBSCRIPTION_COUNT_MAX)
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+# Unlike recvExact, sendPacket is not bounded by the timeout. The loop in
+# sendPacket will continue until all the bytes are sent or a network error
+# occurs. Please see NetworkInterfaceReceiveStub in 
+# libraries\standard\mqtt\cbmc\stubs\network_interface_stubs.c for more 
+# information.
+UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES)
+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)
+# The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength()
+# divides a size_t variable by 128 until it reaches zero to stop the loop.
+# log128(SIZE_MAX) = 4.571...
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/event_callback_stub.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_state.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_Subscribe/README.md

@@ -0,0 +1,10 @@
+MQTT_Subscribe proof
+==============
+
+This directory contains a memory safety proof for MQTT_Subscribe.
+
+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_Subscribe/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_Subscribe/cbmc-viewer.json

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

cbmc/proofs/MQTT_Unsubscribe/MQTT_Unsubscribe_harness.c

@@ -0,0 +1,47 @@
+/*
+ * 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_Unsubscribe_harness.c
+ * @brief Implements the proof harness for MQTT_Unsubscribe function.
+ */
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    MQTTContext_t * pContext;
+    MQTTSubscribeInfo_t * pSubscriptionList;
+    size_t subscriptionCount;
+    uint16_t packetId;
+
+    pContext = allocateMqttContext( NULL );
+    __CPROVER_assume( isValidMqttContext( pContext ) );
+
+    /* Please see the default bound description on SUBSCRIPTION_COUNT_MAX in
+     * mqtt_cbmc_state.c for more information. */
+    __CPROVER_assume( subscriptionCount < SUBSCRIPTION_COUNT_MAX );
+
+    pSubscriptionList = allocateMqttSubscriptionList( NULL, subscriptionCount );
+    __CPROVER_assume( isValidMqttSubscriptionList( pSubscriptionList, subscriptionCount ) );
+
+    MQTT_Unsubscribe( pContext, pSubscriptionList, subscriptionCount, packetId );
+}

cbmc/proofs/MQTT_Unsubscribe/Makefile

@@ -0,0 +1,62 @@
+#
+# 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_Unsubscribe_harness
+
+# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for
+# more information on MAX_NETWORK_SEND_TRIES.
+MAX_NETWORK_SEND_TRIES=3
+# Bound on the 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 += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES)
+DEFINES += -DSUBSCRIPTION_COUNT_MAX=$(SUBSCRIPTION_COUNT_MAX)
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+# Unlike recvExact, sendPacket is not bounded by the timeout. The loop in
+# sendPacket will continue until all the bytes are sent or a network error
+# occurs. Please see NetworkInterfaceReceiveStub in 
+# libraries\standard\mqtt\cbmc\stubs\network_interface_stubs.c for more 
+# information.
+UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES)
+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)
+# The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength()
+# divides a size_t variable by 128 until it reaches zero to stop the loop.
+# log128(SIZE_MAX) = 4.571...
+UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c
+PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/event_callback_stub.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c
+PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_state.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_Unsubscribe/README.md

@@ -0,0 +1,10 @@
+MQTT_Unsubscribe proof
+==============
+
+This directory contains a memory safety proof for MQTT_Unsubscribe.
+
+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_Unsubscribe/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_Unsubscribe/cbmc-viewer.json

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

cbmc/proofs/Makefile-project-targets

@@ -1 +0,0 @@
-../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile-project-targets

cbmc/proofs/Makefile-project-targets

@@ -0,0 +1,7 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+################################################################
+# Use this file to give project-specific targets, including targets
+# that may depend on targets defined in Makefile.common.
+################################################################

cbmc/proofs/Makefile-project-testing

@@ -1 +0,0 @@
-../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile-project-testing

cbmc/proofs/Makefile-project-testing

@@ -0,0 +1,8 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+################################################################
+# 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
+################################################################

cbmc/sources/mqtt_cbmc_state.c

@@ -26,20 +26,20 @@
 #include "get_time_stub.h"
 #include "event_callback_stub.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. */
+/* An exclusive 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
+    #define SUBSCRIPTION_COUNT_MAX    2U
 #endif
 
-/* A default bound on the remainingLength in an incoming packet. This bound
- * is used for the MQTT_DeserializeAck() proof to limit the number of iterations
- * on a SUBACK packet's payload bytes. We do not need to iterate an unbounded
- * remaining length amount of bytes to verify memory safety in the dereferencing
- * the SUBACK payload's bytes. */
+/* An exclusive default bound on the remainingLength in an incoming packet. This
+ * bound is used for the MQTT_DeserializeAck() proof to limit the number of
+ * iterations on a SUBACK packet's payload bytes. We do not need to iterate an
+ * unbounded remaining length amount of bytes to verify memory safety in the
+ * dereferencing the SUBACK payload's bytes. */
 #ifndef REMAINING_LENGTH_MAX
     #define REMAINING_LENGTH_MAX    CBMC_MAX_OBJECT_SIZE
 #endif

cbmc/stubs/memcpy.c

@@ -0,0 +1,54 @@
+/*
+ * 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 memcpy.c
+ * @brief A stub for memcpy so that the proofs for functions that call memcpy
+ * run much faster.
+ */
+
+#include <string.h>
+
+/* This is a clang macro not available on linux */
+#ifndef __has_builtin
+    #define __has_builtin( x )    0
+#endif
+
+#if __has_builtin( __builtin___memcpy_chk )
+    void * __builtin___memcpy_chk( void * dest,
+                                   const void * src,
+                                   size_t n,
+                                   size_t m )
+    {
+        __CPROVER_assert( __CPROVER_w_ok( dest, n ), "write" );
+        __CPROVER_assert( __CPROVER_r_ok( src, n ), "read" );
+        return dest;
+    }
+#else
+    void * memcpy( void * dest,
+                   const void * src,
+                   size_t n )
+    {
+        __CPROVER_assert( __CPROVER_w_ok( dest, n ), "write" );
+        __CPROVER_assert( __CPROVER_r_ok( src, n ), "read" );
+        return dest;
+    }
+#endif /* if __has_builtin( __builtin___memcpy_chk ) */

cbmc/stubs/network_interface_stubs.c

@@ -72,7 +72,7 @@ int32_t NetworkInterfaceSendStub( NetworkContext_t * pNetworkContext,
      * iterations. Looping for INT32_MAX times adds no value to the proof.
      * What matters is that the MQTT library can handle all the possible values
      * that could be returned. */
-    if( tries < MAX_NETWORK_SEND_TRIES )
+    if( tries < ( MAX_NETWORK_SEND_TRIES - 1 ) )
     {
         tries++;
     }

lexicon.txt

@@ -74,6 +74,7 @@ int
 iot
 isduplicate
 isn
+linux
 lsb
 lwt
 malloc

src/mqtt.c

@@ -493,6 +493,7 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext,
 
     assert( pContext != NULL );
     assert( pContext->getTime != NULL );
+
     bytesToReceive = pContext->networkBuffer.size;
     getTimeStampMs = pContext->getTime;
 
@@ -693,6 +694,8 @@ static MQTTStatus_t handleKeepAlive( MQTTContext_t * pContext )
     uint32_t now = 0U, keepAliveMs = 0U;
 
     assert( pContext != NULL );
+    assert( pContext->getTime != NULL );
+
     now = pContext->getTime();
     keepAliveMs = 1000U * ( uint32_t ) pContext->keepAliveIntervalSec;
 
@@ -731,6 +734,7 @@ static MQTTStatus_t handleIncomingPublish( MQTTContext_t * pContext,
 
     assert( pContext != NULL );
     assert( pIncomingPacket != NULL );
+    assert( pContext->appCallback != NULL );
 
     status = MQTT_DeserializePublish( pIncomingPacket, &packetIdentifier, &publishInfo );
     LogInfo( ( "De-serialized incoming PUBLISH packet: DeserializerResult=%d.", status ) );
@@ -897,6 +901,7 @@ static MQTTStatus_t handleIncomingAck( MQTTContext_t * pContext,
 
     assert( pContext != NULL );
     assert( pIncomingPacket != NULL );
+    assert( pContext->appCallback != NULL );
 
     appCallback = pContext->appCallback;