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 );