Update ThingName to a maximum of 128 characters (#468)

* Update max ThingName size to 128 The AWS IoT Core quota says that thingnames can be up to 128 characters long. This did not match out existing implementation which limited the ThingName to 64 characters. The ThingName may be truncated when added to the ClientToken. --------- Co-authored-by: Cobus van Eeden <35851496+cobusve@users.noreply.github.com>
aws · Feb 15, 2023 · e43672a · e43672a
1 parent 45342aa
commit e43672a
Show file tree

Hide file tree

Showing 9 changed files with 178 additions and 48 deletions.
diff --git a/docs/doxygen/include/size_table.md b/docs/doxygen/include/size_table.md
@@ -9,8 +9,8 @@
     </tr>
     <tr>
         <td>ota.c</td>
-        <td><center>8.3K</center></td>
-        <td><center>7.5K</center></td>
+        <td><center>8.5K</center></td>
+        <td><center>7.6K</center></td>
     </tr>
     <tr>
         <td>ota_interface.c</td>
@@ -25,7 +25,7 @@
     <tr>
         <td>ota_mqtt.c</td>
         <td><center>2.4K</center></td>
-        <td><center>2.2K</center></td>
+        <td><center>2.3K</center></td>
     </tr>
     <tr>
         <td>ota_cbor.c</td>
@@ -39,7 +39,7 @@
     </tr>
     <tr>
         <td><b>Total estimates</b></td>
-        <td><b><center>12.5K</center></b></td>
-        <td><b><center>11.3K</center></b></td>
+        <td><b><center>12.7K</center></b></td>
+        <td><b><center>11.5K</center></b></td>
     </tr>
 </table>
diff --git a/source/include/ota_config_defaults.h b/source/include/ota_config_defaults.h
@@ -133,11 +133,15 @@
  * agent uses this size to allocate static storage for the Thing name used in
  * all OTA base topics. Namely $aws/things/thingName
  *
- * <b>Possible values:</b> Any unsigned 32 integer. <br>
- * <b>Default value:</b> '64'
+ * AWS IoT Core limits the ThingName length to 128 characters maximum. For more,
+ * see the AWS IoT Core Quotas here -
+ * https://console.aws.amazon.com/servicequotas/home/services/iotcore/quotas/L-83BC2FA9
+ *
+ * <b>Possible values:</b> Any unsigned 32 integer - though practical limit is 128 <br>
+ * <b>Default value:</b> '128'
  */
 #ifndef otaconfigMAX_THINGNAME_LEN
-    #define otaconfigMAX_THINGNAME_LEN    64U
+    #define otaconfigMAX_THINGNAME_LEN    128U
 #endif
 
 /**

diff --git a/source/ota_mqtt.c b/source/ota_mqtt.c
@@ -45,24 +45,27 @@
 #include "ota_appversion32.h"
 
 /* Stream GET message constants. */
-#define OTA_CLIENT_TOKEN             "rdy"                  /*!< Arbitrary client token sent in the stream "GET" message. */
+#define OTA_CLIENT_TOKEN                      "rdy"         /*!< Arbitrary client token sent in the stream "GET" message. */
+
+/* Maximum length of ThingName appended onto the ClientToken*/
+#define OTA_CLIENT_TOKEN_MAX_THINGNAME_LEN    53U           /*!<  Max ThingName length = Max client token length (64) - Max request count length (10) - 1 (colon separator) */
 
 /* Agent to Job Service status message constants. */
-#define OTA_STATUS_MSG_MAX_SIZE      128U               /*!< Max length of a job status message to the service. */
+#define OTA_STATUS_MSG_MAX_SIZE               128U          /*!< Max length of a job status message to the service. */
 
 /**
  *  @brief Topic strings used by the OTA process.
  *
  * These first few are topic extensions to the dynamic base topic that includes the Thing name.
  */
-#define MQTT_API_THINGS              "$aws/things/"                   /*!< Topic prefix for thing APIs. */
-#define MQTT_API_JOBS_NEXT_GET       "/jobs/$next/get"                /*!< Topic suffix for job API. */
-#define MQTT_API_JOBS_NOTIFY_NEXT    "/jobs/notify-next"              /*!< Topic suffix for job API. */
-#define MQTT_API_JOBS                "/jobs/"                         /*!< Job API identifier. */
-#define MQTT_API_UPDATE              "/update"                        /*!< Job API identifier. */
-#define MQTT_API_STREAMS             "/streams/"                      /*!< Stream API identifier. */
-#define MQTT_API_DATA_CBOR           "/data/cbor"                     /*!< Stream API suffix. */
-#define MQTT_API_GET_CBOR            "/get/cbor"                      /*!< Stream API suffix. */
+#define MQTT_API_THINGS                       "$aws/things/"          /*!< Topic prefix for thing APIs. */
+#define MQTT_API_JOBS_NEXT_GET                "/jobs/$next/get"       /*!< Topic suffix for job API. */
+#define MQTT_API_JOBS_NOTIFY_NEXT             "/jobs/notify-next"     /*!< Topic suffix for job API. */
+#define MQTT_API_JOBS                         "/jobs/"                /*!< Job API identifier. */
+#define MQTT_API_UPDATE                       "/update"               /*!< Job API identifier. */
+#define MQTT_API_STREAMS                      "/streams/"             /*!< Stream API identifier. */
+#define MQTT_API_DATA_CBOR                    "/data/cbor"            /*!< Stream API suffix. */
+#define MQTT_API_GET_CBOR                     "/get/cbor"             /*!< Stream API suffix. */
 
 /* NOTE: The format specifiers in this string are placeholders only; the lengths of these
  * strings are used to calculate buffer sizes.
@@ -129,13 +132,13 @@ static const char asciiDigits[] =
 /* Pre-calculate max buffer size for mqtt topics and messages. We make sure the buffer size is large
  * enough to hold a dynamically constructed topic and message string.
  */
-#define TOPIC_PLUS_THINGNAME_LEN( topic )    ( CONST_STRLEN( topic ) + otaconfigMAX_THINGNAME_LEN + NULL_CHAR_LEN )              /*!< Calculate max buffer size based on topic template and thing name length. */
-#define TOPIC_GET_NEXT_BUFFER_SIZE       ( TOPIC_PLUS_THINGNAME_LEN( pOtaJobsGetNextTopicTemplate ) )                            /*!< Max buffer size for `jobs/$next/get` topic. */
-#define TOPIC_NOTIFY_NEXT_BUFFER_SIZE    ( TOPIC_PLUS_THINGNAME_LEN( pOtaJobsNotifyNextTopicTemplate ) )                         /*!< Max buffer size for `jobs/notify-next` topic. */
-#define TOPIC_JOB_STATUS_BUFFER_SIZE     ( TOPIC_PLUS_THINGNAME_LEN( pOtaJobStatusTopicTemplate ) + JOB_NAME_MAX_LEN )           /*!< Max buffer size for `jobs/<job_name>/update` topic. */
-#define TOPIC_STREAM_DATA_BUFFER_SIZE    ( TOPIC_PLUS_THINGNAME_LEN( pOtaStreamDataTopicTemplate ) + STREAM_NAME_MAX_LEN )       /*!< Max buffer size for `streams/<stream_name>/data/cbor` topic. */
-#define TOPIC_GET_STREAM_BUFFER_SIZE     ( TOPIC_PLUS_THINGNAME_LEN( pOtaGetStreamTopicTemplate ) + STREAM_NAME_MAX_LEN )        /*!< Max buffer size for `streams/<stream_name>/get/cbor` topic. */
-#define MSG_GET_NEXT_BUFFER_SIZE         ( TOPIC_PLUS_THINGNAME_LEN( pOtaGetNextJobMsgTemplate ) + U32_MAX_LEN )                 /*!< Max buffer size for message of `jobs/$next/get topic`. */
+#define TOPIC_PLUS_THINGNAME_LEN( topic )    ( CONST_STRLEN( topic ) + otaconfigMAX_THINGNAME_LEN + NULL_CHAR_LEN )                                                                     /*!< Calculate max buffer size based on topic template and thing name length. */
+#define TOPIC_GET_NEXT_BUFFER_SIZE       ( TOPIC_PLUS_THINGNAME_LEN( pOtaJobsGetNextTopicTemplate ) )                                                                                   /*!< Max buffer size for `jobs/$next/get` topic. */
+#define TOPIC_NOTIFY_NEXT_BUFFER_SIZE    ( TOPIC_PLUS_THINGNAME_LEN( pOtaJobsNotifyNextTopicTemplate ) )                                                                                /*!< Max buffer size for `jobs/notify-next` topic. */
+#define TOPIC_JOB_STATUS_BUFFER_SIZE     ( TOPIC_PLUS_THINGNAME_LEN( pOtaJobStatusTopicTemplate ) + JOB_NAME_MAX_LEN )                                                                  /*!< Max buffer size for `jobs/<job_name>/update` topic. */
+#define TOPIC_STREAM_DATA_BUFFER_SIZE    ( TOPIC_PLUS_THINGNAME_LEN( pOtaStreamDataTopicTemplate ) + STREAM_NAME_MAX_LEN )                                                              /*!< Max buffer size for `streams/<stream_name>/data/cbor` topic. */
+#define TOPIC_GET_STREAM_BUFFER_SIZE     ( TOPIC_PLUS_THINGNAME_LEN( pOtaGetStreamTopicTemplate ) + STREAM_NAME_MAX_LEN )                                                               /*!< Max buffer size for `streams/<stream_name>/get/cbor` topic. */
+#define MSG_GET_NEXT_BUFFER_SIZE         ( CONST_STRLEN( "{\"clientToken\":\"" ) + CONST_STRLEN( ":" ) + CONST_STRLEN( "\"}" ) + OTA_CLIENT_TOKEN_MAX_THINGNAME_LEN + U32_MAX_LEN + 1 ) /*!< Max buffer size for message of `jobs/$next/get topic`. */
 
 /**
  * @brief Subscribe to the jobs notification topic (i.e. New file version available).
@@ -859,13 +862,15 @@ OtaErr_t requestJob_Mqtt( const OtaAgentContext_t * pAgentCtx )
     /* The following buffer is big enough to hold a dynamically constructed
      * $next/get job message. It contains a client token that is used to track
      * how many requests have been made. */
-    char pMsg[ MSG_GET_NEXT_BUFFER_SIZE ];
+    char pMsg[ MSG_GET_NEXT_BUFFER_SIZE ] = { '\0' };
 
     static uint32_t reqCounter = 0;
     OtaErr_t otaError = OtaErrRequestJobFailed;
     OtaMqttStatus_t mqttStatus = OtaMqttSuccess;
     uint32_t msgSize = 0;
     uint16_t topicLen = 0;
+    uint32_t xThingNameLength = 0;
+    uint32_t reqCounterStringLength = 0;
 
     /* NULL-terminated list of topic string parts. */
     const char * pTopicParts[] =
@@ -876,29 +881,32 @@ OtaErr_t requestJob_Mqtt( const OtaAgentContext_t * pAgentCtx )
         NULL
     };
     char reqCounterString[ U32_MAX_LEN + 1 ];
