Fix subscribe wildcard check bounds

source/core_mqtt.c

@@ -3868,8 +3868,15 @@ static bool checkWildcardSubscriptions( uint8_t isWildcardAvailable,
 
     if( isWildcardAvailable == 0U )
     {
-        if( ( ( strchr( pSubscriptionList[ iterator ].pTopicFilter, ( int32_t ) '#' ) != NULL ) ||
-              ( strchr( pSubscriptionList[ iterator ].pTopicFilter, ( int32_t ) '+' ) != NULL ) ) )
+        const char * pTopicFilter = pSubscriptionList[ iterator ].pTopicFilter;
+        size_t topicFilterLength = pSubscriptionList[ iterator ].topicFilterLength;
+
+        /* Topic filters are length-prefixed (MQTT 5.0 section 1.5.4) and are not
+         * required to be NUL-terminated. Use memchr() bounded by
+         * topicFilterLength rather than strchr() so that the scan stops at the
+         * end of the caller-supplied buffer. */
+        if( ( memchr( pTopicFilter, ( int32_t ) '#', topicFilterLength ) != NULL ) ||
+            ( memchr( pTopicFilter, ( int32_t ) '+', topicFilterLength ) != NULL ) )
         {
             ret = true;
         }

test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/MQTT_Subscribe_BoundedTopicFilter_harness.c

@@ -0,0 +1,97 @@
+/*
+ * coreMQTT
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * SPDX-License-Identifier: MIT
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/**
+ * @file MQTT_Subscribe_BoundedTopicFilter_harness.c
+ * @brief Proof harness for MQTT_Subscribe when the broker has reported that
+ * wildcard subscriptions are not available. In that branch coreMQTT scans the
+ * caller-supplied topic filter for the wildcard characters '#' and '+'. The
+ * scan must be bounded by MQTTSubscribeInfo_t::topicFilterLength so it never
+ * reads past the buffer that the caller allocated.
+ *
+ * allocateMqttSubscriptionList() backs each pTopicFilter with a malloc of
+ * exactly topicFilterLength bytes (no NUL terminator). Any read past that
+ * boundary is an out-of-bounds access CBMC will catch.
+ */
+
+#include "core_mqtt.h"
+#include "mqtt_cbmc_state.h"
+#include "core_mqtt_config_defaults.h"
+
+/**
+ * @brief Implement a get time function to return timeout after certain
+ * iterations have been made in the code. This ensures that we do not hit
+ * unwinding error in CBMC.
+ */
+static uint32_t ulGetTimeFunction( void )
+{
+    static uint32_t systemTime = 0;
+
+    if( systemTime >= MAX_NETWORK_SEND_TRIES )
+    {
+        systemTime = systemTime + MQTT_SEND_TIMEOUT_MS + 1;
+    }
+    else
+    {
+        systemTime = systemTime + 1;
+    }
+
+    return systemTime;
+}
+
+MQTTStatus_t MQTT_ValidateSubscribeProperties( bool isSubscriptionIdAvailable,
+                                               const MQTTPropBuilder_t * propBuilder )
+{
+    MQTTStatus_t status;
+
+    return status;
+}
+
+void harness()
+{
+    MQTTContext_t * pContext;
+    MQTTSubscribeInfo_t * pSubscriptionList;
+    MQTTPropBuilder_t * propBuffer;
+    uint16_t packetId;
+
+    pContext = allocateMqttContext( NULL );
+    __CPROVER_assume( isValidMqttContext( pContext ) );
+
+    if( pContext != NULL )
+    {
+        pContext->getTime = ulGetTimeFunction;
+
+        /* Force the validation path that scans the topic filter for the
+         * wildcard characters. */
+        pContext->connectionProperties.isWildcardAvailable = 0U;
+    }
+
+    pSubscriptionList = allocateMqttSubscriptionList( NULL, 1U );
+    __CPROVER_assume( isValidMqttSubscriptionList( pSubscriptionList, 1U ) );
+
+    propBuffer = allocateMqttPropBuilder( NULL );
+    __CPROVER_assume( isValidMqttPropBuilder( propBuffer ) );
+
+    MQTT_Subscribe( pContext, pSubscriptionList, 1U, packetId, propBuffer );
+}

test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/Makefile

@@ -0,0 +1,76 @@
+#
+# Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# SPDX-License-Identifier: MIT
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy of
+# this software and associated documentation files (the "Software"), to deal in
+# the Software without restriction, including without limitation the rights to
+# use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+# the Software, and to permit persons to whom the Software is furnished to do so,
+# subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+# FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+# COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+# IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+# CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+#
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=MQTT_Subscribe_BoundedTopicFilter_harness
+PROOF_UID=MQTT_Subscribe_BoundedTopicFilter
+
+# Bound on the topic-filter length used by the proof. Kept small so the proof
+# terminates quickly. The OOB-read property does not depend on the length, so
+# a tight bound is sufficient to expose any over-read.
+MAX_TOPIC_NAME_FILTER_LENGTH=4
+# Loops that iterate over the subscription list (allocateMqttSubscriptionList,
+# validateSubscribeUnsubscribeParams, calculateSubscriptionPacketSize) need an
+# unwind bound of count+1 to discharge their termination assertions. The harness
+# uses a single subscription, so this must be at least 2 (matches the upstream
+# MQTT_Subscribe proof).
+SUBSCRIPTION_COUNT_MAX=2
+SUBSCRIBE_PACKET_VECTORS=7
+MAX_NETWORK_SEND_TRIES=3
+
+DEFINES += -DMAX_TOPIC_NAME_FILTER_LENGTH=$(MAX_TOPIC_NAME_FILTER_LENGTH)
+DEFINES += -DSUBSCRIPTION_COUNT_MAX=$(SUBSCRIPTION_COUNT_MAX)
+DEFINES += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES)
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY += MQTT_ValidateSubscribeProperties
+
+# Bound the scan-for-wildcard loops by the topic filter length. The harness
+# allocates pTopicFilter to exactly topicFilterLength bytes, so any iteration
+# past that bound is an out-of-bounds access CBMC will report.
+UNWINDSET += strchr.0:$(MAX_TOPIC_NAME_FILTER_LENGTH)
+UNWINDSET += memchr.0:$(MAX_TOPIC_NAME_FILTER_LENGTH)
+UNWINDSET += allocateMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX)
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_validateSharedSubscriptions.0:$(MAX_TOPIC_NAME_FILTER_LENGTH)
+UNWINDSET += __CPROVER_file_local_core_mqtt_serializer_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX)
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_validateSubscribeUnsubscribeParams.0:$(SUBSCRIPTION_COUNT_MAX)
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_validateSubscribeUnsubscribeParams.1:$(SUBSCRIPTION_COUNT_MAX)
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendMessageVector.0:${SUBSCRIBE_PACKET_VECTORS}
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendMessageVector.1:${SUBSCRIBE_PACKET_VECTORS}
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendMessageVector.2:${SUBSCRIBE_PACKET_VECTORS}
+UNWINDSET += encodeVariableLength.0:5
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendSubscribeWithoutCopy.0:$(MAX_NETWORK_SEND_TRIES)
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendSubscribeWithoutCopy.1:$(MAX_NETWORK_SEND_TRIES)
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/network_interface_stubs.c
+PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/get_time_stub.c
+PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/event_callback_stub.c
+PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
+PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c
+PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_serializer.c
+PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_serializer_private.c
+PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_state.c
+
+include ../Makefile.common

