diff --git a/docs/doxygen/include/size_table.md b/docs/doxygen/include/size_table.md index 0d92ce7af..094448b07 100644 --- a/docs/doxygen/include/size_table.md +++ b/docs/doxygen/include/size_table.md @@ -9,8 +9,8 @@ ota.c -
8.7K
-
7.8K
+
8.6K
+
7.7K
ota_interface.c @@ -39,7 +39,7 @@ Total estimates -
12.9K
-
11.7K
+
12.8K
+
11.6K
diff --git a/source/ota.c b/source/ota.c index e76a6f999..6667042ca 100644 --- a/source/ota.c +++ b/source/ota.c @@ -495,6 +495,11 @@ static void callOtaCallback( OtaJobEvent_t eEvent, */ static void resetEventQueue( void ); +/** + * @brief Calculate the number of blocks required to download the file. + */ +static uint32_t fileSizeToBlocks( uint32_t fileSize ); + /* OTA state event handler functions. */ static OtaErr_t startHandler( const OtaEventData_t * pEventData ); /*!< Start timers and initiate request for job document. */ @@ -2256,6 +2261,14 @@ static OtaJobParseErr_t validateAndStartJob( OtaFileContext_t * pFileContext, LogError( ( "Parameter check failed: pFileContext->fileSize is 0: File size should be > 0." ) ); err = OtaJobParseErrZeroFileSize; } + else if( fileSizeToBlocks( pFileContext->fileSize ) > ( OTA_MAX_BLOCK_BITMAP_SIZE * BITS_PER_BYTE ) ) + { + err = OtaJobParseErrBadModelInitParams; + LogError( ( "Parameter check failed: pFileContext->fileSize (%u) greater than can be tracked.", + pFileContext->fileSize ) ); + LogWarn( ( "Largest trackable size: OTA_MAX_BLOCK_BITMAP_SIZE (%u) * BITS_PER_BYTE (%u) = %u", + OTA_MAX_BLOCK_BITMAP_SIZE, BITS_PER_BYTE, ( OTA_MAX_BLOCK_BITMAP_SIZE * BITS_PER_BYTE ) ) ); + } /* If there's an active job, verify that it's the same as what's being reported now. */ /* We already checked for missing parameters so we SHOULD have a job name in the context. */ else if( strlen( ( const char * ) otaAgent.pActiveJobName ) > 0u ) @@ -2401,12 +2414,6 @@ static DocParseErr_t parseJobDoc( const JsonDocParam_t * pJsonExpectedParams, { err = OtaJobParseErrBadModelInitParams; } - else if( pFileContext->blocksRemaining > OTA_MAX_BLOCK_BITMAP_SIZE ) - { - err = OtaJobParseErrBadModelInitParams; - LogWarn( ( "OTA size (%u blocks) greater than can be tracked. Increase `OTA_MAX_BLOCK_BITMAP_SIZE`", - ( unsigned ) pFileContext->blocksRemaining ) ); - } else { parseError = parseJSONbyModel( pJson, messageLength, &otaJobDocModel ); @@ -2485,7 +2492,7 @@ static OtaErr_t getFileContextFromJob( const char * pRawMsg, { /* Calculate how many bytes we need in our bitmap for tracking received blocks. * The below calculation requires power of 2 page sizes. */ - numBlocks = ( ( *pFileContext )->fileSize + ( OTA_FILE_BLOCK_SIZE - 1U ) ) >> otaconfigLOG2_FILE_BLOCK_SIZE; + numBlocks = fileSizeToBlocks( ( *pFileContext )->fileSize ); bitmapLen = ( numBlocks + ( BITS_PER_BYTE - 1U ) ) >> LOG2_BITS_PER_BYTE; /* This conditional statement has been excluded from the coverage report because one of branches in the @@ -3093,6 +3100,11 @@ static void callOtaCallback( OtaJobEvent_t eEvent, } } +static uint32_t fileSizeToBlocks( uint32_t fileSize ) +{ + return ( uint32_t ) ( ( fileSize + ( OTA_FILE_BLOCK_SIZE - 1U ) ) >> otaconfigLOG2_FILE_BLOCK_SIZE ); +} + void OTA_EventProcessingTask( const void * pUnused ) { ( void ) pUnused; diff --git a/test/cbmc/proofs/validateAndStartJob/validateAndStartJob_harness.c b/test/cbmc/proofs/validateAndStartJob/validateAndStartJob_harness.c index ce95e53ac..e84f33cfb 100644 --- a/test/cbmc/proofs/validateAndStartJob/validateAndStartJob_harness.c +++ b/test/cbmc/proofs/validateAndStartJob/validateAndStartJob_harness.c @@ -60,6 +60,10 @@ void validateAndStartJob_harness() * the size of new job name. */ __CPROVER_assume( activeJobNameSize > jobSize ); + /* The maximum and the minimum size of the downloaded fileSize allowed to + * avoid buffer overflow. */ + __CPROVER_assume( ( fileContext.fileSize > 0u ) && ( fileContext.fileSize < OTA_MAX_FILE_SIZE ) ); + fileContext.pJobName = jobName; /* Non-deterministically set the terminating character of the diff --git a/test/unit-test/ota_utest.c b/test/unit-test/ota_utest.c index 863a818de..f1bdd9afa 100644 --- a/test/unit-test/ota_utest.c +++ b/test/unit-test/ota_utest.c @@ -3595,8 +3595,11 @@ void test_OTA_parseJobFailsMoreBlocksThanBitmap() { OTA_JSON_JOB_ID_KEY, OTA_JOB_PARAM_REQUIRED, U16_OFFSET( OtaFileContext_t, pJobName ), U16_OFFSET( OtaFileContext_t, jobNameMaxSize ), UINT16_MAX }, }; - /* The document structure has an invalid value for ModelParamType_t. */ - otaAgent.fileContext.blocksRemaining = OTA_MAX_BLOCK_BITMAP_SIZE + 1; + /* Set the file size to be more than the maximum that can be tracked using + * bitmap. */ + otaAgent.fileContext.fileSize = ( ( OTA_MAX_BLOCK_BITMAP_SIZE * BITS_PER_BYTE ) /* Maximum number of trackable blocks. */ + * OTA_FILE_BLOCK_SIZE ) /* Size of each block. */ + + 1; /* File size bigger than the maximum trackable. */ otaInitDefault(); err = parseJobDoc( otaCustomJobDocModelParamStructure, 1, JOB_DOC_A, strlen( JOB_DOC_A ), &updateJob, &pContext );