+
     /* NULL-terminated list of payload parts */
-    /* NOTE: this must agree with pOtaGetNextJobMsgTemplate, do not add spaces, etc. */
-    const char * pPayloadParts[] =
-    {
-        "{\"clientToken\":\"",
-        NULL, /* Request counter string not available at compile time, initialized below. */
-        ":",
-        NULL, /* Thing Name not available at compile time, initialized below. */
-        "\"}",
-        NULL
-    };
 
     assert( pAgentCtx != NULL );
 
     /* Suppress warnings about unused variables. */
     ( void ) pOtaJobsGetNextTopicTemplate;
     ( void ) pOtaGetNextJobMsgTemplate;
 
-    pTopicParts[ 1 ] = ( const char * ) pAgentCtx->pThingName;
-    pPayloadParts[ 1 ] = reqCounterString;
-    pPayloadParts[ 3 ] = ( const char * ) pAgentCtx->pThingName;
+    /* Client token max length is 64. It is a combination of request counter (max 10 characters), a separator colon, and the ThingName. */
+    xThingNameLength = ( uint32_t ) strnlen( ( const char * ) pAgentCtx->pThingName, OTA_CLIENT_TOKEN_MAX_THINGNAME_LEN );
+
+    reqCounterStringLength = ( uint32_t ) stringBuilderUInt32Decimal( reqCounterString, sizeof( reqCounterString ), reqCounter );
 