test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/README.md

@@ -0,0 +1,22 @@
+MQTT_Subscribe_BoundedTopicFilter proof
+=======================================
+
+This directory contains a memory safety proof for `MQTT_Subscribe` along the
+validation path that exercises the file-local `checkWildcardSubscriptions`
+helper.
+
+`checkWildcardSubscriptions` scans the caller-supplied topic filter for the
+two wildcard characters defined by the MQTT specification. The scan must be
+bounded by the caller-supplied `MQTTSubscribeInfo_t::topicFilterLength`
+because `pTopicFilter` is a length-prefixed buffer that is not required to
+be NUL-terminated.
+
+The proof confirms that, when invoked along the wildcard-validation path,
+`MQTT_Subscribe` never reads past the end of the `pTopicFilter` buffer that
+`allocateMqttSubscriptionList()` allocated for it.
+
+To run the proof.
+* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer
+  to your path.
+* Run "make".
+* Open html/index.html in a web browser.

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

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

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

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

test/unit-test/core_mqtt_utest.c

@@ -8490,6 +8490,54 @@ void test_MQTTV5_Subscribe_invalid_params( void )
     TEST_ASSERT_EQUAL_INT( MQTTBadParameter, mqttStatus );
 }
 
+/**
+ * @brief Test that the wildcard check is bounded by topicFilterLength.
+ *
+ * A topic filter is a pointer paired with a separate topicFilterLength and is
+ * not required to be NUL-terminated, so a '#' or '+' byte sitting past
+ * topicFilterLength inside a larger caller-owned buffer must not affect the
+ * result. Two buffers identical within topicFilterLength and differing only at
+ * the byte just past it must therefore produce the same status.
+ */
+void test_MQTTV5_Subscribe_WildcardCheck_HonorsTopicFilterLength( void )
+{
+    MQTTStatus_t cleanStatus;
+    MQTTStatus_t trappedStatus;
+    MQTTContext_t context = { 0 };
+    MQTTSubscribeInfo_t subscribeInfo = { 0 };
+    char cleanBuffer[ 16 ];
+    char trappedBuffer[ 16 ];
+
+    memset( cleanBuffer, 'X', sizeof( cleanBuffer ) );
+    cleanBuffer[ sizeof( cleanBuffer ) - 1U ] = '\0';
+    memcpy( cleanBuffer, "alarm", 5U );
+
+    memcpy( trappedBuffer, cleanBuffer, sizeof( cleanBuffer ) );
+    trappedBuffer[ 5 ] = '#';
+
+    /* Broker reported that wildcards are unavailable, which selects the
+     * wildcard-check branch. */
+    context.connectionProperties.isWildcardAvailable = 0U;
+    subscribeInfo.qos = MQTTQoS0;
+    subscribeInfo.topicFilterLength = 5U;
+
+    /* Reaching the packet-size step returns a sentinel status, distinguishing
+     * it from the MQTTBadParameter the wildcard check would return. Both
+     * buffers are expected to reach this step. */
+    MQTT_GetSubscribePacketSize_ExpectAnyArgsAndReturn( MQTTNoMemory );
+    MQTT_GetSubscribePacketSize_ExpectAnyArgsAndReturn( MQTTNoMemory );
+
+    subscribeInfo.pTopicFilter = cleanBuffer;
+    cleanStatus = MQTT_Subscribe( &context, &subscribeInfo, 1,
+                                  MQTT_FIRST_VALID_PACKET_ID, NULL );
+
+    subscribeInfo.pTopicFilter = trappedBuffer;
+    trappedStatus = MQTT_Subscribe( &context, &subscribeInfo, 1,
+                                    MQTT_FIRST_VALID_PACKET_ID, NULL );
+
+    TEST_ASSERT_EQUAL_INT( cleanStatus, trappedStatus );
+}
+
 void test_MQTTV5_Subscribe_ValidateFailure( void )
 {
     MQTTStatus_t mqttStatus;