summaryrefslogtreecommitdiffstats
path: root/src/file_tiff_le.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/file_tiff_le.c')
-rw-r--r--src/file_tiff_le.c190
1 files changed, 121 insertions, 69 deletions
diff --git a/src/file_tiff_le.c b/src/file_tiff_le.c
index 2a4aa92..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,34 +87,47 @@ 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)
return tmp;
}
exififd=(const struct ifd_header *)find_tag_from_tiff_header_le_aux(tiff, tiff_size, TIFFTAG_EXIFIFD, potential_error, ifd0);
- if(exififd!=NULL)
+ if((const char *)exififd > (const char *)tiff &&
+ (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;
}
tiff_next_diroff=(const uint32_t *)(&ifd0->ifd + le16(ifd0->nbr_fields));
- if( (const char *)tiff_next_diroff >= (const char *)tiff &&
- (const char *)(tiff_next_diroff + 1) < (const char*)tiff + tiff_size &&
+ if( (const char *)tiff_next_diroff > (const char *)tiff &&
+ (const char *)(tiff_next_diroff + 1) <= (const char*)tiff + tiff_size &&
le32(*tiff_next_diroff)>0)
{
/* IFD1 */
const struct ifd_header *ifd1=(const struct ifd_header*)((const char *)tiff+le32(*tiff_next_diroff));
- return find_tag_from_tiff_header_le_aux(tiff, tiff_size, tag, potential_error, ifd1);
+ 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?
@@ -115,17 +138,18 @@ static uint64_t parse_strip_le(FILE *handle, const TIFFDirEntry *entry_strip_off
uint32_t *sizep;
uint64_t max_offset=0;
if(le32(entry_strip_offsets->tdir_count) != le32(entry_strip_bytecounts->tdir_count))
- return -1;
+ return TIFF_ERROR;
if(le32(entry_strip_offsets->tdir_count)==0 ||
le16(entry_strip_offsets->tdir_type)!=4 ||
le16(entry_strip_bytecounts->tdir_type)!=4)
- return -1;
+ 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)
{
free(offsetp);
- return -1;
+ return TIFF_ERROR;
}
sizep=(uint32_t *)MALLOC(nbr*sizeof(*sizep));
if(fseek(handle, le32(entry_strip_bytecounts->tdir_offset), SEEK_SET) < 0 ||
@@ -133,7 +157,7 @@ static uint64_t parse_strip_le(FILE *handle, const TIFFDirEntry *entry_strip_off
{
free(offsetp);
free(sizep);
- return -1;
+ return TIFF_ERROR;
}
for(i=0; i<nbr; i++)
{
@@ -146,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)
@@ -183,12 +212,13 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
uint64_t tile_bytecounts=0;
const TIFFDirEntry *entry;
if(tiff_diroff < sizeof(TIFFHeader))
- return -1;
+ return TIFF_ERROR;
if(fseek(in, tiff_diroff, SEEK_SET) < 0)
- return -1;
+ return TIFF_ERROR;
data_read=fread(buffer, 1, sizeof(buffer), in);
if(data_read<2)
- return -1;
+ 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 )
@@ -199,10 +229,10 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
log_info("tiff_le_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 -1;
+ return TIFF_ERROR;
for(i=0;i<n;i++)
{
const uint64_t val=(uint64_t)le32(entry->tdir_count) * tiff_type2size(le16(entry->tdir_type));
@@ -221,7 +251,7 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
{
const uint64_t new_offset=le32(entry->tdir_offset)+val;
if(new_offset==0)
- return -1;
+ return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
@@ -260,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;
@@ -279,36 +308,47 @@ 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 -1;
+ return TIFF_ERROR;
if(count>16)
- return -1;
+ return TIFF_ERROR;
if(tiff_diroff < sizeof(TIFFHeader))
- return -1;
+ return TIFF_ERROR;
if(fseek(fr->handle, tiff_diroff, SEEK_SET) < 0)
- return -1;
+ 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 -1;
- n=buffer[0]+(buffer[1]<<8);
+ return TIFF_ERROR;
+ /*@ 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 -1;
- for(i=0;i<n;i++)
+ return TIFF_ERROR;
+ /*@ 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
@@ -324,16 +364,20 @@ 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 -1;
+ { /* 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)
{
const uint64_t new_offset=le32(entry->tdir_offset)+val;
if(new_offset==0)
- return -1;
+ return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
@@ -355,9 +399,9 @@ 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);
- if(new_offset==-1)
- return -1;
+ 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)
max_offset=new_offset;
}
@@ -371,9 +415,9 @@ 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);
- if(new_offset==-1)
- return -1;
+ 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)
max_offset=new_offset;
}
@@ -382,8 +426,8 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
case EXIFTAG_MAKERNOTE:
{
const uint64_t new_offset=tiff_le_makernote(fr->handle, tmp);
- if(new_offset==-1)
- return -1;
+ if(new_offset==TIFF_ERROR)
+ return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
@@ -393,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:
@@ -401,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 -1;
+ 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 -1;
+ 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);
- if(new_offset==-1)
+ 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 -1;
+ return TIFF_ERROR;
}
if(max_offset < new_offset)
max_offset = new_offset;
}
- free(subifd_offsetp);
}
break;
case TIFFTAG_STRIPOFFSETS:
@@ -442,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;
@@ -459,32 +507,36 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
if(entry_strip_offsets != NULL && entry_strip_bytecounts != NULL)
{
const uint64_t tmp=parse_strip_le(fr->handle, entry_strip_offsets, entry_strip_bytecounts);
- if(tmp==-1)
- return -1;
+ if(tmp==TIFF_ERROR)
+ return TIFF_ERROR;
if(max_offset < tmp)
max_offset=tmp;
}
if(entry_tile_offsets != NULL && entry_tile_bytecounts != NULL)
{
const uint64_t tmp=parse_strip_le(fr->handle, entry_tile_offsets, entry_tile_bytecounts);
- if(tmp==-1)
- return -1;
+ if(tmp==TIFF_ERROR)
+ return TIFF_ERROR;
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 != -1 && 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 char raf_fp[15]={0x49, 0x49, 0x2a, 0x00, 0x08, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0xf0, 0x0d, 0x00, 0x01};
+ 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;
const TIFFHeader *header=(const TIFFHeader *)buffer;
if((uint32_t)le32(header->tiff_diroff) < sizeof(TIFFHeader))
@@ -526,7 +578,7 @@ int header_check_tiff_le_new(const unsigned char *buffer, const unsigned int buf
file_recovery_new->extension="sr2";
else if(strncmp(tag_make, "SONY ",5)==0)
file_recovery_new->extension="arw";
- else if(memcmp(tag_make, "NIKON CORPORATION", 18)==0)
+ else if(tag_make < (const char *)buffer + buffer_size - 18 && memcmp(tag_make, "NIKON CORPORATION", 18)==0)
file_recovery_new->extension="nef";
}
}