summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-11-16 16:22:04 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2019-11-16 16:22:04 +0100
commite474cb0c6e01f195176d69a82ea2c97f021142b1 (patch)
tree945324ebc8dc414782fcbc6e73dfceae8733f74a
parent90efd3e667ab7be0f04e0749903571305756bd0c (diff)
New prototype for get_date_from_tiff_header()
-rw-r--r--Makefile.am4
-rw-r--r--src/file_jpg.c5
-rw-r--r--src/file_orf.c2
-rw-r--r--src/file_rw2.c2
-rw-r--r--src/file_tiff.c19
-rw-r--r--src/file_tiff.h12
-rw-r--r--src/file_tiff_be.c3
-rw-r--r--src/file_tiff_le.c42
-rw-r--r--src/file_wdp.c2
-rw-r--r--src/filegen.c2
-rw-r--r--src/filegen.h7
11 files changed, 69 insertions, 31 deletions
diff --git a/Makefile.am b/Makefile.am
index 0ccabc1..7b424bf 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -88,13 +88,13 @@ session_id3.framac: src/file_mp3.c src/common.c src/filegen.c src/log.c
gcc -W -Wall -DMAIN_id3 -DHAVE_CONFIG_H -O -o demo -I. $^
frama-c $^ -cpp-extra-args="-DMAIN_id3 -DHAVE_CONFIG_H -D__x86_64__" $(FRAMA_C_FLAGS) -save $@
-session_jpg.framac: src/file_jpg.c src/common.c src/filegen.c src/log.c src/suspend_no.c src/setdate.c
+session_jpg.framac: src/file_jpg.c src/file_tiff.c src/file_tiff_be.c src/file_tiff_le.c src/common.c src/filegen.c src/log.c src/suspend_no.c src/setdate.c
gcc -W -Wall -DMAIN_jpg -DHAVE_CONFIG_H -O -o demo -I. $^ -ljpeg
frama-c $^ -cpp-extra-args="-DMAIN_jpg -DHAVE_CONFIG_H -D__x86_64__ -I/usr/include -I $(frama-c -print-path)/libc" $(FRAMA_C_FLAGS) -save $@
session_tiff_be.framac: src/file_tiff.c src/file_tiff_be.c src/file_tiff_le.c src/common.c src/filegen.c src/log.c
gcc -W -Wall -DMAIN_tiff_le -DHAVE_CONFIG_H -O -o demo -I. $^
- frama-c $^ -cpp-extra-args="-DMAIN_tiff_le -DHAVE_CONFIG_H -D__x86_64__" $(FRAMA_C_FLAGS) -save $@
+ frama-c $^ -cpp-extra-args="-DMAIN_tiff_be -DHAVE_CONFIG_H -D__x86_64__" $(FRAMA_C_FLAGS) -save $@
session_tiff_le.framac: src/file_tiff.c src/file_tiff_be.c src/file_tiff_le.c src/common.c src/filegen.c src/log.c
gcc -W -Wall -DMAIN_tiff_le -DHAVE_CONFIG_H -O -o demo -I. $^
diff --git a/src/file_jpg.c b/src/file_jpg.c
index bf82acd..e7dd47f 100644
--- a/src/file_jpg.c
+++ b/src/file_jpg.c
@@ -493,7 +493,7 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
unsigned int tiff_size=2+(buffer[i+2]<<8)+buffer[i+3]-0x0A;
if(buffer_size - (i+0x0A) < tiff_size)
tiff_size=buffer_size - (i+0x0A);
- jpg_time=get_date_from_tiff_header((const TIFFHeader*)&buffer[i+0x0A], tiff_size);
+ jpg_time=get_date_from_tiff_header(&buffer[i+0x0A], tiff_size);
}
}
else if(buffer[i+1]==0xc4)
@@ -1494,13 +1494,14 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign
{
const char *potential_error=NULL;
const TIFFHeader *tiff=(const TIFFHeader*)&buffer[i+0x0A];
+ const unsigned char *tiff_buffer=&buffer[i+0x0A];
unsigned int tiff_size=2+size-0x0A;
const char *thumb_data=NULL;
const char *ifbytecount=NULL;
if(nbytes - (i+0x0A) < tiff_size)
tiff_size=nbytes - (i+0x0A);
if(file_recovery->time==0)
- file_recovery->time=get_date_from_tiff_header(tiff, tiff_size);
+ file_recovery->time=get_date_from_tiff_header(tiff_buffer, tiff_size);
thumb_data=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFOFFSET, &potential_error);
if(thumb_data!=NULL)
{
diff --git a/src/file_orf.c b/src/file_orf.c
index 71895e8..15531a5 100644
--- a/src/file_orf.c
+++ b/src/file_orf.c
@@ -53,7 +53,7 @@ static int header_check_orf_IIRO(const unsigned char *buffer, const unsigned int
{
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_orf.extension;
- file_recovery_new->time=get_date_from_tiff_header((const TIFFHeader *)buffer, buffer_size);
+ file_recovery_new->time=get_date_from_tiff_header(buffer, buffer_size);
file_recovery_new->file_check=&file_check_tiff_le;
return 1;
}
diff --git a/src/file_rw2.c b/src/file_rw2.c
index 4e2cd4f..639a036 100644
--- a/src/file_rw2.c
+++ b/src/file_rw2.c
@@ -52,7 +52,7 @@ static int header_check_rw2(const unsigned char *buffer, const unsigned int buff
/* Panasonic/Leica */
reset_file_recovery(file_recovery_new);
file_recovery_new->extension="rw2";
- file_recovery_new->time=get_date_from_tiff_header(header, buffer_size);
+ file_recovery_new->time=get_date_from_tiff_header(buffer, buffer_size);
file_recovery_new->file_check=&file_check_tiff_le;
return 1;
}
diff --git a/src/file_tiff.c b/src/file_tiff.c
index 7599856..33c7786 100644
--- a/src/file_tiff.c
+++ b/src/file_tiff.c
@@ -152,18 +152,21 @@ const char *find_tag_from_tiff_header(const TIFFHeader *tiff, const unsigned int
return NULL;
}
-time_t get_date_from_tiff_header(const TIFFHeader *tiff, const unsigned int tiff_size)
+time_t get_date_from_tiff_header(const unsigned char *buffer, const unsigned int buffer_size)
{
const char *potential_error=NULL;
- const char *date_asc;
+ const unsigned char *date_asc;
+ if(buffer_size < sizeof(TIFFHeader) || buffer_size < 19)
+ return (time_t)0;
+ /*@ assert buffer_size >= sizeof(TIFFHeader); */
/* DateTimeOriginal */
- date_asc=find_tag_from_tiff_header(tiff, tiff_size, 0x9003, &potential_error);
+ date_asc=(const unsigned char *)find_tag_from_tiff_header((const TIFFHeader *)buffer, buffer_size, 0x9003, &potential_error);
/* DateTimeDigitalized*/
- if(date_asc==NULL || date_asc < (const char *)tiff || &date_asc[18] >= (const char *)tiff + tiff_size)
- date_asc=find_tag_from_tiff_header(tiff, tiff_size, 0x9004, &potential_error);
- if(date_asc==NULL || date_asc < (const char *)tiff || &date_asc[18] >= (const char *)tiff + tiff_size)
- date_asc=find_tag_from_tiff_header(tiff, tiff_size, 0x132, &potential_error);
- if(date_asc==NULL || date_asc < (const char *)tiff || &date_asc[18] >= (const char *)tiff + tiff_size)
+ if(date_asc==NULL || date_asc < buffer || &date_asc[18] >= buffer + buffer_size)
+ date_asc=(const unsigned char *)find_tag_from_tiff_header((const TIFFHeader *)buffer, buffer_size, 0x9004, &potential_error);
+ if(date_asc==NULL || date_asc < buffer || &date_asc[18] >= buffer + buffer_size)
+ date_asc=(const unsigned char *)find_tag_from_tiff_header((const TIFFHeader *)buffer, buffer_size, 0x132, &potential_error);
+ if(date_asc==NULL || date_asc < buffer || &date_asc[18] >= buffer + buffer_size)
return (time_t)0;
return get_time_from_YYYY_MM_DD_HH_MM_SS(date_asc);
}
diff --git a/src/file_tiff.h b/src/file_tiff.h
index aaac994..1882b6a 100644
--- a/src/file_tiff.h
+++ b/src/file_tiff.h
@@ -70,12 +70,13 @@ struct ifd_header {
/*@
@ requires tiff_size >= sizeof(TIFFHeader);
- @ requires \valid_read((const unsigned char *)tiff+(0..tiff_size-1));
+ @ requires \valid_read(buffer+(0..buffer_size-1));
@*/
-time_t get_date_from_tiff_header(const TIFFHeader *tiff, const unsigned int tiff_size);
+time_t get_date_from_tiff_header(const unsigned char*buffer, const unsigned int buffer_size);
/*@
@ requires \valid_read((const unsigned char *)tiff+(0..tiff_size-1));
+ @ requires \separated(potential_error, tiff);
@*/
const char *find_tag_from_tiff_header(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char **potential_error);
@@ -84,6 +85,7 @@ const char *find_tag_from_tiff_header(const TIFFHeader *tiff, const unsigned int
@ requires tiff_size >= sizeof(TIFFHeader);
@ requires \valid_read((const unsigned char *)tiff+(0..tiff_size-1));
@ requires \valid(potential_error);
+ @ requires \separated(potential_error, tiff);
@*/
const char *find_tag_from_tiff_header_le(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char**potential_error);
@@ -92,6 +94,8 @@ const char *find_tag_from_tiff_header_le(const TIFFHeader *tiff, const unsigned
@ requires \valid(fr->handle);
@ requires \valid_read(&fr->extension);
@ requires valid_read_string(fr->extension);
+ @ ensures \valid(fr->handle);
+ @ ensures valid_read_string(fr->extension);
@*/
void file_check_tiff_le(file_recovery_t *fr);
@@ -114,9 +118,12 @@ int header_check_tiff_le(const unsigned char *buffer, const unsigned int buffer_
@ requires tiff_size >= sizeof(TIFFHeader);
@ requires \valid_read((const unsigned char *)tiff+(0..tiff_size-1));
@ requires \valid(potential_error);
+ @ requires \separated(potential_error, tiff);
@*/
const char *find_tag_from_tiff_header_be(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char**potential_error);
+#endif
+#if !defined(MAIN_tiff_le) && !defined(MAIN_jpg)
/*@
@ requires buffer_size >= 15;
@ requires \valid_read(buffer+(0..buffer_size-1));
@@ -124,7 +131,6 @@ const char *find_tag_from_tiff_header_be(const TIFFHeader *tiff, const unsigned
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ ensures \result == 0 || \result == 1;
- @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_tiff_be);
@ ensures (\result == 1) ==> (file_recovery_new->extension != \null);
@ ensures (\result == 1) ==> valid_read_string(file_recovery_new->extension);
@*/
diff --git a/src/file_tiff_be.c b/src/file_tiff_be.c
index fb4eebc..ef21ad4 100644
--- a/src/file_tiff_be.c
+++ b/src/file_tiff_be.c
@@ -611,6 +611,7 @@ static void file_check_tiff_be(file_recovery_t *fr)
#endif
/*@
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_tiff_be);
@ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_tiff.extension ||
file_recovery_new->extension == extension_dcr ||
file_recovery_new->extension == extension_dng ||
@@ -653,7 +654,7 @@ int header_check_tiff_be(const unsigned char *buffer, const unsigned int buffer_
file_recovery_new->extension=extension_dcr;
}
}
- file_recovery_new->time=get_date_from_tiff_header(header, buffer_size);
+ file_recovery_new->time=get_date_from_tiff_header(buffer, buffer_size);
file_recovery_new->file_check=&file_check_tiff_be;
return 1;
}
diff --git a/src/file_tiff_le.c b/src/file_tiff_le.c
index 899e342..81d7aaf 100644
--- a/src/file_tiff_le.c
+++ b/src/file_tiff_le.c
@@ -42,8 +42,10 @@
#include "__fc_builtin.h"
#endif
-#if !defined(MAIN_tiff_be) && !defined(MAIN_tiff_le)
+#if !defined(MAIN_tiff_be) && !defined(MAIN_tiff_le) && !defined(MAIN_jpg)
extern const file_hint_t file_hint_raf;
+#endif
+#if (!defined(MAIN_tiff_be) && !defined(MAIN_tiff_le)) || defined(MAIN_jpg)
extern const file_hint_t file_hint_jpg;
#endif
extern const file_hint_t file_hint_tiff;
@@ -59,6 +61,7 @@ static const char *extension_sr2="sr2";
@ requires \valid_read((const unsigned char*)tiff+(0..tiff_size-1));
@ requires \valid(potential_error);
@ requires \valid_read(hdr);
+ @ requires \separated(potential_error, \union(tiff, 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)
@@ -72,10 +75,14 @@ static const char *find_tag_from_tiff_header_le_aux(const TIFFHeader *tiff, cons
return NULL;
/*@ assert \valid_read(hdr); */
nbr_fields=le16(hdr->nbr_fields);
+ /*@
+ @ loop assigns i, *potential_error, tmp;
+ @*/
for(i=0, tmp=&hdr->ifd;
i < nbr_fields && (const char*)(tmp+1) <= (const char*)tiff+tiff_size;
i++, tmp++)
{
+ /*@ assert \valid_read(tmp); */
if(le16(tmp->tdir_type) > 18 && (*potential_error==NULL || *potential_error > (const char*)&tmp->tdir_type+1))
{
*potential_error = (const char*)&tmp->tdir_type+1;
@@ -91,11 +98,18 @@ const char *find_tag_from_tiff_header_le(const TIFFHeader *tiff, const unsigned
const struct ifd_header *ifd0;
const struct ifd_header *exififd;
const uint32_t *tiff_next_diroff;
+ unsigned int tiff_diroff;
if(tiff_size < sizeof(TIFFHeader))
return NULL;
- if(tiff_size < le32(tiff->tiff_diroff)+sizeof(TIFFDirEntry))
+ /*@ assert tiff_size >= sizeof(TIFFHeader); */
+ /*@ assert \valid_read(tiff); */
+ tiff_diroff=le32(tiff->tiff_diroff);
+ if(tiff_diroff >= tiff_size)
+ return NULL;
+ /*@ assert tiff_diroff < tiff_size; */
+ if(tiff_size < tiff_diroff+sizeof(struct ifd_header))
return NULL;
- ifd0=(const struct ifd_header *)((const char*)tiff + le32(tiff->tiff_diroff));
+ ifd0=(const struct ifd_header *)((const char*)tiff + tiff_diroff);
/* Bound checking */
if((const char *)ifd0 <= (const char *)tiff ||
(const char *)(ifd0 + 1) > (const char *)tiff + tiff_size)
@@ -143,13 +157,16 @@ static uint64_t parse_strip_le(FILE *handle, const TIFFDirEntry *entry_strip_off
const unsigned int nbr=(le32(entry_strip_offsets->tdir_count)<2048?
le32(entry_strip_offsets->tdir_count):
2048);
+ /*@ assert nbr <= 2048; */
unsigned int i;
uint32_t *offsetp;
uint32_t *sizep;
uint64_t max_offset=0;
- if(le32(entry_strip_offsets->tdir_count) != le32(entry_strip_bytecounts->tdir_count))
+ /* le32() isn't required to compare the 2 values */
+ if(entry_strip_offsets->tdir_count != entry_strip_bytecounts->tdir_count)
return TIFF_ERROR;
- if(le32(entry_strip_offsets->tdir_count)==0 ||
+ /*@ assert entry_strip_offsets->tdir_count == entry_strip_bytecounts->tdir_count; */
+ if(nbr==0 ||
le16(entry_strip_offsets->tdir_type)!=4 ||
le16(entry_strip_bytecounts->tdir_type)!=4)
return TIFF_ERROR;
@@ -321,6 +338,9 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
@ requires \valid(fr->handle);
@ requires \valid_read(&fr->extension);
@ requires valid_read_string(fr->extension);
+ @ requires \separated(&errno, 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)
@@ -435,6 +455,7 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
#ifndef __FRAMAC__
{
const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0);
+ /*@ assert \valid(fr->handle); */
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
@@ -453,6 +474,7 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
else
{
const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0);
+ /*@ assert \valid(fr->handle); */
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
@@ -560,6 +582,9 @@ 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)
{
@@ -592,6 +617,7 @@ void file_check_tiff_le(file_recovery_t *fr)
#endif
if(header.tiff_magic==TIFF_LITTLEENDIAN)
calculated_file_size=file_check_tiff_le_aux(fr, le32(header.tiff_diroff), 0, 0);
+ /*@ assert \valid(fr->handle); */
#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);
@@ -632,7 +658,7 @@ int header_check_tiff_le(const unsigned char *buffer, const unsigned int buffer_
return 0;
/* Avoid a false positiv with some RAF files */
if(file_recovery->file_stat!=NULL &&
-#if !defined(MAIN_tiff_be) && !defined(MAIN_tiff_le)
+#if !defined(MAIN_tiff_be) && !defined(MAIN_tiff_le) && !defined(MAIN_jpg)
file_recovery->file_stat->file_hint==&file_hint_raf &&
#endif
memcmp(buffer, raf_fp, 15)==0)
@@ -640,7 +666,7 @@ int header_check_tiff_le(const unsigned char *buffer, const unsigned int buffer_
header_ignored(file_recovery_new);
return 0;
}
-#if !defined(MAIN_tiff_be) && !defined(MAIN_tiff_le)
+#if !defined(MAIN_tiff_be) && !defined(MAIN_tiff_le) && !defined(MAIN_jpg)
if(file_recovery->file_stat!=NULL &&
file_recovery->file_stat->file_hint==&file_hint_jpg)
{
@@ -675,7 +701,7 @@ int header_check_tiff_le(const unsigned char *buffer, const unsigned int buffer_
file_recovery_new->extension=extension_nef;
}
}
- file_recovery_new->time=get_date_from_tiff_header(header, buffer_size);
+ file_recovery_new->time=get_date_from_tiff_header(buffer, buffer_size);
file_recovery_new->file_check=&file_check_tiff_le;
return 1;
}
diff --git a/src/file_wdp.c b/src/file_wdp.c
index f70dd56..0be5694 100644
--- a/src/file_wdp.c
+++ b/src/file_wdp.c
@@ -51,7 +51,7 @@ static int header_check_wdp(const unsigned char *buffer, const unsigned int buff
return 0;
reset_file_recovery(file_recovery_new);
file_recovery_new->extension="wdp";
- file_recovery_new->time=get_date_from_tiff_header((const TIFFHeader *)buffer, buffer_size);
+ file_recovery_new->time=get_date_from_tiff_header(buffer, buffer_size);
file_recovery_new->file_check=&file_check_tiff_le;
return 1;
}
diff --git a/src/filegen.c b/src/filegen.c
index dc12987..c197b5e 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -863,7 +863,7 @@ time_t get_time_from_YYMMDDHHMMSS(const char *date_asc)
return mktime(&tm_time);
}
-time_t get_time_from_YYYY_MM_DD_HH_MM_SS(const char *date_asc)
+time_t get_time_from_YYYY_MM_DD_HH_MM_SS(const unsigned char *date_asc)
{
struct tm tm_time;
if(memcmp(date_asc, "0000", 4)==0)
diff --git a/src/filegen.h b/src/filegen.h
index 70cbee4..31aabfa 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -249,9 +249,9 @@ void header_ignored_cond_reset(uint64_t start, uint64_t end);
void header_ignored(const file_recovery_t *file_recovery_new);
/*@
+ @ requires separation: \separated(file_recovery, file_recovery_new, &errno);
@ requires \valid_read(file_recovery);
@ requires \valid_read(file_recovery_new);
- @ requires separation: \separated(file_recovery, file_recovery_new);
@ requires \initialized(&file_recovery->file_check);
@ requires \initialized(&file_recovery->handle);
@ ensures \result == 0 || \result == 1;
@@ -261,8 +261,9 @@ int header_ignored_adv(const file_recovery_t *file_recovery, const file_recovery
/*@
requires valid_stream: \valid(stream);
requires whence_enum: whence == SEEK_SET || whence == SEEK_CUR || whence == SEEK_END;
+ requires \separated(&errno, stream);
assigns *stream \from *stream, indirect:offset, indirect:whence;
- assigns \result, __fc_errno \from indirect:*stream, indirect:offset,
+ assigns \result, errno \from indirect:*stream, indirect:offset,
indirect:whence;
*/
int my_fseek(FILE *stream, off_t offset, int whence);
@@ -275,7 +276,7 @@ time_t get_time_from_YYMMDDHHMMSS(const char *date_asc);
/*@
@ requires \valid_read(date_asc + (0 .. 18));
@*/
-time_t get_time_from_YYYY_MM_DD_HH_MM_SS(const char *date_asc);
+time_t get_time_from_YYYY_MM_DD_HH_MM_SS(const unsigned char *date_asc);
/*@
@ requires \valid_read(date_asc + (0 .. 16));