-    ( void ) stringBuilderUInt32Decimal( reqCounterString, sizeof( reqCounterString ), reqCounter );
+    /* Assemble the string by copying the pieces into the buffer. This is done manually since we know the size of the thingname. */
+    strncpy( &pMsg[ msgSize ], "{\"clientToken\":\"", MSG_GET_NEXT_BUFFER_SIZE );
+    msgSize = 16U;
+    strncpy( &pMsg[ msgSize ], reqCounterString, reqCounterStringLength );
+    /* Do not count the terminating null byte on the request counter string */
+    msgSize += reqCounterStringLength - 1;
+    strncpy( &pMsg[ msgSize ], ":", MSG_GET_NEXT_BUFFER_SIZE - msgSize );
+    msgSize++;
+    strncpy( &pMsg[ msgSize ], ( const char * ) pAgentCtx->pThingName, xThingNameLength );
+    msgSize += xThingNameLength;
+    strncpy( &pMsg[ msgSize ], "\"}", MSG_GET_NEXT_BUFFER_SIZE - msgSize );
+    msgSize += 2U;
 
     /* Subscribe to the OTA job notification topic. */
     mqttStatus = subscribeToJobNotificationTopics( pAgentCtx );
@@ -907,11 +915,6 @@ OtaErr_t requestJob_Mqtt( const OtaAgentContext_t * pAgentCtx )
     {
         LogDebug( ( "MQTT job request number: counter=%u", reqCounter ) );
 
-        msgSize = ( uint32_t ) stringBuilder(
-            pMsg,
-            sizeof( pMsg ),
-            pPayloadParts );
-
         /* The buffer is static and the size is calculated to fit. */
         assert( ( msgSize > 0U ) && ( msgSize < sizeof( pMsg ) ) );
 

diff --git a/test/cbmc/proofs/OTA_Init/Makefile b/test/cbmc/proofs/OTA_Init/Makefile
@@ -13,7 +13,7 @@ PROJECT_SOURCES += $(SRCDIR)/source/ota.c
 
 NONDET_STATIC += "--nondet-static"
 
-UNWINDSET += strlen.0:66
+UNWINDSET += strlen.0:150
 
 REMOVE_FUNCTION_BODY += setControlInterface
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_ota_c_initializeAppBuffers

diff --git a/test/cbmc/proofs/requestJob_Mqtt/Makefile b/test/cbmc/proofs/requestJob_Mqtt/Makefile
@@ -7,8 +7,17 @@ HARNESS_FILE = $(HARNESS_ENTRY)
 PROOF_UID = requestJob_Mqtt
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(PROOF_STUB)/strnlen.c
 PROJECT_SOURCES += $(SRCDIR)/source/ota_mqtt.c
 
+# The strncpy bound is large due to requestJob_Mqtt copying message peices
+# into a buffer. This is much higher than the 84 characters of the buffer
+# as null characters are used after the copied in strin to fill the buffer.
+UNWINDSET += strncpy.0:220
+# The strnlen function is used when calculating the maximum thingname length 
+# which can be used to generate the client token.
+UNWINDSET += strnlen.0:54
+
 # If this proof is found to consume huge amounts of RAM, you can set the
 # EXPENSIVE variable. With new enough versions of the proof tools, this will
 # restrict the number of EXPENSIVE CBMC jobs running at once. See the

diff --git a/test/cbmc/proofs/requestJob_Mqtt/requestJob_Mqtt_harness.c b/test/cbmc/proofs/requestJob_Mqtt/requestJob_Mqtt_harness.c
@@ -60,6 +60,9 @@ size_t __CPROVER_file_local_ota_mqtt_c_stringBuilderUInt32Decimal( char * pBuffe
 {
     size_t buffersize;
 
+    /* Output can only be at most 10 characters as max unsigned 32-bit integer value is 10 characters long */
+    __CPROVER_assume( buffersize > 0 && buffersize <= 10U );
+
     /* pBuffer is always initialized before passing it to the stringBuilderUInt32Decimal
      * function and thus should not be NULL. */
     __CPROVER_assert( pBuffer != NULL,
@@ -95,12 +98,16 @@ void requestJob_Mqtt_harness()
 {
     OtaAgentContext_t agent;
     OtaInterfaces_t otaInterface;
+    size_t size;
+
+    __CPROVER_assume( size >= 1 && size < 128U );
 
     /* publish reference to the mqtt function is expected to be assigned by the user and thus
      * assumed not to be NULL. */
     otaInterface.mqtt.publish = stubMqttPublish;
 
     agent.pOtaInterface = &otaInterface;
+    agent.pThingName[ size ] = '\0';
 
     /* Ota agent is declared globally and cannot be NULL. */
     requestJob_Mqtt( &agent );

diff --git a/test/cbmc/stubs/strnlen.c b/test/cbmc/stubs/strnlen.c
@@ -0,0 +1,41 @@
+/**
+ * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ * SPDX-License-Identifier: Apache-2.0.
+ */
+
+/**
+ * FUNCTION: strnlen
+ *
+ * This function stubs the standard implementation of the strnlen function
+ * from string.h. It returns the size of the c-string *s up to a maximum of
+ * length maxlen. The length excludes the null-byte.
+ */
+
+
+#include <stdlib.h>
+
+/**
+ * Stub strnlen used by CBMC.
+ */
+size_t strnlen( const char * s,
+                size_t maxlen )
+{
+    #ifdef __CPROVER_STRING_ABSTRACTION
+        __CPROVER_precondition( __CPROVER_is_zero_string( s ), "strnlen zero-termination" );
+        return __CPROVER_zero_string_length( s );
+    #else
+        size_t len = 0;
+
+        while( s[ len ] != 0 && len < maxlen )
+        {
+            len++;
+        }
+        return len;
+    #endif
+}
+
+size_t __builtin___strnlen_chk( const char * s,
+                                size_t maxlen )
+{
+    return strnlen( s, maxlen );
+}
diff --git a/test/unit-test/ota_utest.c b/test/unit-test/ota_utest.c
@@ -117,6 +117,8 @@ const char OTA_JsonFileSignatureKey[ OTA_FILE_SIG_KEY_STR_MAX_LENGTH ] = "sig-sh
 /* OTA client name. */
 static const char * pOtaDefaultClientId = "ota_utest";
 
+/* Longest supported OTA Thingname*/
+static const char * longestThingname = "AReallyLongThingNameWhichIs128CharactersAndMatchesTheAWSIoTSpecificationForThingnameLengthMaximums12345678901234567890123456789";
 /* OTA job doc. */
 static const char * pOtaJobDoc = NULL;
 
@@ -465,6 +467,42 @@ static OtaMqttStatus_t stubMqttPublish( const char * const unused_1,
     return OtaMqttSuccess;
 }
 
+static OtaMqttStatus_t stubMqttPublishOnlySuccedsIfTruncatedValue( const char * const unused_1,
+                                                                   uint16_t unused_2,
+                                                                   const char * msg,
+                                                                   uint32_t msgSize,
+                                                                   uint8_t unused_3 )
+{
+    ( void ) unused_1;
+    ( void ) unused_2;
+    ( void ) unused_3;
+
+    /* Maximum message size is 64 characters for client token + 19 characters for JSON formatting */
+    TEST_ASSERT_LESS_OR_EQUAL( 83U, msgSize );
+    TEST_ASSERT_GREATER_THAN( 19U, msgSize );
+
+    char expected[ 54 ] = { 0 };
+    char actual[ 54 ] = { 0 };
+
+    /* Calculate the start of the thingname */
+    int offset = msgSize - 53U - 2;
+
+    memcpy( actual, msg, 16U );
+
+    TEST_ASSERT_EQUAL_STRING( "{\"clientToken\":\"", actual );
+
+    TEST_ASSERT_EQUAL_CHAR( ':', *( msg + ( offset - 1 ) ) );
+
+    /* Copy out the first 53 characters of the thingname */
+    memcpy( expected, longestThingname, 53U );
+    /* Copy out the 53 characters of the truncated thingname */
+    memcpy( actual, msg + ( offset ), 53U );
+
+    TEST_ASSERT_EQUAL_STRING( expected, actual );
+
+    return OtaMqttSuccess;
+}
+
 OtaErr_t mockControlInterfaceRequestJobAlwaysFail( const OtaAgentContext_t * unused )
 {
     ( void ) unused;
@@ -1025,10 +1063,20 @@ void test_OTA_InitWithNullName()
     TEST_ASSERT_EQUAL( OtaAgentStateStopped, OTA_GetState() );
 }
 
+void test_OTA_InitWithNameAtMaxLength()
+{
+    /* OTA does not accept name longer than 128. Explicitly test long client name. */
+    char long_name[ 129 ] = { 0 };
+
+    memset( long_name, 1, sizeof( long_name ) - 1 );
+    otaInit( long_name, mockAppCallback );
+    TEST_ASSERT_EQUAL( OtaAgentStateInit, OTA_GetState() );
+}
+
 void test_OTA_InitWithNameTooLong()
 {
-    /* OTA does not accept name longer than 64. Explicitly test long client name. */
-    char long_name[ 100 ] = { 0 };
+    /* OTA does not accept name longer than 128. Explicitly test long client name. */
+    char long_name[ 130 ] = { 0 };
 
     memset( long_name, 1, sizeof( long_name ) - 1 );
     otaInit( long_name, mockAppCallback );
@@ -2729,6 +2777,20 @@ void test_OTA_MQTT_JobSubscribingFailed()
     TEST_ASSERT_EQUAL( OtaErrRequestJobFailed, err );
 }
 
+/* Test thingname is truncated in requestJob_Mqtt */
+void test_OTA_MQTT_ThingNameTruncated()
+{
+    OtaErr_t err = OtaErrNone;
+
+    otaInit( longestThingname, mockAppCallback );
+    otaInterfaces.mqtt.subscribe = stubMqttSubscribe;
+    otaInterfaces.mqtt.publish = stubMqttPublishOnlySuccedsIfTruncatedValue;
+
+    err = requestJob_Mqtt( &otaAgent );
+
+    TEST_ASSERT_EQUAL( OtaErrNone, err );
+}
+
 /* Test that initFileTransfer_Mqtt fails if the Subscribe fails. */
 void test_OTA_MQTT_InitFileTransferSubscribeFailed()
 {