From b310abea46850c846c9df6cac089976c23191301 Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sat, 23 Nov 2019 18:30:36 +0100 Subject: [PATCH] src/file_jpg.c: make most code frama-c friendly, file_tiff* modified to help --- src/file_jpg.c | 340 ++++++++++++++++++++++++--------------------- src/file_tiff.c | 9 +- src/file_tiff.h | 1 - src/file_tiff_be.c | 117 ++++++++++++---- src/file_tiff_le.c | 115 +++++++++++---- 5 files changed, 363 insertions(+), 219 deletions(-) diff --git a/src/file_jpg.c b/src/file_jpg.c index 3b0a895d..64abd7bf 100644 --- a/src/file_jpg.c +++ b/src/file_jpg.c @@ -288,7 +288,6 @@ static uint64_t check_mpo_le(const unsigned char *mpo, const uint64_t mpo_offset @*/ static uint64_t check_mpo(const unsigned char *mpo, const uint64_t offset, const unsigned int size) { -#ifndef MAIN_jpg if(mpo[0]=='I' && mpo[1]=='I' && mpo[2]=='*' && mpo[3]==0) { return check_mpo_le(mpo, offset, size); @@ -297,13 +296,13 @@ static uint64_t check_mpo(const unsigned char *mpo, const uint64_t offset, const { return check_mpo_be(mpo, offset, size); } -#endif return 0; } /*@ @ requires \valid(fr); @ requires \valid(fr->handle); + @ requires valid_read_string((char *)&fr->filename); @ requires \initialized(&fr->time); @*/ static void file_check_mpo(file_recovery_t *fr) @@ -401,9 +400,37 @@ static int is_marker_valid(const unsigned int marker) } } +/*@ + @ requires \valid_read(buffer + (0 .. buffer_size-1)); + @*/ +static time_t jpg_get_date(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int i, const unsigned int size) +{ /* APP1 Exif information */ + const unsigned int tiff_offset=i+2+8; + if(tiff_offset < buffer_size && size > 8) + { + /*@ assert tiff_offset < buffer_size; */ + /*@ assert size > 8; */ + unsigned int tiff_size=size-0x08; + if(buffer_size - tiff_offset < tiff_size) + { + tiff_size=buffer_size - tiff_offset; + /*@ assert tiff_offset + tiff_size == buffer_size; */ + } + else + { + /*@ assert tiff_offset + tiff_size <= buffer_size; */ + } + /*@ assert tiff_offset + tiff_size <= buffer_size; */ + return get_date_from_tiff_header(&buffer[tiff_offset], tiff_size); + } + return 0; +} + + /*@ @ requires \valid_read(buffer+(0..buffer_size-1)); @ requires \valid_read(file_recovery); + @ requires file_recovery->file_stat==\null || valid_read_string((char*)&file_recovery->filename); @ requires \valid(file_recovery_new); @ requires file_recovery_new->blocksize > 0; @ ensures \result == 0 || \result == 1; @@ -530,22 +557,14 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff } while(i+4 0x0A) - { - unsigned int tiff_size=tmp-0x0A; - if(buffer_size - (i+0x0A) < tiff_size) - tiff_size=buffer_size - (i+0x0A); -#ifndef MAIN_jpg - jpg_time=get_date_from_tiff_header(&buffer[i+0x0A], tiff_size); -#endif - } + jpg_time=jpg_get_date(buffer, buffer_size, i, size); } else if(buffer[i+1]==0xc4) { @@ -553,7 +572,7 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff if(jpg_check_dht(buffer, buffer_size, i, 2+(buffer[i+2]<<8)+buffer[i+3])!=0) return 0; } - i+=2+(buffer[i+2]<<8)+buffer[i+3]; + i+=2+size; } } if(i+1 < file_recovery_new->blocksize && buffer[i+1]!=0xda) @@ -572,8 +591,7 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff return 1; } -#ifndef MAIN_jpg -#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) +#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && !defined(__FRAMAC__) struct my_error_mgr { struct jpeg_error_mgr pub; /* "public" fields, must be the first field */ @@ -1378,7 +1396,6 @@ static void jpg_check_picture(file_recovery_t *file_recovery) } } #endif -#endif /*@ @ requires i < buffer_size; @@ -1461,6 +1478,7 @@ static int jpg_check_sof0(const unsigned char *buffer, const unsigned int buffer @ requires \valid(file_recovery->handle); @ requires file_recovery->blocksize <= 1048576; @ requires file_recovery->offset_error <= (1<<63) - 1; + @ ensures \valid(file_recovery->handle); @*/ static void jpg_search_marker(file_recovery_t *file_recovery) { @@ -1498,6 +1516,7 @@ static void jpg_search_marker(file_recovery_t *file_recovery) @ loop invariant offset + i >= offset_test; @ loop invariant offset_test >= file_recovery->offset_error; @ loop invariant 0 <= i < nbytes + file_recovery->blocksize; + @ loop assigns i,file_recovery->extra; @*/ while(i+1extra=tmp - file_recovery->offset_error; +#ifndef __FRAMAC__ if(file_recovery->extra % file_recovery->blocksize != 0) { log_info("jpg_search_marker %s extra=%llu\n", file_recovery->filename, (long long unsigned)file_recovery->extra); } +#endif return ; } i+=file_recovery->blocksize; @@ -1533,6 +1554,7 @@ static void jpg_search_marker(file_recovery_t *file_recovery) @ requires \valid(file_recovery); @ requires \valid(file_recovery->handle); @ requires \valid(thumb_offset); + @ requires valid_read_string((char *)&file_recovery->filename); @ requires file_recovery->blocksize > 0; @ requires \valid_read(buffer + (0 .. nbytes-1)); @ requires \initialized(&file_recovery->time); @@ -1541,158 +1563,158 @@ static void jpg_search_marker(file_recovery_t *file_recovery) static int jpg_check_app1(file_recovery_t *file_recovery, const unsigned int extract_thumb, const unsigned char *buffer, const unsigned int i, const unsigned int offset, const unsigned int size, const size_t nbytes, uint64_t *thumb_offset) { /* APP1 Exif information */ const unsigned int tiff_offset=i+2+8; - if(tiff_offset < nbytes && size > 8) + const unsigned char *potential_error=NULL; + const unsigned char *thumb_data=NULL; + const unsigned char *tiff; + unsigned int thumb_size=0; + unsigned int tiff_size; + if(tiff_offset >= nbytes || size <= 8) + return 1; + /*@ assert tiff_offset < nbytes; */ + /*@ assert size > 8; */ + tiff_size=size-0x08; + if(nbytes - tiff_offset < tiff_size) + { + tiff_size=nbytes - tiff_offset; + /*@ assert tiff_offset + tiff_size == nbytes; */ + } + else { - /*@ assert tiff_offset < nbytes; */ - /*@ assert size > 8; */ - const unsigned char *potential_error=NULL; - unsigned int tiff_size=size-0x08; - const unsigned char *thumb_data=NULL; - unsigned int thumb_size=0; - if(nbytes - tiff_offset < tiff_size) - { - tiff_size=nbytes - tiff_offset; - /*@ assert tiff_offset + tiff_size == nbytes; */ - } - else - { - /*@ assert tiff_offset + tiff_size <= nbytes; */ - } /*@ assert tiff_offset + tiff_size <= nbytes; */ - if(tiff_size= sizeof(TIFFHeader); */ - { - /*@ assert \valid_read(buffer + (0 .. tiff_offset+tiff_size-1)); */ - /*@ assert \valid_read((buffer + tiff_offset) + (0 .. tiff_size-1)); */ - const unsigned char *tiff=&buffer[tiff_offset]; - /*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */ - if(file_recovery->time==0) - { - /*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */ - file_recovery->time=get_date_from_tiff_header(tiff, tiff_size); - } -#ifndef __FRAMAC__ - *thumb_offset=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFOFFSET, &potential_error); - if(*thumb_offset!=0) - { - *thumb_offset+=tiff_offset; - thumb_data=buffer+ (*thumb_offset); - thumb_size=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFBYTECOUNT, &potential_error); - } + } + /*@ assert tiff_offset + tiff_size <= nbytes; */ + if(tiff_size= sizeof(TIFFHeader); */ + /*@ assert \valid_read(buffer + (0 .. tiff_offset+tiff_size-1)); */ + /*@ assert \valid_read((buffer + tiff_offset) + (0 .. tiff_size-1)); */ + tiff=&buffer[tiff_offset]; + /*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */ + if(file_recovery->time==0) + { + /*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */ + file_recovery->time=get_date_from_tiff_header(tiff, tiff_size); + } + *thumb_offset=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFOFFSET, &potential_error); + if(*thumb_offset!=0) + { + *thumb_offset+=tiff_offset; + thumb_data=buffer+ (*thumb_offset); + thumb_size=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFBYTECOUNT, &potential_error); + } + if(potential_error!=NULL) + { + file_recovery->offset_error=potential_error-buffer; + return 0; + } + if(file_recovery->offset_okoffset_ok=i; + if(thumb_data!=0 && thumb_size!=0 && *thumb_offset < nbytes - 1) + { + unsigned int j=*thumb_offset+2; + unsigned int thumb_sos_found=0; +#ifdef DEBUG_JPEG + unsigned int j_old=j; #endif - if(potential_error!=NULL) + if(buffer[*thumb_offset]!=0xff) + { + file_recovery->offset_error=*thumb_offset; + jpg_search_marker(file_recovery); + return 0; + } + if(buffer[*thumb_offset+1]!=0xd8) + { + file_recovery->offset_error=*thumb_offset+1; + return 0; + } + while(j+4offset_error=potential_error-buffer; + file_recovery->offset_error=j; +#ifdef DEBUG_JPEG + log_info("%s thumb no marker at 0x%x\n", file_recovery->filename, j); + log_error("%s Error between %u and %u\n", file_recovery->filename, j_old, j); +#endif + jpg_search_marker(file_recovery); return 0; } - if(file_recovery->offset_okoffset_ok=i; -#ifndef MAIN_jpg - if(thumb_data!=0 && thumb_size!=0) + if(buffer[j+1]==0xff) { - if(*thumb_offset < nbytes - 1) + /* See B.1.1.2 Markers in http://www.w3.org/Graphics/JPEG/itu-t81.pdf*/ + j++; + continue; + } +#ifdef DEBUG_JPEG + log_info("%s thumb marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j); +#endif + if(buffer[j+1]==0xda) /* Thumb SOS: Start Of Scan */ + thumb_sos_found=1; + else if(buffer[j+1]==0xc4) /* DHT */ + { + if(jpg_check_dht(buffer, nbytes, j, 2+(buffer[j+2]<<8)+buffer[j+3])!=0) { - unsigned int j=*thumb_offset+2; - unsigned int thumb_sos_found=0; + file_recovery->offset_error=j+2; + return 0; + } + } + else if(buffer[j+1]==0xdb || /* DQT */ + buffer[j+1]==0xc0 || /* SOF0 */ + buffer[j+1]==0xdd) /* DRI */ + { + } + else if((buffer[j+1]>=0xc0 && buffer[j+1]<=0xcf) || /* SOF0 - SOF15 */ + (buffer[j+1]>=0xe0 && buffer[j+1]<=0xef) || /* APP0 - APP15 */ + buffer[j+1]==0xfe) /* COM */ + { + /* Unusual marker, bug ? */ + } + else + { + log_info("%s thumb unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j); + file_recovery->offset_error=j; + return 0; + } + if(file_recovery->offset_okoffset_ok=j; #ifdef DEBUG_JPEG - unsigned int j_old=j; + j_old=j; #endif - if(buffer[*thumb_offset]!=0xff) + j+=2U+(buffer[j+2]<<8)+buffer[j+3]; + } + if(thumb_sos_found>0 && extract_thumb>0 + && offset < nbytes && buffer[offset]==0xff) + { + char *thumbname; + /*@ assert valid_read_string((char *)&file_recovery->filename); */ +#ifndef __FRAMAC__ + thumbname=strdup(file_recovery->filename); + if(thumbname!=NULL) + { + char *sep; + /*@ assert thumbname!=\null; */ + /*@ assert valid_read_string(thumbname); */ + sep=strrchr(thumbname,'/'); + if(sep!=NULL && *(sep+1)=='f' && *thumb_offset+thumb_size < nbytes) + { + FILE *out; + *(sep+1)='t'; + if((out=fopen(thumbname,"wb"))!=NULL) { - file_recovery->offset_error=*thumb_offset; - jpg_search_marker(file_recovery); - return 0; + if(fwrite(&buffer[*thumb_offset], thumb_size, 1, out) < 1) + { + log_error("Can't write to %s: %s\n", thumbname, strerror(errno)); + } + fclose(out); + if(file_recovery->time!=0 && file_recovery->time!=(time_t)-1) + set_date(thumbname, file_recovery->time, file_recovery->time); } - if(buffer[*thumb_offset+1]!=0xd8) + else { - file_recovery->offset_error=*thumb_offset+1; - return 0; - } - while(j+4offset_error=j; -#ifdef DEBUG_JPEG - log_info("%s thumb no marker at 0x%x\n", file_recovery->filename, j); - log_error("%s Error between %u and %u\n", file_recovery->filename, j_old, j); -#endif - jpg_search_marker(file_recovery); - return 0; - } - if(buffer[j+1]==0xff) - { - /* See B.1.1.2 Markers in http://www.w3.org/Graphics/JPEG/itu-t81.pdf*/ - j++; - continue; - } -#ifdef DEBUG_JPEG - log_info("%s thumb marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j); -#endif - if(buffer[j+1]==0xda) /* Thumb SOS: Start Of Scan */ - thumb_sos_found=1; - else if(buffer[j+1]==0xc4) /* DHT */ - { - if(jpg_check_dht(buffer, nbytes, j, 2+(buffer[j+2]<<8)+buffer[j+3])!=0) - { - file_recovery->offset_error=j+2; - return 0; - } - } - else if(buffer[j+1]==0xdb || /* DQT */ - buffer[j+1]==0xc0 || /* SOF0 */ - buffer[j+1]==0xdd) /* DRI */ - { - } - else if((buffer[j+1]>=0xc0 && buffer[j+1]<=0xcf) || /* SOF0 - SOF15 */ - (buffer[j+1]>=0xe0 && buffer[j+1]<=0xef) || /* APP0 - APP15 */ - buffer[j+1]==0xfe) /* COM */ - { - /* Unusual marker, bug ? */ - } - else - { - log_info("%s thumb unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j); - file_recovery->offset_error=j; - return 0; - } - if(file_recovery->offset_okoffset_ok=j; -#ifdef DEBUG_JPEG - j_old=j; -#endif - j+=2U+(buffer[j+2]<<8)+buffer[j+3]; - } - if(thumb_sos_found>0 && extract_thumb>0 - && offset < nbytes && buffer[offset]==0xff) - { - char *thumbname; - char *sep; - thumbname=strdup(file_recovery->filename); - sep=strrchr(thumbname,'/'); - if(sep!=NULL && *(sep+1)=='f' && *thumb_offset+thumb_size < nbytes) - { - FILE *out; - *(sep+1)='t'; - if((out=fopen(thumbname,"wb"))!=NULL) - { - if(fwrite(&buffer[*thumb_offset], thumb_size, 1, out) < 1) - { - log_error("Can't write to %s: %s\n", thumbname, strerror(errno)); - } - fclose(out); - if(file_recovery->time!=0 && file_recovery->time!=(time_t)-1) - set_date(thumbname, file_recovery->time, file_recovery->time); - } - else - { - log_error("fopen %s failed\n", thumbname); - } - } - free(thumbname); + log_error("fopen %s failed\n", thumbname); } } + free(thumbname); } #endif } @@ -1705,6 +1727,7 @@ static int jpg_check_app1(file_recovery_t *file_recovery, const unsigned int ext @ requires \valid(file_recovery->handle); @ requires file_recovery->blocksize > 0; @ requires \initialized(&file_recovery->time); + @ requires valid_read_string((char *)&file_recovery->filename); */ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsigned int extract_thumb) { @@ -1740,7 +1763,7 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign const unsigned int size=(buffer[i+2]<<8)+buffer[i+3]; if(buffer[i]!=0xff) { -#ifdef DEBUG_JPEG +#if defined(DEBUG_JPEG) && !defined(__FRAMAC__) log_info("%s no marker at 0x%x\n", file_recovery->filename, i); #endif file_recovery->offset_error=i; @@ -1753,7 +1776,7 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign offset++; continue; } -#ifdef DEBUG_JPEG +#if defined(DEBUG_JPEG) && !defined(__FRAMAC__) log_info("%s marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[i+1], i); #endif offset+=(uint64_t)2+size; @@ -1788,7 +1811,9 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign } else { +#ifndef __FRAMAC__ log_info("%s unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[i+1], i+1); +#endif file_recovery->offset_error=i+1; return thumb_offset; } @@ -1804,6 +1829,7 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign /*@ @ requires \valid(file_recovery); @ requires \valid(file_recovery->handle); + @ requires valid_read_string((char *)&file_recovery->filename); @ requires \initialized(&file_recovery->time); @*/ static void file_check_jpg(file_recovery_t *file_recovery) @@ -1828,7 +1854,7 @@ static void file_check_jpg(file_recovery_t *file_recovery) #ifdef DEBUG_JPEG log_info("jpg_check_structure error at %llu\n", (long long unsigned)file_recovery->offset_error); #endif -#ifndef MAIN_jpg +#ifndef __FRAMAC__ #if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) if(thumb_offset!=0 && (file_recovery->checkpoint_status==0 || thumb_error!=0) && @@ -1857,7 +1883,7 @@ static void file_check_jpg(file_recovery_t *file_recovery) #endif if(file_recovery->offset_error!=0) return ; -#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && ! defined(MAIN_jpg) +#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && ! defined(__FRAMAC__) jpg_check_picture(file_recovery); #else file_recovery->file_size=file_recovery->calculated_file_size; diff --git a/src/file_tiff.c b/src/file_tiff.c index 02624570..96626ce8 100644 --- a/src/file_tiff.c +++ b/src/file_tiff.c @@ -140,8 +140,11 @@ const char *tag_name(unsigned int tag) unsigned int find_tag_from_tiff_header(const unsigned char*buffer, const unsigned int buffer_size, const unsigned int tag, const unsigned char **potential_error) { const TIFFHeader *tiff=(const TIFFHeader *)buffer; - if(buffer_size < sizeof(TIFFHeader)) + /*@ assert sizeof(TIFFHeader) <= sizeof(struct ifd_header); */ + if(buffer_size < sizeof(struct ifd_header)) return 0; + /*@ assert buffer_size >= sizeof(TIFFHeader); */ + /*@ assert buffer_size >= sizeof(struct ifd_header); */ #ifndef MAIN_tiff_le if(tiff->tiff_magic==TIFF_BIGENDIAN) return find_tag_from_tiff_header_be(buffer, buffer_size, tag, potential_error); @@ -159,9 +162,11 @@ time_t get_date_from_tiff_header(const unsigned char *buffer, const unsigned int unsigned int date_asc=0; time_t tmp; /*@ assert \valid_read(buffer+(0..buffer_size-1)); */ - if(buffer_size < sizeof(TIFFHeader) || buffer_size < 19) + /*@ assert sizeof(TIFFHeader) <= sizeof(struct ifd_header); */ + if(buffer_size < sizeof(struct ifd_header) || buffer_size < 19) return (time_t)0; /*@ assert buffer_size >= sizeof(TIFFHeader); */ + /*@ assert buffer_size >= sizeof(struct ifd_header); */ /* DateTimeOriginal */ date_asc=find_tag_from_tiff_header(buffer, buffer_size, 0x9003, &potential_error); /* DateTimeDigitalized*/ diff --git a/src/file_tiff.h b/src/file_tiff.h index b030da2e..0fb5f6c8 100644 --- a/src/file_tiff.h +++ b/src/file_tiff.h @@ -69,7 +69,6 @@ struct ifd_header { } __attribute__ ((gcc_struct, __packed__)); /*@ - @ requires buffer_size >= sizeof(TIFFHeader); @ requires \valid_read(buffer+(0..buffer_size-1)); @ ensures \valid_read(buffer+(0..buffer_size-1)); @*/ diff --git a/src/file_tiff_be.c b/src/file_tiff_be.c index 21bfd5f3..92ac8707 100644 --- a/src/file_tiff_be.c +++ b/src/file_tiff_be.c @@ -126,7 +126,7 @@ unsigned int find_tag_from_tiff_header_be(const unsigned char *buffer, const uns return 0; /*@ assert \valid_read(buffer+(0..tiff_size-1)); */ /*@ assert offset_ifd0 + sizeof(struct ifd_header) <= tiff_size; */ - /*@ assert \valid_read(buffer+(0..offset_ifd0 + sizeof(struct ifd_header)-1)); */ + /*X assert \valid_read(buffer+(0..offset_ifd0 + sizeof(struct ifd_header)-1)); */ { const unsigned int tmp=find_tag_from_tiff_header_be_aux(buffer, tiff_size, tag, potential_error, offset_ifd0); /*@ assert \valid_read(buffer+(0..tiff_size-1)); */ @@ -259,6 +259,7 @@ static uint64_t tiff_be_makernote(FILE *in, const uint32_t tiff_diroff) data_read=fread(buffer, 1, sizeof(buffer), in); if(data_read<2) return TIFF_ERROR; + /*@ assert data_read >= 2; */ #if defined(__FRAMAC__) Frama_C_make_unknown((char *)buffer, sizeof(buffer)); #endif @@ -336,16 +337,55 @@ static uint64_t tiff_be_makernote(FILE *in, const uint32_t tiff_diroff) #endif #if !defined(MAIN_tiff_le) && !defined(MAIN_jpg) +static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count); + /*@ @ requires \valid(fr); @ requires \valid(fr->handle); @ requires \valid_read(&fr->extension); @ requires valid_read_string(fr->extension); @ requires \separated(&errno, fr); + @ requires \valid_read(buffer + (0 .. buffer_size - 1)); + @ ensures \valid(fr); @ ensures \valid(fr->handle); @ ensures valid_read_string(fr->extension); - @ - */ + @*/ +static uint64_t file_check_tiff_be_aux_next(file_recovery_t *fr, const unsigned int depth, const unsigned int count, const unsigned char *buffer, const unsigned int buffer_size, const unsigned int offset_ptr_offset) +{ + if(buffer_size < 4) + return 0; + /*@ assert buffer_size >= 4; */ + if(offset_ptr_offset > buffer_size-4) + return 0; + { + /*@ assert offset_ptr_offset <= buffer_size - 4; */ + /*@ assert offset_ptr_offset + 4 <= buffer_size; */ + /*@ assert \valid_read(buffer + (0 .. offset_ptr_offset + 4 - 1)); */ + const unsigned char *ptr_offset=&buffer[offset_ptr_offset]; + /*@ assert \valid_read(ptr_offset + (0 .. 4 - 1)); */ + const uint32_t *ptr32_offset=(const uint32_t *)ptr_offset; + /*@ assert \valid_read(ptr32_offset); */ + const unsigned int next_diroff=be32(*ptr32_offset); + if(next_diroff == 0) + return 0; + /*@ assert \valid(fr); */ + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ + return file_check_tiff_be_aux(fr, next_diroff, depth+1, count+1); + } +} + +/*@ + @ requires \valid(fr); + @ requires \valid(fr->handle); + @ requires \valid_read(&fr->extension); + @ requires valid_read_string(fr->extension); + @ requires \separated(&errno, fr); + @ ensures \valid(fr); + @ ensures \valid(fr->handle); + @ ensures valid_read_string(fr->extension); + @*/ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count) { unsigned char buffer[8192]; @@ -369,6 +409,9 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_ const TIFFDirEntry *entry_strip_bytecounts=NULL; const TIFFDirEntry *entry_tile_offsets=NULL; const TIFFDirEntry *entry_tile_bytecounts=NULL; + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ #ifdef DEBUG_TIFF log_info("file_check_tiff_be_aux(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count); #endif @@ -395,6 +438,7 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_ #endif if(n==0) return TIFF_ERROR; + /*@ assert 0 < n <= 65535; */ /*@ assert sizeof(TIFFDirEntry)==12; */ /*X X loop invariant 0 <= i <=n && i <= (data_read-2)/12; @@ -402,6 +446,10 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_ X*/ for(i=0; i < n && i < (unsigned int)(data_read-2)/12; i++) { + /*@ assert \valid(fr); */ + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ const TIFFDirEntry *entry=&entries[i]; /*@ assert 0 <= i < n; */ /*@ assert \valid_read(entry); */ @@ -454,28 +502,38 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_ case TIFFTAG_TILEOFFSETS: tile_offsets=tmp; break; case TIFFTAG_EXIFIFD: case TIFFTAG_KODAKIFD: -#ifndef __FRAMAC__ { - const uint64_t new_offset=file_check_tiff_be_aux(fr, tmp, depth+1, 0); + /*@ assert \valid(fr); */ /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ + const uint64_t new_offset=file_check_tiff_be_aux(fr, tmp, depth+1, 0); + /*@ assert \valid(fr); */ + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ if(new_offset==TIFF_ERROR) return TIFF_ERROR; if(max_offset < new_offset) max_offset=new_offset; } -#endif break; case TIFFTAG_SUBIFD: -#ifndef __FRAMAC__ { - const uint64_t new_offset=file_check_tiff_be_aux(fr, tmp, depth+1, 0); + /*@ assert \valid(fr); */ /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ + const uint64_t new_offset=file_check_tiff_be_aux(fr, tmp, depth+1, 0); + /*@ assert \valid(fr); */ + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ if(new_offset==TIFF_ERROR) return TIFF_ERROR; if(max_offset < new_offset) max_offset=new_offset; } -#endif break; #ifdef ENABLE_TIFF_MAKERNOTE case EXIFTAG_MAKERNOTE: @@ -515,15 +573,21 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_ #if defined(__FRAMAC__) Frama_C_make_unknown((char *)&subifd_offsetp, sizeof(subifd_offsetp)); #endif -#ifndef __FRAMAC__ - /*@ - @ loop invariant 0 <= j <= nbr <=32; - @ loop variant nbr-j; - @*/ + /*X + X loop invariant 0 <= j <= nbr <=32; + X loop variant nbr-j; + X*/ for(j=0; jhandle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ + const uint64_t new_offset=file_check_tiff_be_aux(fr, be32(subifd_offsetp[j]), depth+1, 0); + /*@ assert \valid(fr); */ + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ if(new_offset==TIFF_ERROR) { return TIFF_ERROR; @@ -531,7 +595,6 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_ if(max_offset < new_offset) max_offset = new_offset; } -#endif } break; case TIFFTAG_STRIPOFFSETS: @@ -578,22 +641,16 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_ if(max_offset < tmp) max_offset=tmp; } - if(data_read < 6) - return max_offset; - /*@ assert data_read >= 6; */ -#ifndef __FRAMAC__ - if ( 2 + n*12 + 4 <= (unsigned int)data_read) { - /*@ assert n <= (data_read - 6) /12; */ - const uint32_t *tiff_next_diroff=(const uint32_t *)&entries[n]; - if(be32(*tiff_next_diroff) > 0) - { - const uint64_t new_offset=file_check_tiff_be_aux(fr, be32(*tiff_next_diroff), depth+1, count+1); - if(new_offset != TIFF_ERROR && max_offset < new_offset) - max_offset=new_offset; - } + const unsigned int offset_ptr_offset=2+12*n; + const uint64_t new_offset=file_check_tiff_be_aux_next(fr, depth, count, buffer, data_read, offset_ptr_offset); + /*@ assert \valid(fr); */ + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ + if(new_offset != TIFF_ERROR && max_offset < new_offset) + max_offset=new_offset; } -#endif return max_offset; } diff --git a/src/file_tiff_le.c b/src/file_tiff_le.c index 5b205653..590e7bf9 100644 --- a/src/file_tiff_le.c +++ b/src/file_tiff_le.c @@ -262,6 +262,7 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff) data_read=fread(buffer, 1, sizeof(buffer), in); if(data_read<2) return TIFF_ERROR; + /*@ assert data_read >= 2; */ #if defined(__FRAMAC__) Frama_C_make_unknown((char *)buffer, sizeof(buffer)); #endif @@ -339,16 +340,55 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff) #endif #if !defined(MAIN_tiff_be) && !defined(MAIN_jpg) +static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count); + /*@ @ requires \valid(fr); @ requires \valid(fr->handle); @ requires \valid_read(&fr->extension); @ requires valid_read_string(fr->extension); @ requires \separated(&errno, fr); + @ requires \valid_read(buffer + (0 .. buffer_size - 1)); + @ ensures \valid(fr); @ ensures \valid(fr->handle); @ ensures valid_read_string(fr->extension); - @ - */ + @*/ +static uint64_t file_check_tiff_le_aux_next(file_recovery_t *fr, const unsigned int depth, const unsigned int count, const unsigned char *buffer, const unsigned int buffer_size, const unsigned int offset_ptr_offset) +{ + if(buffer_size < 4) + return 0; + /*@ assert buffer_size >= 4; */ + if(offset_ptr_offset > buffer_size-4) + return 0; + { + /*@ assert offset_ptr_offset <= buffer_size - 4; */ + /*@ assert offset_ptr_offset + 4 <= buffer_size; */ + /*@ assert \valid_read(buffer + (0 .. offset_ptr_offset + 4 - 1)); */ + const unsigned char *ptr_offset=&buffer[offset_ptr_offset]; + /*@ assert \valid_read(ptr_offset + (0 .. 4 - 1)); */ + const uint32_t *ptr32_offset=(const uint32_t *)ptr_offset; + /*@ assert \valid_read(ptr32_offset); */ + const unsigned int next_diroff=le32(*ptr32_offset); + if(next_diroff == 0) + return 0; + /*@ assert \valid(fr); */ + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ + return file_check_tiff_le_aux(fr, next_diroff, depth+1, count+1); + } +} + +/*@ + @ requires \valid(fr); + @ requires \valid(fr->handle); + @ requires \valid_read(&fr->extension); + @ requires valid_read_string(fr->extension); + @ requires \separated(&errno, fr); + @ ensures \valid(fr); + @ ensures \valid(fr->handle); + @ ensures valid_read_string(fr->extension); + @*/ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count) { unsigned char buffer[8192]; @@ -372,6 +412,9 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_ const TIFFDirEntry *entry_strip_bytecounts=NULL; const TIFFDirEntry *entry_tile_offsets=NULL; const TIFFDirEntry *entry_tile_bytecounts=NULL; + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ #ifdef DEBUG_TIFF log_info("file_check_tiff_le_aux(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count); #endif @@ -398,6 +441,7 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_ #endif if(n==0) return TIFF_ERROR; + /*@ assert 0 < n <= 65535; */ /*@ assert sizeof(TIFFDirEntry)==12; */ /*X X loop invariant 0 <= i <=n && i <= (data_read-2)/12; @@ -405,6 +449,10 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_ X*/ for(i=0; i < n && i < (unsigned int)(data_read-2)/12; i++) { + /*@ assert \valid(fr); */ + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ const TIFFDirEntry *entry=&entries[i]; /*@ assert 0 <= i < n; */ /*@ assert \valid_read(entry); */ @@ -458,16 +506,21 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_ case TIFFTAG_TILEOFFSETS: tile_offsets=tmp; break; case TIFFTAG_EXIFIFD: case TIFFTAG_KODAKIFD: -#ifndef __FRAMAC__ { - const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0); + /*@ assert \valid(fr); */ /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ + const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0); + /*@ assert \valid(fr); */ + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ if(new_offset==TIFF_ERROR) return TIFF_ERROR; if(max_offset < new_offset) max_offset=new_offset; } -#endif break; case TIFFTAG_SUBIFD: if(fr->extension == extension_arw) @@ -476,17 +529,22 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_ if(max_offset < tmp) max_offset=tmp; } -#ifndef __FRAMAC__ else { - const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0); + /*@ assert \valid(fr); */ /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ + const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0); + /*@ assert \valid(fr); */ + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ if(new_offset==TIFF_ERROR) return TIFF_ERROR; if(max_offset < new_offset) max_offset=new_offset; } -#endif break; #ifdef ENABLE_TIFF_MAKERNOTE case EXIFTAG_MAKERNOTE: @@ -526,15 +584,21 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_ #if defined(__FRAMAC__) Frama_C_make_unknown((char *)&subifd_offsetp, sizeof(subifd_offsetp)); #endif -#ifndef __FRAMAC__ - /*@ - @ loop invariant 0 <= j <= nbr <=32; - @ loop variant nbr-j; - @*/ + /*X + X loop invariant 0 <= j <= nbr <=32; + X loop variant nbr-j; + X*/ for(j=0; jhandle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ + const uint64_t new_offset=file_check_tiff_le_aux(fr, le32(subifd_offsetp[j]), depth+1, 0); + /*@ assert \valid(fr); */ + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ if(new_offset==TIFF_ERROR) { return TIFF_ERROR; @@ -542,7 +606,6 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_ if(max_offset < new_offset) max_offset = new_offset; } -#endif } break; case TIFFTAG_STRIPOFFSETS: @@ -589,22 +652,16 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_ if(max_offset < tmp) max_offset=tmp; } - if(data_read < 6) - return max_offset; - /*@ assert data_read >= 6; */ -#ifndef __FRAMAC__ - if ( 2 + n*12 + 4 <= (unsigned int)data_read) { - /*@ assert n <= (data_read - 6) /12; */ - const uint32_t *tiff_next_diroff=(const uint32_t *)&entries[n]; - if(le32(*tiff_next_diroff) > 0) - { - const uint64_t new_offset=file_check_tiff_le_aux(fr, le32(*tiff_next_diroff), depth+1, count+1); - if(new_offset != TIFF_ERROR && max_offset < new_offset) - max_offset=new_offset; - } + const unsigned int offset_ptr_offset=2+12*n; + const uint64_t new_offset=file_check_tiff_le_aux_next(fr, depth, count, buffer, data_read, offset_ptr_offset); + /*@ assert \valid(fr); */ + /*@ assert \valid(fr->handle); */ + /*@ assert \valid_read(&fr->extension); */ + /*@ assert valid_read_string(fr->extension); */ + if(new_offset != TIFF_ERROR && max_offset < new_offset) + max_offset=new_offset; } -#endif return max_offset; }