Proof for MQTT_MatchTopic API (#1137)

cbmc/proofs/MQTT_MatchTopic/MQTT_MatchTopic_harness.c

@@ -0,0 +1,49 @@
+/*
+ * 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_MatchTopic_harness.c
+ * @brief Implements the proof harness for MQTT_MatchTopic function.
+ */
+
+#include "mqtt.h"
+#include "mqtt_cbmc_state.h"
+
+void harness()
+{
+    const char * pTopicName;
+    uint16_t nameLength;
+    const char * pTopicFilter;
+    uint16_t filterLength;
+    bool * pMatchResult;
+
+    __CPROVER_assume( nameLength < MAX_TOPIC_NAME_FILTER_LENGTH );
+    pTopicName = mallocCanFail( ( sizeof( char ) * nameLength ) );
+    __CPROVER_assume( filterLength < MAX_TOPIC_NAME_FILTER_LENGTH );
+    pTopicFilter = mallocCanFail( ( sizeof( char ) * filterLength ) );
+    pMatchResult = mallocCanFail( sizeof( bool ) );
+
+    MQTT_MatchTopic( pTopicName,
+                     nameLength,
+                     pTopicFilter,
+                     filterLength,
+                     pMatchResult );
+}

cbmc/proofs/MQTT_MatchTopic/Makefile

@@ -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.
+#
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=MQTT_MatchTopic_harness
+
+# The topic name/filter length are bounded, so that the loops in topic matching algorithmic
+# functions called by MQTT_MatchTopic can be unwound to an expected
+# amount that won't make the proof run too long.
+MAX_TOPIC_NAME_FILTER_LENGTH=10
+
+DEFINES += -DMAX_TOPIC_NAME_FILTER_LENGTH=$(MAX_TOPIC_NAME_FILTER_LENGTH)
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += __CPROVER_file_local_mqtt_c_matchTopicFilter.0:$(MAX_TOPIC_NAME_FILTER_LENGTH)
+UNWINDSET += strncmp.0:$(MAX_TOPIC_NAME_FILTER_LENGTH)
+UNWINDSET += __CPROVER_file_local_mqtt_c_matchWildcards.0:$(MAX_TOPIC_NAME_FILTER_LENGTH)
+
+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.c
+
+include ../Makefile.common

cbmc/proofs/MQTT_MatchTopic/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_MatchTopic/cbmc-viewer.json

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

lexicon.txt

@@ -33,8 +33,8 @@ connectinfo
 connectpacketsize
 const
 createcleansession
-currentstate
 csdk
+currentstate
 defragmenting
 deserialization
 deserializationresult
@@ -49,9 +49,9 @@ disconnectpacketsize
 doesn
 doxygen
 dup
-endcond
 emptyindex
 endcode
+endcond
 endif
 enum
 enums
@@ -176,8 +176,8 @@ payloadlength
 pbuffer
 pbuffertosend
 pcallbacks
-pconnack
 pclientidentifier
+pconnack
 pconnectinfo
 pcontext
 pcurrentstate
@@ -185,9 +185,8 @@ pcursor
 pdeserialized
 pdeserializedinfo
 pdestination
-ppacketidentifier
-ppingresp
 pem
+pfilterindex
 pfixedbuffer
 pheadersize
 pincomingpacket
@@ -206,12 +205,14 @@ pnetworkinterface
 pnewstate
 posix
 ppacketid
+ppacketidentifier
 ppacketinfo
 ppacketsize
 ppassword
 ppayload
 ppayloadsize
 ppayloadstart
+ppingresp
 ppubinfo
 ppublishinfo
 pqos

src/mqtt.c

@@ -318,7 +318,11 @@ static MQTTStatus_t validatePublishParams( const MQTTContext_t * pContext,
                                            uint16_t packetId );
 
 /**
- * topic filter, this function handles the following 2 cases:
+ * @brief Performs matching for special cases when the passed topic filter
+ * ends with a wildcard character.
+ *
+ * When the topic name has been consumed but there are remaining characters to
+ * to match in the topic filter, this function handles the following 2 cases:
  * - When the topic filter ends with "/+" or "/#" characters, but the topic
  * name only ends with '/'.
  * - When the topic filter ends with "/#" characters, but the topic name
@@ -350,9 +354,10 @@ static bool matchEndWildcardsSpecialCases( const char * pTopicFilter,
  * @param[in] topicNameLength Length of the topic name.
  * @param[in] pTopicFilter The topic filter to match.
  * @param[in] topicFilterLength Length of the topic filter.
- * @param[in,out] pNameIndex Current index in topic name being examined.. It is
+ * @param[in,out] pNameIndex Current index in the topic name being examined. It is
  * advanced by one level for `+` wildcards.
- * @param[in] filterIndex Current index in the topic filter being examined..
+ * @param[in, out] pFilterIndex Current index in the topic filter being examined.
+ * It is advanced to position of '/' level separator for '+' wildcard.
  * @param[out] pMatch Whether the topic filter and topic name match.
  *
  * @return `true` if the caller of this function should exit; `false` if the
@@ -363,7 +368,7 @@ static bool matchWildcards( const char * pTopicName,
                             const char * pTopicFilter,
                             uint16_t topicFilterLength,
                             uint16_t * pNameIndex,
-                            uint16_t filterIndex,
+                            uint16_t * pFilterIndex,
                             bool * pMatch );
 
 /**
@@ -396,7 +401,8 @@ static bool matchEndWildcardsSpecialCases( const char * pTopicFilter,
      * "/#". This check handles the case to match filter "sport/#" with topic
      * "sport". The reason is that the '#' wildcard represents the parent and
      * any number of child levels in the topic name.*/
-    if( ( filterIndex == ( topicFilterLength - 3U ) ) &&
+    if( ( topicFilterLength >= 3U ) &&
+        ( filterIndex == ( topicFilterLength - 3U ) ) &&
         ( pTopicFilter[ filterIndex + 1U ] == '/' ) &&
         ( pTopicFilter[ filterIndex + 2U ] == '#' ) )
 
@@ -428,7 +434,7 @@ static bool matchWildcards( const char * pTopicName,
                             const char * pTopicFilter,
                             uint16_t topicFilterLength,
                             uint16_t * pNameIndex,
-                            uint16_t filterIndex,
+                            uint16_t * pFilterIndex,
                             bool * pMatch )
 {
     bool shouldStopMatching = false;
@@ -439,56 +445,86 @@ static bool matchWildcards( const char * pTopicName,
     assert( pTopicFilter != NULL );
     assert( topicFilterLength != 0 );
     assert( pNameIndex != NULL );
+    assert( pFilterIndex != NULL );
     assert( pMatch != NULL );
 
     /* Wild card in a topic filter is only valid either at the starting position
      * or when it is preceded by a '/'.*/
-    locationIsValidForWildcard = ( ( filterIndex == 0u ) ||
-                                   ( pTopicFilter[ filterIndex - 1U ] == '/' )
+    locationIsValidForWildcard = ( ( *pFilterIndex == 0u ) ||
+                                   ( pTopicFilter[ *pFilterIndex - 1U ] == '/' )
                                    ) ? true : false;
 
-    if( locationIsValidForWildcard == true )
+    if( ( pTopicFilter[ *pFilterIndex ] == '+' ) && ( locationIsValidForWildcard == true ) )
     {
-        if( pTopicFilter[ filterIndex ] == '+' )
+        bool nextLevelExistsInTopicName = false;
+        bool nextLevelExistsinTopicFilter = false;
+
+        /* Move topic name index to the end of the current level. The end of the
+         * current level is identified by the last character before the next level
+         * separator '/'. */
+        while( *pNameIndex < topicNameLength )
         {
-            /* Move topic name index to the end of the current level. The end of the
-             * current level is identified by '/'. */
-            while( ( *pNameIndex < topicNameLength ) && ( pTopicName[ *pNameIndex ] != '/' ) )
+            /* Exit the loop if we hit the level separator. */
+            if( pTopicName[ *pNameIndex ] == '/' )
             {
-                ( *pNameIndex )++;
+                nextLevelExistsInTopicName = true;
+                break;
             }
 
-            /* Decrement the topic name index for 2 different cases:
-             * - If the break condition is ( *pNameIndex < topicNameLength ), then
-             *   we have reached past the end of the topic name and we move back the
-             *   the index on the last character.
-             * - If the break condition is ( pTopicName[ *pNameIndex ] != '/' ), we
-             *   move back the index on the '/' character. */
-            ( *pNameIndex )--;
+            ( *pNameIndex )++;
         }
 
-        /* '#' matches everything remaining in the topic name. It must be the
-         * last character in a topic filter. */
-        else if( ( pTopicFilter[ filterIndex ] == '#' ) &&
-                 ( filterIndex == ( topicFilterLength - 1U ) ) )
+        /* Determine if the topic filter contains a child level after the current level
+         * represented by the '+' wildcard. */
+        if( ( *pFilterIndex < ( topicFilterLength - 1U ) ) &&
+            ( pTopicFilter[ *pFilterIndex + 1U ] == '/' ) )
         {
-            /* Subsequent characters don't need to be checked for the
-             * multi-level wildcard. */
-            *pMatch = true;
-            shouldStopMatching = true;
+            nextLevelExistsinTopicFilter = true;
         }
-        else
+
+        /* If the topic name contains a child level but the topic filter ends at
+         * the current level, then there does not exist a match. */
+        if( ( nextLevelExistsInTopicName == true ) &&
+            ( nextLevelExistsinTopicFilter == false ) )
         {
-            /* Any character mismatch other than '+' or '#' means the topic
-             * name does not match the topic filter. */
             *pMatch = false;
             shouldStopMatching = true;
         }
+
+        /* If the topic name and topic filter have child levels, then advance the
+         * filter index to the level separator in the topic filter, so that match
+         * can be performed in the next level.
+         * Note: The name index already points to the level separator in the topic
+         * name. */
+        else if( nextLevelExistsInTopicName == true )
+        {
+            ( *pFilterIndex )++;
+        }
+        else
+        {
+            /* If we have reached here, the the loop terminated on the
+             * ( *pNameIndex < topicNameLength) condition, which means that have
+             * reached past the end of the topic name, and thus, we decrement the
+             * index to the last character in the topic name.*/
+            ( *pNameIndex )--;
+        }
+    }
+
+    /* '#' matches everything remaining in the topic name. It must be the
+     * last character in a topic filter. */
+    else if( ( pTopicFilter[ *pFilterIndex ] == '#' ) &&
+             ( *pFilterIndex == ( topicFilterLength - 1U ) ) &&
+             ( locationIsValidForWildcard == true ) )
+    {
+        /* Subsequent characters don't need to be checked for the
+         * multi-level wildcard. */
+        *pMatch = true;
+        shouldStopMatching = true;
     }
     else
     {
-        /* If the location is not valid for a wildcard, the topic name does not
-         * match the topic filter. */
+        /* Any character mismatch other than '+' or '#' means the topic
+         * name does not match the topic filter. */
         *pMatch = false;
         shouldStopMatching = true;
     }
@@ -535,7 +571,7 @@ static bool matchTopicFilter( const char * pTopicName,
                                                  pTopicFilter,
                                                  topicFilterLength,
                                                  &nameIndex,
-                                                 filterIndex,
+                                                 &filterIndex,
                                                  &matchFound );
         }
 

utest/mqtt_utest.c

@@ -2251,6 +2251,15 @@ void test_MQTT_MatchTopic_Wildcard_SingleLevel( void )
                                                      &matchResult ) );
     TEST_ASSERT_EQUAL( false, matchResult );
 
+    pTopicName = "/";
+    pTopicFilter = "+";
+    TEST_ASSERT_EQUAL( MQTTSuccess, MQTT_MatchTopic( pTopicName,
+                                                     strlen( pTopicName ),
+                                                     pTopicFilter,
+                                                     strlen( pTopicFilter ),
+                                                     &matchResult ) );
+    TEST_ASSERT_EQUAL( false, matchResult );
+
     /* Test with '+' as the topic filter. */
     pTopicName = "test";
     pTopicFilter = "+";