summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2023-08-31 13:55:08 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2023-08-31 13:55:08 +0200
commit2457531d2bf936e99389da82d5aab9c66c1451bf (patch)
tree84e26c276b9715fa5b8866f602990b28f4c7579e /src
parentd2d79fe4297a64d1ee56aa322effc97203c665bc (diff)
src/file_doc.c: improve Frama-C annotationsHEADmaster
Diffstat (limited to 'src')
-rw-r--r--src/file_doc.c164
1 files changed, 111 insertions, 53 deletions
diff --git a/src/file_doc.c b/src/file_doc.c
index 8e442a3..55734ed 100644
--- a/src/file_doc.c
+++ b/src/file_doc.c
@@ -200,14 +200,83 @@ static uint32_t *OLE_load_FAT(FILE *IN, const struct OLE_HDR *header, const uint
return fat;
}
+/*@
+ @ requires num_FAT_blocks > 0;
+ @ requires 9 == uSectorShift || 12 == uSectorShift;
+ @ requires \valid_read((const char *)fat + ( 0 .. (num_FAT_blocks<<uSectorShift)-1));
+ @ requires \initialized((const char *)fat + (0 .. (num_FAT_blocks<<uSectorShift)-1));
+ @ requires num_FAT_blocks <= 109+50*((1<<uSectorShift)/4-1);
+ @ assigns \nothing;
+ @*/
+static uint64_t fat2size(const unsigned int num_FAT_blocks, const unsigned int uSectorShift, const uint32_t *fat, const uint64_t offset)
+{
+ /* Search how many entries are not used at the end of the FAT */
+ /*@ assert 9 == uSectorShift || 12 == uSectorShift; */
+ /*@ assert num_FAT_blocks <= 109+50*((1<<uSectorShift)/4-1); */
+ const unsigned int val_max=(num_FAT_blocks<<uSectorShift)/4-1;
+ unsigned int freesect_count=0;
+ unsigned int block;
+ /*@ assert \valid_read((char *)fat + ( 0 .. val_max)); */
+ /*@
+ @ loop invariant 0 <= freesect_count <= val_max;
+ @ loop assigns freesect_count;
+ @ loop variant val_max - freesect_count;
+ @*/
+ for(freesect_count=0; freesect_count < val_max; freesect_count++)
+ {
+ const unsigned j=val_max-freesect_count;
+ /*@ assert 0 <= j <= val_max; */
+ if(fat[j]!=0xFFFFFFFF)
+ break;
+ }
+ block = val_max - freesect_count + 1;
+ return offset + (((uint64_t)1+block)<<uSectorShift);
+}
+
+/*@
+ @ requires 9 == uSectorShift || 12 == uSectorShift;
+ @ requires \valid_read((const char *)dir_entries + (0 .. (1<<uSectorShift)-1));
+ @ requires \initialized((const char *)dir_entries + (0 .. (1<<uSectorShift)-1));
+ @ requires offset <= 4006;
+ @ assigns \nothing;
+ @*/
+static int doc_check_entries(const unsigned int uSectorShift, const struct OLE_DIR *dir_entries, const unsigned int miniSectorCutoff, const unsigned int fat_entries, const uint64_t doc_file_size, const uint64_t offset)
+{
+ unsigned int sid;
+ /*@
+ @ loop assigns sid;
+ @*/
+ for(sid=0;
+ sid<(1<<uSectorShift)/sizeof(struct OLE_DIR);
+ sid++)
+ {
+ const struct OLE_DIR *dir_entry=&dir_entries[sid];
+ /*@ assert \valid_read(dir_entry); */
+ if(dir_entry->type==NO_ENTRY)
+ break;
+ if(offset + le32(dir_entry->start_block) > 0 &&
+ le32(dir_entry->size) > 0 &&
+ ((le32(dir_entry->size) >= miniSectorCutoff && le32(dir_entry->start_block) > fat_entries) ||
+ le32(dir_entry->size) > doc_file_size))
+ {
+#ifdef DEBUG_OLE
+ log_info("error at sid %u\n", sid);
+#endif
+ return 1;
+ }
+ }
+ return 0;
+}
+
void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset)
{
+ /*@ assert \valid(file_recovery); */
unsigned char buffer_header[512];
uint64_t doc_file_size;
uint32_t *fat;
unsigned long int i;
- unsigned int freesect_count=0;
const struct OLE_HDR *header=(const struct OLE_HDR*)&buffer_header;
+ /*@ assert \valid_read(header); */
const uint64_t doc_file_size_org=file_recovery->file_size;
unsigned int uSectorShift;
unsigned int num_FAT_blocks;
@@ -246,37 +315,12 @@ void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset)
#endif
return ;
}
- /* Search how many entries are not used at the end of the FAT */
- {
- const unsigned int val_max=(num_FAT_blocks<<uSectorShift)/4-1;
- /*@ assert \valid_read((char *)fat + ( 0 .. val_max)); */
- /*@
- @ loop invariant 0 <= freesect_count <= val_max;
- @ loop assigns freesect_count;
- @ loop variant val_max - freesect_count;
- @*/
- for(freesect_count=0; freesect_count < val_max; freesect_count++)
- {
- const unsigned j=val_max-freesect_count;
- /*@ assert 0 <= j <= val_max; */
- if(fat[j]!=0xFFFFFFFF)
- break;
- }
- }
- /*@ assert 0 <= freesect_count <= (num_FAT_blocks<<uSectorShift)/4-1; */
- {
- const unsigned int block=(num_FAT_blocks<<uSectorShift)/4-freesect_count;
- doc_file_size=offset + (((uint64_t)1+block)<<uSectorShift);
- }
+ doc_file_size=fat2size(num_FAT_blocks, uSectorShift, fat, offset);
if(doc_file_size > doc_file_size_org)
{
#ifdef DEBUG_OLE
- log_info("doc_file_size=%llu + (1+(%u<<%u)/4-%u)<<%u\n",
- (unsigned long long)offset,
- num_FAT_blocks, uSectorShift,
- freesect_count, uSectorShift);
log_info("doc_file_size %llu > doc_file_size_org %llu\n",
- (unsigned long long)doc_file_size, (unsigned long long)doc_file_size_org);
+ (unsigned long long)doc_file_size, (unsigned long long)doc_file_size_org);
#endif
free(fat);
return ;
@@ -294,6 +338,9 @@ void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset)
#endif
/* FFFFFFFE = ENDOFCHAIN
* Use a loop count i to avoid endless loop */
+ /*@
+ @ loop invariant 9 == uSectorShift || 12 == uSectorShift;
+ @*/
for(block=le32(header->root_start_block), i=0;
block!=0xFFFFFFFE && i<fat_entries;
block=le32(fat[block]), i++)
@@ -321,29 +368,11 @@ void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset)
free(fat);
return ;
}
+ if(doc_check_entries(uSectorShift, dir_entries, le32(header->miniSectorCutoff), fat_entries, doc_file_size, offset))
{
- unsigned int sid;
- for(sid=0;
- sid<(1<<uSectorShift)/sizeof(struct OLE_DIR);
- sid++)
- {
- const struct OLE_DIR *dir_entry=&dir_entries[sid];
- if(dir_entry->type==NO_ENTRY)
- break;
- if(offset +
- le32(dir_entry->start_block) > 0 && le32(dir_entry->size) > 0 &&
- ((le32(dir_entry->size) >= le32(header->miniSectorCutoff)
- && le32(dir_entry->start_block) > fat_entries) ||
- le32(dir_entry->size) > doc_file_size))
- {
-#ifdef DEBUG_OLE
- log_info("error at sid %u\n", sid);
-#endif
- free(dir_entries);
- free(fat);
- return ;
- }
- }
+ free(dir_entries);
+ free(fat);
+ return ;
}
free(dir_entries);
}
@@ -509,6 +538,7 @@ static const char *ole_get_file_extension(const struct OLE_HDR *header, const un
unsigned int block;
unsigned int i;
const unsigned int uSectorShift=le16(header->uSectorShift);
+ /*@ assert 9 == uSectorShift || 12 == uSectorShift; */
unsigned int fat_size;
if(buffer_size<512)
return NULL;
@@ -550,6 +580,7 @@ static const char *ole_get_file_extension(const struct OLE_HDR *header, const un
sid++)
{
const struct OLE_DIR *dir_entry=&dir_entries[sid];
+ /*@ assert \valid_read(dir_entry); */
if(dir_entry->type==NO_ENTRY)
break;
#ifdef DEBUG_OLE
@@ -654,6 +685,7 @@ static void *OLE_read_stream(FILE *IN,
char *dataPt;
unsigned int block;
unsigned int i;
+ /*@ assert 9 == uSectorShift || 12 == uSectorShift; */
const unsigned int i_max=((len+(1<<uSectorShift)-1) >> uSectorShift);
#ifdef DISABLED_FOR_FRAMAC
dataPt=(char *)MALLOC(((1024*1024+(1<<uSectorShift)-1) >> uSectorShift) << uSectorShift);
@@ -695,7 +727,7 @@ static void *OLE_read_stream(FILE *IN,
@ requires \valid_read(header);
@ requires \valid_read(fat);
@ requires 9 == le16(header->uSectorShift) || 12 == le16(header->uSectorShift);
- @ requires 0 < le32(header->csectMiniFat) <= 2048;
+ @ requires le32(header->csectMiniFat) <= 2048;
@ ensures \result!=\null ==> \valid((char *)\result + (0 .. (le32(header->csectMiniFat) << le16(header->uSectorShift)) - 1));
@ ensures \result!=\null ==> \initialized((char *)\result + (0 .. (le32(header->csectMiniFat) << le16(header->uSectorShift)) - 1));
@*/
@@ -705,8 +737,9 @@ static uint32_t *OLE_load_MiniFAT(FILE *IN, const struct OLE_HDR *header, const
unsigned int block;
unsigned int i;
const unsigned int uSectorShift=le16(header->uSectorShift);
- /*@ assert uSectorShift==9 || uSectorShift==12; */
const unsigned int csectMiniFat=le32(header->csectMiniFat);
+ /*@ assert uSectorShift==9 || uSectorShift==12; */
+ /*@ assert csectMiniFat <= 2048; */
const unsigned int minifat_length=csectMiniFat << uSectorShift;
if(csectMiniFat==0)
return NULL;
@@ -756,6 +789,7 @@ static uint32_t get32u(const void *buffer, const unsigned int offset)
/*@ assert \valid_read(ptr + (0 .. 4-1)); */
/*@ assert \initialized(ptr + (0 .. 4-1)); */
const uint32_t *val=(const uint32_t *)ptr;
+ /*@ assert \valid_read(val); */
return le32(*val);
}
@@ -770,6 +804,7 @@ static uint64_t get64u(const void *buffer, const unsigned int offset)
const char *ptr=(const char *)buffer + offset;
/*@ assert \valid_read(ptr + (0 .. 7)); */
const uint64_t *val=(const uint64_t *)ptr;
+ /*@ assert \valid_read(val); */
return le64(*val);
}
@@ -901,6 +936,7 @@ struct summary_entry
/*@
@ requires 8 <= size <= 1024*1024;
+ @ requires offset <= 1024*1024;
@ requires \valid_read(buffer+ (0 .. size-1));
@ requires \initialized(buffer+ (0 .. size-1));
@ requires \valid(ext);
@@ -966,6 +1002,7 @@ static void OLE_parse_software_entry(const char *buffer, const unsigned int size
/*@
@ requires 8 <= size <= 1024*1024;
+ @ requires offset <= size;
@ requires \valid_read(buffer+ (0 .. size-1));
@ requires \initialized(buffer+ (0 .. size-1));
@ requires \valid(ext);
@@ -1025,6 +1062,7 @@ static void OLE_parse_uni_software_entry(const char *buffer, const unsigned int
/*@
@ requires 8 <= size <= 1024*1024;
+ @ requires offset <= size;
@ requires \valid_read(buffer+ (0 .. size-1));
@ requires \valid(title + (0 .. 1024-1));
@ requires valid_string(title);
@@ -1090,6 +1128,7 @@ static void OLE_parse_title_entry(const char *buffer, const unsigned int size, c
/*@
@ requires 8 <= size <= 1024*1024;
+ @ requires offset <= size;
@ requires \valid_read(buffer+ (0 .. size-1));
@ requires \initialized(buffer+ (0 .. size-1));
@ requires \valid(file_time);
@@ -1308,6 +1347,7 @@ static void OLE_parse_summary_aux(const char *dataPt, const unsigned int dirLen,
#ifdef DEBUG_OLE
dump_log(dataPt, dirLen);
#endif
+ /*@ assert \valid_read(udataPt + (0 .. dirLen-1)); */
if(udataPt[0]!=0xfe || udataPt[1]!=0xff)
return ;
pos=get32u(dataPt, 44);
@@ -1367,6 +1407,7 @@ static void *OLE_read_ministream(const unsigned char *ministream,
unsigned char *dataPt;
unsigned int mblock=miniblock_start;
unsigned int size_read;
+ /*@ assert uMiniSectorShift==6; */
#ifdef DISABLED_FOR_FRAMAC
const unsigned int len_aligned=(1024*1024+(1<<uMiniSectorShift)-1) / (1<<uMiniSectorShift) * (1<<uMiniSectorShift);
#else
@@ -1374,6 +1415,8 @@ static void *OLE_read_ministream(const unsigned char *ministream,
#endif
dataPt=(unsigned char *)MALLOC(len_aligned);
/*@
+ @ loop invariant uMiniSectorShift==6;
+ @ loop invariant 48 <= len <= 1024*1024;
@ loop invariant 0 <= size_read < len + (1<<uMiniSectorShift);
@ loop invariant size_read > 0 ==> \initialized(dataPt + size_read - (1<<uMiniSectorShift) + (0 .. (1<<uMiniSectorShift)- 1));
@ loop invariant size_read > 0 ==> \initialized(dataPt + (0 .. size_read - 1));
@@ -1392,8 +1435,10 @@ static void *OLE_read_ministream(const unsigned char *ministream,
free(dataPt);
return NULL;
}
+ /*@ assert mblock < ministream_size>>uMiniSectorShift; */
memcpy(&dataPt[size_read], &ministream[mblock<<uMiniSectorShift], (1<<uMiniSectorShift));
/*@ assert \initialized(dataPt + size_read + (0 .. (1<<uMiniSectorShift)-1)); */
+ /*@ assert \valid_read(minifat + mblock); */
mblock=le32(minifat[mblock]);
}
/*@ assert \initialized(dataPt + (0 .. len - 1)); */
@@ -1421,6 +1466,7 @@ static void OLE_parse_summary(FILE *file, const uint32_t *fat, const unsigned in
const uint64_t offset)
{
const unsigned int uSectorShift=le16(header->uSectorShift);
+ /*@ assert 9 == uSectorShift || 12 == uSectorShift; */
char *summary=NULL;
/*@ assert *ext == \null || valid_read_string(*ext); */
/*@ assert valid_string(title); */
@@ -1446,6 +1492,7 @@ static void OLE_parse_summary(FILE *file, const uint32_t *fat, const unsigned in
return ;
}
/*@ assert 0 < le32(header->csectMiniFat) <= 2048; */
+ /*@ assert 9 == uSectorShift || 12 == uSectorShift; */
{
const unsigned int mini_fat_entries=(le32(header->csectMiniFat) << uSectorShift) / 4;
uint32_t *minifat;
@@ -1503,6 +1550,7 @@ static void file_rename_doc(file_recovery_t *file_recovery)
unsigned char buffer_header[512];
uint32_t *fat;
const struct OLE_HDR *header=(const struct OLE_HDR*)&buffer_header;
+ /*@ assert \valid_read(header); */
time_t file_time=0;
unsigned int fat_entries;
unsigned int uSectorShift;
@@ -1559,6 +1607,8 @@ static void file_rename_doc(file_recovery_t *file_recovery)
fclose(file);
return ;
}
+ /*@ assert num_FAT_blocks <= 109 + 50 *((1<<uSectorShift)/4-1); */
+ /*@ assert 9 == uSectorShift || 12 == uSectorShift; */
fat_entries=(num_FAT_blocks==0 ? 109 : (num_FAT_blocks<<uSectorShift)/4);
{
unsigned int ministream_block=0;
@@ -1570,6 +1620,10 @@ static void file_rename_doc(file_recovery_t *file_recovery)
#ifdef DEBUG_OLE
log_info("file_rename_doc root_start_block=%u, fat_entries=%u\n", le32(header->root_start_block), fat_entries);
#endif
+ /*@
+ @ loop invariant \valid_read(header);
+ @ loop invariant valid_string(&title[0]);
+ */
for(block=le32(header->root_start_block), i=0;
block<fat_entries && block!=0xFFFFFFFE && i<fat_entries;
block=le32(fat[block]), i++)
@@ -1598,16 +1652,20 @@ static void file_rename_doc(file_recovery_t *file_recovery)
if(i==0)
{
const struct OLE_DIR *dir_entry=dir_entries;
+ /*@ assert \valid_read(dir_entry); */
ministream_block=le32(dir_entry->start_block);
ministream_size=le32(dir_entry->size);
}
- /*@ assert valid_string(&title[0]); */
+ /*@
+ @ loop invariant valid_string(&title[0]);
+ @*/
for(sid=0;
sid<(1<<uSectorShift)/sizeof(struct OLE_DIR);
sid++)
{
/*@ assert valid_string(&title[0]); */
const struct OLE_DIR *dir_entry=&dir_entries[sid];
+ /*@ assert \valid_read(dir_entry); */
if(dir_entry->type!=NO_ENTRY)
{
const char SummaryInformation[40]=