From 6d4908eb2fd858e108ca002c4f070cdeb866c122 Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sat, 20 Mar 2021 09:07:51 +0100 Subject: [PATCH] src/file_wim.c: rewrite header_check_wim(), add Frama-C annotations --- src/file_wim.c | 140 ++++++++++++++++++++++++++++++++----------------- 1 file changed, 93 insertions(+), 47 deletions(-) diff --git a/src/file_wim.c b/src/file_wim.c index be2c702f..a18d6546 100644 --- a/src/file_wim.c +++ b/src/file_wim.c @@ -33,76 +33,122 @@ #include "common.h" #include "log.h" +/*@ requires \valid(file_stat); */ static void register_header_check_wim(file_stat_t *file_stat); /* http://go.microsoft.com/fwlink/?LinkId=92227 */ -const file_hint_t file_hint_wim= { - .extension="wim", - .description="Windows imaging (WIM) image", - .max_filesize=PHOTOREC_MAX_FILE_SIZE, - .recover=1, - .enable_by_default=1, - .register_header_check=®ister_header_check_wim +const file_hint_t file_hint_wim = { + .extension = "wim", + .description = "Windows imaging (WIM) image", + .max_filesize = PHOTOREC_MAX_FILE_SIZE, + .recover = 1, + .enable_by_default = 1, + .register_header_check = ®ister_header_check_wim }; struct reshdr_disk_short { - union { - uint64_t flags; /* one byte is a combination of RESHDR_FLAG_XXX */ - uint64_t size; /* the 7 low-bytes are used to store the size */ + union + { + uint64_t flags; /* one byte is a combination of RESHDR_FLAG_XXX */ + uint64_t size; /* the 7 low-bytes are used to store the size */ }; uint64_t offset; uint64_t original_size; -} __attribute__ ((gcc_struct, __packed__)); +} __attribute__((gcc_struct, __packed__)); #define RESHDR_GET_SIZE(R) (le64(R.size) & 0x00FFFFFFFFFFFFFF) struct _WIMHEADER_V1_PACKED { - char ImageTag[8]; - uint32_t cbSize; - uint32_t dwVersion; - uint32_t dwFlags; - uint32_t dwCompressionSize; - unsigned char gWIMGuid[16]; - uint16_t usPartNumber; - uint16_t usTotalParts; - uint32_t dwImageCount; - struct reshdr_disk_short rhOffsetTable; - struct reshdr_disk_short rhXmlData; - struct reshdr_disk_short rhBootMetadata; - uint32_t dwBootIndex; - struct reshdr_disk_short rhIntegrity; - unsigned char bUnused[60]; -} __attribute__ ((gcc_struct, __packed__)); + char ImageTag[8]; + uint32_t cbSize; + uint32_t dwVersion; + uint32_t dwFlags; + uint32_t dwCompressionSize; + unsigned char gWIMGuid[16]; + uint16_t usPartNumber; + uint16_t usTotalParts; + uint32_t dwImageCount; + struct reshdr_disk_short rhOffsetTable; + struct reshdr_disk_short rhXmlData; + struct reshdr_disk_short rhBootMetadata; + uint32_t dwBootIndex; + struct reshdr_disk_short rhIntegrity; + unsigned char bUnused[60]; +} __attribute__((gcc_struct, __packed__)); +/*@ + @ requires size <= 0x00FFFFFFFFFFFFFF; + @ assigns \nothing; + @*/ +static uint64_t wim_max(const uint64_t offset, const uint64_t size, const uint64_t max_size) +{ + uint64_t tmp; + if(size == 0) + return max_size; + if(offset > PHOTOREC_MAX_FILE_SIZE) + return 0; + tmp = offset + size; + if(tmp > max_size) + return tmp; + return max_size; +} + +/*@ + @ requires buffer_size > sizeof(struct _WIMHEADER_V1_PACKED); + @ requires \valid_read(buffer+(0..buffer_size-1)); + @ requires valid_file_recovery(file_recovery); + @ requires \valid(file_recovery_new); + @ requires file_recovery_new->blocksize > 0; + @ requires separation: \separated(&file_hint_wim, buffer+(..), file_recovery, file_recovery_new); + @ ensures \result!=0 ==> valid_file_recovery(file_recovery_new); + @ assigns *file_recovery_new; + @*/ static int header_check_wim(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new) { - const struct _WIMHEADER_V1_PACKED *hdr=(const struct _WIMHEADER_V1_PACKED *)buffer; - uint64_t size=le32(hdr->cbSize); - if(le32(hdr->cbSize) < sizeof(struct _WIMHEADER_V1_PACKED)) + const struct _WIMHEADER_V1_PACKED *hdr = (const struct _WIMHEADER_V1_PACKED *)buffer; + uint64_t size = le32(hdr->cbSize); + const uint64_t rhOffsetTable_s = RESHDR_GET_SIZE(hdr->rhOffsetTable); + /*@ assert rhOffsetTable_s <= 0x00FFFFFFFFFFFFFF; */ + const uint64_t rhOffsetTable_o = le64(hdr->rhOffsetTable.offset); + const uint64_t rhXmlData_s = RESHDR_GET_SIZE(hdr->rhXmlData); + /*@ assert rhXmlData_s <= 0x00FFFFFFFFFFFFFF; */ + const uint64_t rhXmlData_o = le64(hdr->rhXmlData.offset); + const uint64_t rhBootMetadata_s = RESHDR_GET_SIZE(hdr->rhBootMetadata); + /*@ assert rhBootMetadata_s <= 0x00FFFFFFFFFFFFFF; */ + const uint64_t rhBootMetadata_o = le64(hdr->rhBootMetadata.offset); + const uint64_t rhIntegrity_s = RESHDR_GET_SIZE(hdr->rhIntegrity); + /*@ assert rhIntegrity_s <= 0x00FFFFFFFFFFFFFF; */ + const uint64_t rhIntegrity_o = le64(hdr->rhIntegrity.offset); + + if(size < sizeof(struct _WIMHEADER_V1_PACKED)) return 0; #ifdef DEBUG_WIM - log_info("cbSize %llu\n", (unsigned long long)le32(hdr->cbSize)); + log_info("cbSize %llu\n", (unsigned long long)size); log_info("dwCompressionSize %llu\n", (unsigned long long)le32(hdr->dwCompressionSize)); - log_info("rhOffsetTable %llu %llu\n", (unsigned long long)RESHDR_GET_SIZE(hdr->rhOffsetTable), (unsigned long long)le64(hdr->rhOffsetTable.offset)); - log_info("rhXmlData %llu %llu\n", (unsigned long long)RESHDR_GET_SIZE(hdr->rhXmlData), (unsigned long long)le64(hdr->rhXmlData.offset)); - log_info("rhBootMetadata %llu %llu\n", (unsigned long long)RESHDR_GET_SIZE(hdr->rhBootMetadata), (unsigned long long)le64(hdr->rhBootMetadata.offset)); - log_info("rhIntegrity %llu %llu\n", (unsigned long long)RESHDR_GET_SIZE(hdr->rhIntegrity), (unsigned long long)le64(hdr->rhIntegrity.offset)); + log_info("rhOffsetTable %llu %llu\n", (unsigned long long)rhOffsetTable_s, (unsigned long long)rhOffsetTable_o); + log_info("rhXmlData %llu %llu\n", (unsigned long long)rhXmlData_s, (unsigned long long)rhXmlData_o); + log_info("rhBootMetadata %llu %llu\n", (unsigned long long)rhBootMetadata_s, (unsigned long long)rhBootMetadata_o); + log_info("rhIntegrity %llu %llu\n", (unsigned long long)rhIntegrity_s, (unsigned long long)rhIntegrity_o); #endif - if(RESHDR_GET_SIZE(hdr->rhOffsetTable) > 0 && RESHDR_GET_SIZE(hdr->rhOffsetTable) + le64(hdr->rhOffsetTable.offset) > size) - size=RESHDR_GET_SIZE(hdr->rhOffsetTable) + le64(hdr->rhOffsetTable.offset); - if(RESHDR_GET_SIZE(hdr->rhXmlData) > 0 && RESHDR_GET_SIZE(hdr->rhXmlData) + le64(hdr->rhXmlData.offset) > size) - size=RESHDR_GET_SIZE(hdr->rhXmlData) + le64(hdr->rhXmlData.offset); - if(RESHDR_GET_SIZE(hdr->rhBootMetadata) > 0 && RESHDR_GET_SIZE(hdr->rhBootMetadata) + le64(hdr->rhBootMetadata.offset) > size) - size=RESHDR_GET_SIZE(hdr->rhBootMetadata) + le64(hdr->rhBootMetadata.offset); - if(RESHDR_GET_SIZE(hdr->rhIntegrity) > 0 && RESHDR_GET_SIZE(hdr->rhIntegrity) + le64(hdr->rhIntegrity.offset) > size) - size=RESHDR_GET_SIZE(hdr->rhIntegrity) + le64(hdr->rhIntegrity.offset); + size = wim_max(rhOffsetTable_o, rhOffsetTable_s, size); + if(size == 0) + return 0; + size = wim_max(rhXmlData_o, rhXmlData_s, size); + if(size == 0) + return 0; + size = wim_max(rhBootMetadata_o, rhBootMetadata_s, size); + if(size == 0) + return 0; + size = wim_max(rhIntegrity_o, rhIntegrity_s, size); + if(size == 0) + return 0; reset_file_recovery(file_recovery_new); - file_recovery_new->extension=file_hint_wim.extension; - file_recovery_new->calculated_file_size=size; - file_recovery_new->data_check=&data_check_size; - file_recovery_new->file_check=&file_check_size; + file_recovery_new->extension = file_hint_wim.extension; + file_recovery_new->calculated_file_size = size; + file_recovery_new->data_check = &data_check_size; + file_recovery_new->file_check = &file_check_size; return 1; }