From f3f54129f851adbf83aed777e0cfd308bd109fa0 Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sat, 27 Feb 2021 10:44:20 +0100 Subject: [PATCH] src/file_pdf.c: fix problems reported by Frama-C --- src/file_pdf.c | 126 +++++++++++++++++++++++++++++++++++++------------ 1 file changed, 96 insertions(+), 30 deletions(-) diff --git a/src/file_pdf.c b/src/file_pdf.c index 1124546e..527b0f29 100644 --- a/src/file_pdf.c +++ b/src/file_pdf.c @@ -57,7 +57,16 @@ const file_hint_t file_hint_pdf= { /*@ @ assigns \nothing; @*/ -static int hex(int c) +static int is_hexa(const int c) +{ + return ((c>='0' && c<='9') || (c>='A' && c<='F') || (c>='a' && c<='f')); +} + +/*@ + @ assigns \nothing; + @ ensures 0 <= \result <= 15; + @*/ +static unsigned int hex(const int c) { if(c>='0' && c<='9') return c-'0'; @@ -65,7 +74,7 @@ static int hex(int c) return c-'A'+10; if(c>='a' && c<='f') return c-'a'+10; - return -1; + return 0; } /*@ @@ -78,10 +87,11 @@ static void file_rename_pdf(file_recovery_t *file_recovery) char title[512]; const unsigned char pattern[6]={ '/', 'T', 'i', 't', 'l', 'e' }; off_t offset; + uint64_t tmp; FILE *handle; unsigned char*buffer; unsigned int i; - unsigned int j; + unsigned int l; size_t bsize; const unsigned char utf16[3]= { 0xfe, 0xff, 0x00}; if((handle=fopen(file_recovery->filename, "rb"))==NULL) @@ -101,55 +111,79 @@ static void file_rename_pdf(file_recovery_t *file_recovery) fclose(handle); return; } - offset=file_rsearch(handle, offset, pattern, sizeof(pattern)); - if(offset==0) + tmp=file_rsearch(handle, offset, pattern, sizeof(pattern)); + if(tmp==0 || tmp > PHOTOREC_MAX_FILE_SIZE) { fclose(handle); return; } - offset+=sizeof(pattern); + offset=tmp+sizeof(pattern); if(my_fseek(handle, offset, SEEK_SET)<0) { fclose(handle); return ; } buffer=(unsigned char*)MALLOC(512); - if((bsize=fread(buffer, 1, 512, handle)) <= 0) + if((bsize=fread(buffer, 1, 512, handle)) <= 2) { free(buffer); fclose(handle); return ; } + /*@ assert 2 < bsize; */ #if defined(__FRAMAC__) Frama_C_make_unknown(buffer, 512); #endif + /*@ assert \initialized(buffer + (0 .. 512-1)); */ fclose(handle); /* Skip spaces after /Title */ + /*@ + @ loop invariant 0 <= i <= bsize; + @ loop assigns i; + @ */ for(i=0; i= bsize) { /* Too much spaces */ free(buffer); return ; } + /*@ assert i + 2 < bsize; */ if(buffer[i]=='<') { - unsigned int s=i; + unsigned int j; + unsigned int s; /* hexa to ascii */ - j=s; - buffer[j++]='('; - for(s++; s+14 && - (memcmp(&title[j-4], ".doc", 4)==0 || - memcmp(&title[j-4], ".xls", 4)==0)) - j-=4; - else if(j>5 && - (memcmp(&title[j-5], ".docx", 5)==0 || - memcmp(&title[j-5], ".xlsx", 5)==0)) - j-=5; - file_rename(file_recovery, title, j, 0, NULL, 1); + if(l>4 && + (memcmp(&title[l-4], ".doc", 4)==0 || + memcmp(&title[l-4], ".xls", 4)==0)) + l-=4; + else if(l>5 && + (memcmp(&title[l-5], ".docx", 5)==0 || + memcmp(&title[l-5], ".xlsx", 5)==0)) + l-=5; + file_rename(file_recovery, title, l, 0, NULL, 1); free(buffer); } /*@ @ requires \valid(file_recovery); + @ requires valid_file_recovery(file_recovery); + @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source); @*/ static void file_date_pdf(file_recovery_t *file_recovery) { @@ -225,6 +275,11 @@ static void file_date_pdf(file_recovery_t *file_recovery) free(buffer); return ; } + /*@ + @ loop invariant \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, buffer + (..)); + @ loop assigns i, j, *file_recovery->handle, file_recovery->time, buffer[0..21]; + @ loop assigns errno; + @*/ for(i=0; ihandle, offset+i+1, SEEK_SET)>=0 && fread(buffer, 1, 22, file_recovery->handle) == 22) { + /*@ assert \initialized( buffer+ (0 .. 22-1)); */ if(buffer[0]=='=' && (buffer[1]=='\'' || buffer[1]=='"')) { file_recovery->time=get_time_from_YYYY_MM_DD_HH_MM_SS(&buffer[2]); @@ -260,6 +316,9 @@ static void file_date_pdf(file_recovery_t *file_recovery) /*@ @ requires \valid(file_recovery); + @ requires \valid(file_recovery->handle); + @ requires valid_file_recovery(file_recovery); + @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source); @*/ static void file_check_pdf_and_size(file_recovery_t *file_recovery) { @@ -297,6 +356,9 @@ static void file_check_pdf_and_size(file_recovery_t *file_recovery) /*@ @ requires \valid(file_recovery); + @ requires \valid(file_recovery->handle); + @ requires valid_file_recovery(file_recovery); + @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source); @*/ static void file_check_pdf(file_recovery_t *file_recovery) { @@ -336,16 +398,18 @@ static uint64_t read_pdf_file_aux(const unsigned char *buffer, unsigned int i) /*@ @ requires \valid_read(buffer+(0..512-1)); + @ assigns \nothing; @*/ static uint64_t read_pdf_file(const unsigned char *buffer) { const unsigned char sig_linearized[10]={'L','i','n','e','a','r','i','z','e','d'}; - const unsigned char *src; + const char *src; unsigned int i; - src=(const unsigned char *)td_memmem(buffer, 512, sig_linearized, sizeof(sig_linearized)); + const char *sbuffer=(const char *)buffer; + src=(const char *)td_memmem(sbuffer, 512, sig_linearized, sizeof(sig_linearized)); if(src == NULL) return 0; - i = src - buffer; + i = src - sbuffer; i+=sizeof(sig_linearized); if( i >= 512 -1) return 0; @@ -370,6 +434,8 @@ static uint64_t read_pdf_file(const unsigned char *buffer) @ requires \valid(file_recovery_new); @ requires file_recovery_new->blocksize > 0; @ requires separation: \separated(&file_hint_pdf, buffer, file_recovery, file_recovery_new); + @ ensures \result!=0 ==> valid_file_recovery(file_recovery_new); + @ assigns *file_recovery_new; @*/ static int header_check_pdf(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) {