From 4ae7977438e103f975b52dea8bb2c1fc5b851cd2 Mon Sep 17 00:00:00 2001 From: Allan Li Date: Wed, 5 Aug 2026 22:02:10 +0000 Subject: [PATCH] Fix subscribe wildcard check bounds --- source/core_mqtt.c | 11 ++- ...QTT_Subscribe_BoundedTopicFilter_harness.c | 97 +++++++++++++++++++ .../Makefile | 76 +++++++++++++++ .../README.md | 22 +++++ .../cbmc-proof.txt | 1 + .../cbmc-viewer.json | 7 ++ test/unit-test/core_mqtt_utest.c | 48 +++++++++ 7 files changed, 260 insertions(+), 2 deletions(-) create mode 100644 test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/MQTT_Subscribe_BoundedTopicFilter_harness.c create mode 100644 test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/Makefile create mode 100644 test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/README.md create mode 100644 test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/cbmc-proof.txt create mode 100644 test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/cbmc-viewer.json diff --git a/source/core_mqtt.c b/source/core_mqtt.c index 4cb099d7e..bcb873d08 100644 --- a/source/core_mqtt.c +++ b/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; } diff --git a/test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/MQTT_Subscribe_BoundedTopicFilter_harness.c b/test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/MQTT_Subscribe_BoundedTopicFilter_harness.c new file mode 100644 index 000000000..ca3e9c5ff --- /dev/null +++ b/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 ); +} diff --git a/test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/Makefile b/test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/Makefile new file mode 100644 index 000000000..e2fed70f0 --- /dev/null +++ b/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 diff --git a/test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/README.md b/test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/README.md new file mode 100644 index 000000000..749e3ece4 --- /dev/null +++ b/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. diff --git a/test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/cbmc-proof.txt b/test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/cbmc-proof.txt new file mode 100644 index 000000000..6ed46f125 --- /dev/null +++ b/test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/cbmc-viewer.json b/test/cbmc/proofs/MQTT_Subscribe_BoundedTopicFilter/cbmc-viewer.json new file mode 100644 index 000000000..ff65e9817 --- /dev/null +++ b/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" +} diff --git a/test/unit-test/core_mqtt_utest.c b/test/unit-test/core_mqtt_utest.c index 415a157b1..ceb07ced3 100644 --- a/test/unit-test/core_mqtt_utest.c +++ b/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;