summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-09-07 09:01:55 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2019-09-07 09:01:55 +0200
commit5eb2d5a0547f3bb0b77b99eb90563aca73ba76dd (patch)
tree4a7b29794668ec14ffbcea0e028eb56f3dd893a7
parent8d1de543f42d62d84cf9e55501c7a311dbcff746 (diff)
PhotoRec: TIFF parser, fix previous commit and add various frama-c annotationsHEADmaster
-rw-r--r--src/file_tiff.c12
-rw-r--r--src/file_tiff.h60
-rw-r--r--src/file_tiff_be.c106
-rw-r--r--src/file_tiff_le.c111
4 files changed, 218 insertions, 71 deletions
diff --git a/src/file_tiff.c b/src/file_tiff.c
index 91f167a..6dc113f 100644
--- a/src/file_tiff.c
+++ b/src/file_tiff.c
@@ -50,6 +50,8 @@ const file_hint_t file_hint_tiff= {
.register_header_check=&register_header_check_tiff
};
+/* @ ensures \result == 1 || \result == 2 || \result == 4 || \result == 8;
+ */
unsigned int tiff_type2size(const unsigned int type)
{
switch(type)
@@ -134,6 +136,8 @@ const char *tag_name(unsigned int tag)
const char *find_tag_from_tiff_header(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char **potential_error)
{
+ if(tiff_size < sizeof(TIFFHeader))
+ return NULL;
if(tiff->tiff_magic==TIFF_BIGENDIAN)
return find_tag_from_tiff_header_be(tiff, tiff_size, tag, potential_error);
else if(tiff->tiff_magic==TIFF_LITTLEENDIAN)
@@ -161,8 +165,8 @@ static void register_header_check_tiff(file_stat_t *file_stat)
{
static const unsigned char tiff_header_be[4]= { 'M','M',0x00, 0x2a};
static const unsigned char tiff_header_le[4]= { 'I','I',0x2a, 0x00};
- register_header_check(0, tiff_header_be, sizeof(tiff_header_be), &header_check_tiff_be_new, file_stat);
- register_header_check(0, tiff_header_le, sizeof(tiff_header_le), &header_check_tiff_le_new, file_stat);
+ register_header_check(0, tiff_header_be, sizeof(tiff_header_be), &header_check_tiff_be, file_stat);
+ register_header_check(0, tiff_header_le, sizeof(tiff_header_le), &header_check_tiff_le, file_stat);
}
void file_check_tiff(file_recovery_t *fr)
@@ -177,9 +181,9 @@ void file_check_tiff(file_recovery_t *fr)
return;
}
if(header.tiff_magic==TIFF_LITTLEENDIAN)
- calculated_file_size=header_check_tiff_le(fr, le32(header.tiff_diroff), 0, 0);
+ calculated_file_size=file_check_tiff_le(fr, le32(header.tiff_diroff), 0, 0);
else if(header.tiff_magic==TIFF_BIGENDIAN)
- calculated_file_size=header_check_tiff_be(fr, be32(header.tiff_diroff), 0, 0);
+ calculated_file_size=file_check_tiff_be(fr, be32(header.tiff_diroff), 0, 0);
#ifdef DEBUG_TIFF
log_info("TIFF Current %llu\n", (unsigned long long)fr->file_size);
log_info("TIFF Estimated %llu %llx\n", (unsigned long long)calculated_file_size, (unsigned long long)calculated_file_size);
diff --git a/src/file_tiff.h b/src/file_tiff.h
index c68b237..5ef2325 100644
--- a/src/file_tiff.h
+++ b/src/file_tiff.h
@@ -22,7 +22,7 @@
#ifdef __cplusplus
extern "C" {
#endif
-#define TIFF_ERROR 0xffffffffffffffff
+#define TIFF_ERROR 0xffffffffffffffffull
#define TIFF_BIGENDIAN 0x4d4d
#define TIFF_LITTLEENDIAN 0x4949
@@ -67,16 +67,66 @@ struct ifd_header {
TIFFDirEntry ifd;
} __attribute__ ((gcc_struct, __packed__));
+/*@
+ @ requires tiff_size >= sizeof(TIFFHeader);
+ @ requires \valid_read((const unsigned char *)tiff+(0..tiff_size-1));
+ @*/
time_t get_date_from_tiff_header(const TIFFHeader *tiff, const unsigned int tiff_size);
+
+/*@
+ @ requires \valid_read((const unsigned char *)tiff+(0..tiff_size-1));
+ @*/
const char *find_tag_from_tiff_header(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char **potential_error);
+
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @*/
void file_check_tiff(file_recovery_t *file_recovery);
+/*@
+ @ requires tiff_size >= sizeof(TIFFHeader);
+ @ requires \valid_read((const unsigned char *)tiff+(0..tiff_size-1));
+ @ requires \valid(potential_error);
+ @*/
const char *find_tag_from_tiff_header_be(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char**potential_error);
+/*@
+ @ requires tiff_size >= sizeof(TIFFHeader);
+ @ requires \valid_read((const unsigned char *)tiff+(0..tiff_size-1));
+ @ requires \valid(potential_error);
+ @*/
const char *find_tag_from_tiff_header_le(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char**potential_error);
-uint64_t header_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count);
-uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count);
-int header_check_tiff_be_new(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);
-int header_check_tiff_le_new(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);
+
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ requires \valid_read(&fr->extension);
+ @ requires \initialized(&fr->extension);
+ @
+ */
+uint64_t file_check_tiff_be(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 \initialized(&fr->extension);
+ @
+ */
+uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count);
+
+/*@
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @
+ */
+int header_check_tiff_be(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);
+
+/*@
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @
+ */
+int header_check_tiff_le(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);
+
unsigned int tiff_type2size(const unsigned int type);
#ifdef DEBUG_TIFF
const char *tag_name(unsigned int tag);
diff --git a/src/file_tiff_be.c b/src/file_tiff_be.c
index 0cf3b7b..ffb6d4b 100644
--- a/src/file_tiff_be.c
+++ b/src/file_tiff_be.c
@@ -38,9 +38,18 @@
#include "common.h"
#include "file_tiff.h"
#include "log.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
extern const file_hint_t file_hint_jpg;
+/*@
+ @ requires \valid_read((const unsigned char*)tiff+(0..tiff_size-1));
+ @ requires \valid(potential_error);
+ @ requires \valid_read(hdr);
+ @
+ */
static const char *find_tag_from_tiff_header_be_aux(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char**potential_error, const struct ifd_header *hdr)
{
const TIFFDirEntry *tmp;
@@ -50,6 +59,7 @@ static const char *find_tag_from_tiff_header_be_aux(const TIFFHeader *tiff, cons
if((const char*)(hdr) <= (const char*)tiff ||
(const char*)(hdr+1) > (const char*)tiff+tiff_size)
return NULL;
+ /*@ assert \valid_read(hdr); */
nbr_fields=be16(hdr->nbr_fields);
for(i=0, tmp=&hdr->ifd;
i < nbr_fields && (const char*)(tmp+1) <= (const char*)tiff+tiff_size;
@@ -76,9 +86,10 @@ const char *find_tag_from_tiff_header_be(const TIFFHeader *tiff, const unsigned
return NULL;
ifd0=(const struct ifd_header *)((const char*)tiff + be32(tiff->tiff_diroff));
/* Bound checking */
- if((const char*)ifd0 <= (const char*)tiff ||
- (const char*)(ifd0+1) > (const char*)tiff + tiff_size)
+ if((const char *)ifd0 <= (const char *)tiff ||
+ (const char *)(ifd0 + 1) > (const char *)tiff + tiff_size)
return NULL;
+ /*@ assert \valid_read(ifd0); */
{
const char *tmp=find_tag_from_tiff_header_be_aux(tiff, tiff_size, tag, potential_error, ifd0);
if(tmp)
@@ -89,6 +100,7 @@ const char *find_tag_from_tiff_header_be(const TIFFHeader *tiff, const unsigned
(const char *)(exififd + 1) <= (const char *)tiff + tiff_size)
{
/* Exif */
+ /*@ assert \valid_read(exififd); */
const char *tmp=find_tag_from_tiff_header_be_aux(tiff, tiff_size, tag, potential_error, exififd);
if(tmp)
return tmp;
@@ -103,12 +115,18 @@ const char *find_tag_from_tiff_header_be(const TIFFHeader *tiff, const unsigned
if((const char *)ifd1 > (const char *)tiff &&
(const char *)(ifd1 + 1) <= (const char *)tiff + tiff_size)
{
+ /*@ assert \valid_read(ifd1); */
return find_tag_from_tiff_header_be_aux(tiff, tiff_size, tag, potential_error, ifd1);
}
}
return NULL;
}
+/*@
+ @ requires \valid(handle);
+ @ requires \valid_read(entry_strip_offsets);
+ @ requires \valid_read(entry_strip_bytecounts);
+ @*/
static uint64_t parse_strip_be(FILE *handle, const TIFFDirEntry *entry_strip_offsets, const TIFFDirEntry *entry_strip_bytecounts)
{
const unsigned int nbr=(be32(entry_strip_offsets->tdir_count)<2048?
@@ -124,6 +142,7 @@ static uint64_t parse_strip_be(FILE *handle, const TIFFDirEntry *entry_strip_off
be16(entry_strip_offsets->tdir_type)!=4 ||
be16(entry_strip_bytecounts->tdir_type)!=4)
return TIFF_ERROR;
+ /*@ assert 0 < nbr <= 2048; */
offsetp=(uint32_t *)MALLOC(nbr*sizeof(*offsetp));
if(fseek(handle, be32(entry_strip_offsets->tdir_offset), SEEK_SET) < 0 ||
fread(offsetp, sizeof(*offsetp), nbr, handle) != nbr)
@@ -150,6 +169,11 @@ static uint64_t parse_strip_be(FILE *handle, const TIFFDirEntry *entry_strip_off
return max_offset;
}
+/*@
+ @ requires type != 1 || \valid_read((const char *)val);
+ @ requires type != 3 || \valid_read((const char *)val + ( 0 .. 2));
+ @ requires type != 4 || \valid_read((const char *)val + ( 0 .. 4));
+ @*/
static unsigned int tiff_be_read(const void *val, const unsigned int type)
{
switch(type)
@@ -193,6 +217,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 2 <= data_read <= sizeof(buffer); */
if( memcmp(buffer, sign_nikon1, sizeof(sign_nikon1))==0 ||
memcmp(buffer, sign_nikon2, sizeof(sign_nikon2))==0 ||
memcmp(buffer, sign_pentax, sizeof(sign_pentax))==0 )
@@ -203,7 +228,7 @@ static uint64_t tiff_be_makernote(FILE *in, const uint32_t tiff_diroff)
log_info("tiff_be_makernote(%lu) => %u entries\n", (long unsigned)tiff_diroff, n);
#endif
//sizeof(TIFFDirEntry)=12;
- if(n > (unsigned)(data_read-2)/12)
+ if(n > (unsigned int)(data_read-2)/12)
n=(data_read-2)/12;
if(n==0)
return TIFF_ERROR;
@@ -264,12 +289,11 @@ static uint64_t tiff_be_makernote(FILE *in, const uint32_t tiff_diroff)
}
#endif
-uint64_t header_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count)
+uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count)
{
unsigned char buffer[8192];
unsigned int i,n;
int data_read;
- const uint32_t *tiff_next_diroff;
uint64_t max_offset=0;
uint64_t alphaoffset=0;
uint64_t alphabytecount=0;
@@ -283,13 +307,13 @@ uint64_t header_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, c
uint64_t tile_bytecounts=0;
unsigned int tdir_tag_old=0;
unsigned int sorted_tag_error=0;
- const TIFFDirEntry *entry=(const TIFFDirEntry *)&buffer[2];
+ const TIFFDirEntry *entries=(const TIFFDirEntry *)&buffer[2];
const TIFFDirEntry *entry_strip_offsets=NULL;
const TIFFDirEntry *entry_strip_bytecounts=NULL;
const TIFFDirEntry *entry_tile_offsets=NULL;
const TIFFDirEntry *entry_tile_bytecounts=NULL;
#ifdef DEBUG_TIFF
- log_info("header_check_tiff_be(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count);
+ log_info("file_check_tiff_be(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count);
#endif
if(depth>4)
return TIFF_ERROR;
@@ -300,19 +324,30 @@ uint64_t header_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, c
if(fseek(fr->handle, tiff_diroff, SEEK_SET) < 0)
return TIFF_ERROR;
data_read=fread(buffer, 1, sizeof(buffer), fr->handle);
+#if defined(__FRAMAC__)
+ data_read = Frama_C_interval(0, sizeof(buffer));
+ /*@ assert 0 <= data_read <= sizeof(buffer); */
+ Frama_C_make_unknown((char *)buffer, sizeof(buffer));
+#endif
if(data_read<2)
return TIFF_ERROR;
+ /*@ assert 2 <= data_read <= sizeof(buffer); */
n=(buffer[0]<<8)+buffer[1];
#ifdef DEBUG_TIFF
- log_info("header_check_tiff_be(fr, %lu, %u, %u) => %u entries\n", (long unsigned)tiff_diroff, depth, count, n);
+ log_info("file_check_tiff_be(fr, %lu, %u, %u) => %u entries\n", (long unsigned)tiff_diroff, depth, count, n);
#endif
- //sizeof(TIFFDirEntry)=12;
- if(n > (unsigned)(data_read-2)/12)
- n=(data_read-2)/12;
if(n==0)
return TIFF_ERROR;
- for(i=0;i<n;i++)
+ /*@ assert sizeof(TIFFDirEntry)==12; */
+ /*@
+ @ loop invariant 0 <= i <=n && i < (data_read-2)/12;
+ @ loop variant n-i;
+ @*/
+ for(i=0; i < n && i < (unsigned int)(data_read-2)/12; i++)
{
+ const TIFFDirEntry *entry=&entries[i];
+ /*@ assert 0 <= i < n; */
+ /*@ assert \valid_read(entry); */
const unsigned int tdir_tag=be16(entry->tdir_tag);
const uint64_t val=(uint64_t)be32(entry->tdir_count) * tiff_type2size(be16(entry->tdir_type));
#ifdef DEBUG_TIFF
@@ -329,9 +364,12 @@ uint64_t header_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, c
#endif
if(tdir_tag_old > tdir_tag)
{ /* Entries must be sorted by tag */
- sorted_tag_error++;
- if(sorted_tag_error > 1)
+ if(sorted_tag_error > 0)
+ {
return TIFF_ERROR;
+ }
+ else
+ sorted_tag_error=1;
}
if(val>4)
{
@@ -359,7 +397,7 @@ uint64_t header_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, c
case TIFFTAG_EXIFIFD:
case TIFFTAG_KODAKIFD:
{
- const uint64_t new_offset=header_check_tiff_be(fr, tmp, depth+1, 0);
+ const uint64_t new_offset=file_check_tiff_be(fr, tmp, depth+1, 0);
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
@@ -368,7 +406,7 @@ uint64_t header_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, c
break;
case TIFFTAG_SUBIFD:
{
- const uint64_t new_offset=header_check_tiff_be(fr, tmp, depth+1, 0);
+ const uint64_t new_offset=file_check_tiff_be(fr, tmp, depth+1, 0);
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
@@ -390,6 +428,7 @@ uint64_t header_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, c
}
else if(be32(entry->tdir_count) > 1)
{
+ /*@ assert le32(entry->tdir_count) > 1; */
switch(tdir_tag)
{
case TIFFTAG_EXIFIFD:
@@ -398,30 +437,34 @@ uint64_t header_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, c
if(be16(entry->tdir_type)==4)
{
const unsigned int nbr=(be32(entry->tdir_count)<32?be32(entry->tdir_count):32);
+ /*@ assert 2 <= nbr <= 32; */
+ uint32_t subifd_offsetp[32];
unsigned int j;
- uint32_t *subifd_offsetp;
if(fseek(fr->handle, be32(entry->tdir_offset), SEEK_SET) < 0)
{
return TIFF_ERROR;
}
- subifd_offsetp=(uint32_t *)MALLOC(nbr*sizeof(*subifd_offsetp));
- if(fread(subifd_offsetp, sizeof(*subifd_offsetp), nbr, fr->handle) != nbr)
+ if(fread(subifd_offsetp, sizeof(uint32_t), nbr, fr->handle) != nbr)
{
- free(subifd_offsetp);
return TIFF_ERROR;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&subifd_offsetp, sizeof(subifd_offsetp));
+#endif
+ /*@
+ @ loop invariant 0 <= j <= nbr <=32;
+ @ loop variant nbr-j;
+ @*/
for(j=0; j<nbr; j++)
{
- const uint64_t new_offset=header_check_tiff_be(fr, be32(subifd_offsetp[j]), depth+1, 0);
+ const uint64_t new_offset=file_check_tiff_be(fr, be32(subifd_offsetp[j]), depth+1, 0);
if(new_offset==TIFF_ERROR)
{
- free(subifd_offsetp);
return TIFF_ERROR;
}
if(max_offset < new_offset)
max_offset = new_offset;
}
- free(subifd_offsetp);
}
break;
case TIFFTAG_STRIPOFFSETS:
@@ -439,7 +482,6 @@ uint64_t header_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, c
}
}
tdir_tag_old=tdir_tag;
- entry++;
}
if(alphabytecount > 0 && max_offset < alphaoffset + alphabytecount)
max_offset = alphaoffset + alphabytecount;
@@ -469,17 +511,21 @@ uint64_t header_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, c
if(max_offset < tmp)
max_offset=tmp;
}
- tiff_next_diroff=(const uint32_t *)entry;
- if(be32(*tiff_next_diroff) > 0)
+ if ( 2 + n*12 + 4 <= (unsigned int)data_read)
{
- const uint64_t new_offset=header_check_tiff_be(fr, be32(*tiff_next_diroff), depth+1, count+1);
- if(new_offset != TIFF_ERROR && max_offset < new_offset)
- max_offset=new_offset;
+ /*@ 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(fr, be32(*tiff_next_diroff), depth+1, count+1);
+ if(new_offset != TIFF_ERROR && max_offset < new_offset)
+ max_offset=new_offset;
+ }
}
return max_offset;
}
-int header_check_tiff_be_new(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)
+int header_check_tiff_be(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 char *potential_error=NULL;
const TIFFHeader *header=(const TIFFHeader *)buffer;
diff --git a/src/file_tiff_le.c b/src/file_tiff_le.c
index 6da3858..fb62732 100644
--- a/src/file_tiff_le.c
+++ b/src/file_tiff_le.c
@@ -38,10 +38,19 @@
#include "common.h"
#include "file_tiff.h"
#include "log.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
extern const file_hint_t file_hint_raf;
extern const file_hint_t file_hint_jpg;
+/*@
+ @ requires \valid_read((const unsigned char*)tiff+(0..tiff_size-1));
+ @ requires \valid(potential_error);
+ @ requires \valid_read(hdr);
+ @
+ */
static const char *find_tag_from_tiff_header_le_aux(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char**potential_error, const struct ifd_header *hdr)
{
const TIFFDirEntry *tmp;
@@ -51,6 +60,7 @@ static const char *find_tag_from_tiff_header_le_aux(const TIFFHeader *tiff, cons
if((const char*)(hdr) <= (const char*)tiff ||
(const char*)(hdr+1) > (const char*)tiff+tiff_size)
return NULL;
+ /*@ assert \valid_read(hdr); */
nbr_fields=le16(hdr->nbr_fields);
for(i=0, tmp=&hdr->ifd;
i < nbr_fields && (const char*)(tmp+1) <= (const char*)tiff+tiff_size;
@@ -77,9 +87,10 @@ const char *find_tag_from_tiff_header_le(const TIFFHeader *tiff, const unsigned
return NULL;
ifd0=(const struct ifd_header *)((const char*)tiff + le32(tiff->tiff_diroff));
/* Bound checking */
- if((const char*)ifd0 <= (const char*)tiff ||
- (const char*)(ifd0+1) > (const char*)tiff + tiff_size)
+ if((const char *)ifd0 <= (const char *)tiff ||
+ (const char *)(ifd0 + 1) > (const char *)tiff + tiff_size)
return NULL;
+ /*@ assert \valid_read(ifd0); */
{
const char *tmp=find_tag_from_tiff_header_le_aux(tiff, tiff_size, tag, potential_error, ifd0);
if(tmp)
@@ -90,6 +101,7 @@ const char *find_tag_from_tiff_header_le(const TIFFHeader *tiff, const unsigned
(const char *)(exififd + 1) <= (const char *)tiff + tiff_size)
{
/* Exif */
+ /*@ assert \valid_read(exififd); */
const char *tmp=find_tag_from_tiff_header_le_aux(tiff, tiff_size, tag, potential_error, exififd);
if(tmp)
return tmp;
@@ -104,12 +116,18 @@ const char *find_tag_from_tiff_header_le(const TIFFHeader *tiff, const unsigned
if((const char *)ifd1 > (const char *)tiff &&
(const char *)(ifd1 + 1) <= (const char *)tiff + tiff_size)
{
+ /*@ assert \valid_read(ifd1); */
return find_tag_from_tiff_header_le_aux(tiff, tiff_size, tag, potential_error, ifd1);
}
}
return NULL;
}
+/*@
+ @ requires \valid(handle);
+ @ requires \valid_read(entry_strip_offsets);
+ @ requires \valid_read(entry_strip_bytecounts);
+ @*/
static uint64_t parse_strip_le(FILE *handle, const TIFFDirEntry *entry_strip_offsets, const TIFFDirEntry *entry_strip_bytecounts)
{
const unsigned int nbr=(le32(entry_strip_offsets->tdir_count)<2048?
@@ -125,6 +143,7 @@ static uint64_t parse_strip_le(FILE *handle, const TIFFDirEntry *entry_strip_off
le16(entry_strip_offsets->tdir_type)!=4 ||
le16(entry_strip_bytecounts->tdir_type)!=4)
return TIFF_ERROR;
+ /*@ assert 0 < nbr <= 2048; */
offsetp=(uint32_t *)MALLOC(nbr*sizeof(*offsetp));
if(fseek(handle, le32(entry_strip_offsets->tdir_offset), SEEK_SET) < 0 ||
fread(offsetp, sizeof(*offsetp), nbr, handle) != nbr)
@@ -151,6 +170,11 @@ static uint64_t parse_strip_le(FILE *handle, const TIFFDirEntry *entry_strip_off
return max_offset;
}
+/*@
+ @ requires type != 1 || \valid_read((const char *)val);
+ @ requires type != 3 || \valid_read((const char *)val + ( 0 .. 2));
+ @ requires type != 4 || \valid_read((const char *)val + ( 0 .. 4));
+ @*/
static unsigned int tiff_le_read(const void *val, const unsigned int type)
{
switch(type)
@@ -194,6 +218,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 2 <= data_read <= sizeof(buffer); */
if( memcmp(buffer, sign_nikon1, sizeof(sign_nikon1))==0 ||
memcmp(buffer, sign_nikon2, sizeof(sign_nikon2))==0 ||
memcmp(buffer, sign_pentax, sizeof(sign_pentax))==0 )
@@ -265,12 +290,11 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
}
#endif
-uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count)
+uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count)
{
unsigned char buffer[8192];
unsigned int i,n;
int data_read;
- const uint32_t *tiff_next_diroff;
uint64_t max_offset=0;
uint64_t alphaoffset=0;
uint64_t alphabytecount=0;
@@ -284,13 +308,13 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
uint64_t tile_bytecounts=0;
unsigned int tdir_tag_old=0;
unsigned int sorted_tag_error=0;
- const TIFFDirEntry *entry=(const TIFFDirEntry *)&buffer[2];
+ const TIFFDirEntry *entries=(const TIFFDirEntry *)&buffer[2];
const TIFFDirEntry *entry_strip_offsets=NULL;
const TIFFDirEntry *entry_strip_bytecounts=NULL;
const TIFFDirEntry *entry_tile_offsets=NULL;
const TIFFDirEntry *entry_tile_bytecounts=NULL;
#ifdef DEBUG_TIFF
- log_info("header_check_tiff_le(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count);
+ log_info("file_check_tiff_le(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count);
#endif
if(depth>4)
return TIFF_ERROR;
@@ -301,19 +325,30 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
if(fseek(fr->handle, tiff_diroff, SEEK_SET) < 0)
return TIFF_ERROR;
data_read=fread(buffer, 1, sizeof(buffer), fr->handle);
+#if defined(__FRAMAC__)
+ data_read = Frama_C_interval(0, sizeof(buffer));
+ /*@ assert 0 <= data_read <= sizeof(buffer); */
+ Frama_C_make_unknown((char *)buffer, sizeof(buffer));
+#endif
if(data_read<2)
return TIFF_ERROR;
- n=buffer[0]+(buffer[1]<<8);
+ /*@ assert 2 <= data_read <= sizeof(buffer); */
+ n=buffer[0] | (buffer[1]<<8);
#ifdef DEBUG_TIFF
- log_info("header_check_tiff_le(fr, %lu, %u, %u) => %u entries\n", (long unsigned)tiff_diroff, depth, count, n);
+ log_info("file_check_tiff_le(fr, %lu, %u, %u) => %u entries\n", (long unsigned)tiff_diroff, depth, count, n);
#endif
- //sizeof(TIFFDirEntry)=12;
- if(n > (unsigned)(data_read-2)/12)
- n=(data_read-2)/12;
if(n==0)
return TIFF_ERROR;
- for(i=0;i<n;i++)
+ /*@ assert sizeof(TIFFDirEntry)==12; */
+ /*@
+ @ loop invariant 0 <= i <=n && i < (data_read-2)/12;
+ @ loop variant n-i;
+ @*/
+ for(i=0; i < n && i < (unsigned int)(data_read-2)/12; i++)
{
+ const TIFFDirEntry *entry=&entries[i];
+ /*@ assert 0 <= i < n; */
+ /*@ assert \valid_read(entry); */
const unsigned int tdir_tag=le16(entry->tdir_tag);
const uint64_t val=(uint64_t)le32(entry->tdir_count) * tiff_type2size(le16(entry->tdir_type));
#ifdef DEBUG_TIFF
@@ -329,10 +364,14 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
(long unsigned)val);
#endif
if(tdir_tag_old > tdir_tag)
- { /* Entries must be sorted by tag, some SR2 file doesn't respected this rule */
- sorted_tag_error++;
- if(sorted_tag_error > 1 && strcmp(fr->extension,"sr2")!=0)
- return TIFF_ERROR;
+ { /* Entries must be sorted by tag, some SR2 files don't respect this rule */
+ if(sorted_tag_error > 0)
+ {
+ if(strcmp(fr->extension,"sr2")!=0)
+ return TIFF_ERROR;
+ }
+ else
+ sorted_tag_error=1;
}
if(val>4)
{
@@ -360,7 +399,7 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
case TIFFTAG_EXIFIFD:
case TIFFTAG_KODAKIFD:
{
- const uint64_t new_offset=header_check_tiff_le(fr, tmp, depth+1, 0);
+ const uint64_t new_offset=file_check_tiff_le(fr, tmp, depth+1, 0);
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
@@ -376,7 +415,7 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
}
else
{
- const uint64_t new_offset=header_check_tiff_le(fr, tmp, depth+1, 0);
+ const uint64_t new_offset=file_check_tiff_le(fr, tmp, depth+1, 0);
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
@@ -398,6 +437,7 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
}
else if(le32(entry->tdir_count) > 1)
{
+ /*@ assert le32(entry->tdir_count) > 1; */
switch(tdir_tag)
{
case TIFFTAG_EXIFIFD:
@@ -406,30 +446,34 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
if(le16(entry->tdir_type)==4)
{
const unsigned int nbr=(le32(entry->tdir_count)<32?le32(entry->tdir_count):32);
+ /*@ assert 2 <= nbr <= 32; */
+ uint32_t subifd_offsetp[32];
unsigned int j;
- uint32_t *subifd_offsetp;
if(fseek(fr->handle, le32(entry->tdir_offset), SEEK_SET) < 0)
{
return TIFF_ERROR;
}
- subifd_offsetp=(uint32_t *)MALLOC(nbr*sizeof(*subifd_offsetp));
- if(fread(subifd_offsetp, sizeof(*subifd_offsetp), nbr, fr->handle) != nbr)
+ if(fread(subifd_offsetp, sizeof(uint32_t), nbr, fr->handle) != nbr)
{
- free(subifd_offsetp);
return TIFF_ERROR;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&subifd_offsetp, sizeof(subifd_offsetp));
+#endif
+ /*@
+ @ loop invariant 0 <= j <= nbr <=32;
+ @ loop variant nbr-j;
+ @*/
for(j=0; j<nbr; j++)
{
- const uint64_t new_offset=header_check_tiff_le(fr, le32(subifd_offsetp[j]), depth+1, 0);
+ const uint64_t new_offset=file_check_tiff_le(fr, le32(subifd_offsetp[j]), depth+1, 0);
if(new_offset==TIFF_ERROR)
{
- free(subifd_offsetp);
return TIFF_ERROR;
}
if(max_offset < new_offset)
max_offset = new_offset;
}
- free(subifd_offsetp);
}
break;
case TIFFTAG_STRIPOFFSETS:
@@ -447,7 +491,6 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
}
}
tdir_tag_old=tdir_tag;
- entry++;
}
if(alphabytecount > 0 && max_offset < alphaoffset + alphabytecount)
max_offset = alphaoffset + alphabytecount;
@@ -477,17 +520,21 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
if(max_offset < tmp)
max_offset=tmp;
}
- tiff_next_diroff=(const uint32_t *)entry;
- if(le32(*tiff_next_diroff) > 0)
+ if ( 2 + n*12 + 4 <= (unsigned int)data_read)
{
- const uint64_t new_offset=header_check_tiff_le(fr, le32(*tiff_next_diroff), depth+1, count+1);
- if(new_offset != TIFF_ERROR && max_offset < new_offset)
- max_offset=new_offset;
+ /*@ 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(fr, le32(*tiff_next_diroff), depth+1, count+1);
+ if(new_offset != TIFF_ERROR && max_offset < new_offset)
+ max_offset=new_offset;
+ }
}
return max_offset;
}
-int header_check_tiff_le_new(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)
+int header_check_tiff_le(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 unsigned char raf_fp[15]={0x49, 0x49, 0x2a, 0x00, 0x08, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0xf0, 0x0d, 0x00, 0x01};
const char *potential_error=NULL;