summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-01-18 10:18:17 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2020-01-18 10:18:17 +0100
commit9b51c2aeb03fe414b7946043ad39e7ab0b1d0cf9 (patch)
tree3f301f91ee168a27f3024b274dd98f53b9af8f67
parent611da961b33b7d1d0b68a8d7f87437417055dab5 (diff)
PhotoRec - file_tiff*.c: Reintroduce fixed IFD1 parsing.
Buggy version was removed by commit 7e8f99aa92038220efa4d9c45cf8a0857a77d7d8
-rw-r--r--src/file_tiff.h24
-rw-r--r--src/file_tiff_be.c42
-rw-r--r--src/file_tiff_le.c41
3 files changed, 104 insertions, 3 deletions
diff --git a/src/file_tiff.h b/src/file_tiff.h
index 51059f5..fa9af03 100644
--- a/src/file_tiff.h
+++ b/src/file_tiff.h
@@ -77,7 +77,7 @@ time_t get_date_from_tiff_header(const unsigned char*buffer, const unsigned int
/*@
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \separated(potential_error, buffer);
- @ ensures \valid_read(buffer+(0..buffer_size-1));
+ @ assigns *potential_error;
@*/
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);
@@ -88,7 +88,7 @@ unsigned int find_tag_from_tiff_header(const unsigned char *buffer, const unsign
@ requires \valid_read(buffer+(0..tiff_size-1));
@ requires \valid(potential_error);
@ requires \separated(potential_error, buffer);
- @ ensures \valid_read(buffer+(0..tiff_size-1));
+ @ assigns *potential_error;
@*/
unsigned int find_tag_from_tiff_header_le(const unsigned char *buffer, const unsigned int tiff_size, const unsigned int tag, const unsigned char**potential_error);
#endif
@@ -109,12 +109,21 @@ void file_check_tiff_le(file_recovery_t *fr);
@ requires buffer_size >= 15;
@ 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;
+ @ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
+ @ ensures \result == 1 ==> \initialized(&file_recovery_new->time);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_tiff_le);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null);
@ ensures (\result == 1) ==> (file_recovery_new->extension != \null);
@ ensures (\result == 1) ==> valid_read_string(file_recovery_new->extension);
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
@*/
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);
#endif
@@ -126,7 +135,7 @@ int header_check_tiff_le(const unsigned char *buffer, const unsigned int buffer_
@ requires \valid_read(buffer+(0..tiff_size-1));
@ requires \valid(potential_error);
@ requires \separated(potential_error, buffer);
- @ ensures \valid_read(buffer+(0..tiff_size-1));
+ @ assigns *potential_error;
@*/
unsigned int find_tag_from_tiff_header_be(const unsigned char*buffer, const unsigned int tiff_size, const unsigned int tag, const unsigned char**potential_error);
#endif
@@ -136,11 +145,20 @@ unsigned int find_tag_from_tiff_header_be(const unsigned char*buffer, const unsi
@ requires buffer_size >= 15;
@ 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;
+ @ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
+ @ ensures \result == 1 ==> \initialized(&file_recovery_new->time);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null);
@ ensures (\result == 1) ==> (file_recovery_new->extension != \null);
@ ensures (\result == 1) ==> valid_read_string(file_recovery_new->extension);
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
@*/
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);
#endif
diff --git a/src/file_tiff_be.c b/src/file_tiff_be.c
index dfe17a3..84b33af 100644
--- a/src/file_tiff_be.c
+++ b/src/file_tiff_be.c
@@ -54,8 +54,31 @@ static const char *extension_pef="pef";
#ifndef MAIN_tiff_le
/*@
@ requires \valid_read(buffer+(0..tiff_size-1));
+ @ ensures \result <= 0xffff;
+ @ assigns \nothing;
+ @ */
+static unsigned int get_nbr_fields_be(const unsigned char *buffer, const unsigned int tiff_size, const unsigned int offset_hdr)
+{
+ const unsigned char *ptr_hdr;
+ const struct ifd_header *hdr;
+ if(sizeof(struct ifd_header) > tiff_size)
+ return 0;
+ /*@ assert tiff_size >= sizeof(struct ifd_header); */
+ if(offset_hdr > tiff_size - sizeof(struct ifd_header))
+ return 0;
+ /*@ assert offset_hdr + sizeof(struct ifd_header) <= tiff_size; */
+ ptr_hdr=&buffer[offset_hdr];
+ /*@ assert \valid_read(ptr_hdr + (0 .. sizeof(struct ifd_header)-1)); */
+ hdr=(const struct ifd_header *)ptr_hdr;
+ /*@ assert \valid_read(hdr); */
+ return be16(hdr->nbr_fields);
+}
+
+/*@
+ @ requires \valid_read(buffer+(0..tiff_size-1));
@ requires \valid(potential_error);
@ requires \separated(potential_error, buffer+(..));
+ @ assigns *potential_error;
@
*/
static unsigned int find_tag_from_tiff_header_be_aux(const unsigned char *buffer, const unsigned int tiff_size, const unsigned int tag, const unsigned char**potential_error, const unsigned int offset_hdr)
@@ -143,6 +166,25 @@ unsigned int find_tag_from_tiff_header_be(const unsigned char *buffer, const uns
if(tmp)
return tmp;
}
+ {
+ const unsigned int nbr_fields=get_nbr_fields_be(buffer, tiff_size, offset_ifd0);
+ unsigned int offset_tiff_next_diroff;
+ offset_tiff_next_diroff=offset_ifd0 + 2 + nbr_fields * sizeof(TIFFDirEntry);
+ /*@ assert tiff_size >= 4; */
+ if(offset_tiff_next_diroff < tiff_size - 4)
+ {
+ const unsigned char *ptr_hdr;
+ /*@ assert offset_tiff_next_diroff + 4 <= tiff_size; */
+ ptr_hdr=&buffer[offset_tiff_next_diroff];
+ /*@ assert \valid_read(ptr_hdr + (0 .. 4-1)); */
+ const uint32_t *tiff_next_diroff=(const uint32_t *)ptr_hdr;
+ /*@ assert \valid_read(tiff_next_diroff); */
+ /* IFD1 */
+ const unsigned int offset_ifd1=be32(*tiff_next_diroff);
+ if(offset_ifd1 > 0)
+ return find_tag_from_tiff_header_be_aux(buffer, tiff_size, tag, potential_error, offset_ifd1);
+ }
+ }
/*@ assert \valid_read(buffer+(0..tiff_size-1)); */
return 0;
}
diff --git a/src/file_tiff_le.c b/src/file_tiff_le.c
index 590e7bf..d12f146 100644
--- a/src/file_tiff_le.c
+++ b/src/file_tiff_le.c
@@ -58,8 +58,31 @@ static const char *extension_sr2="sr2";
#ifndef MAIN_tiff_be
/*@
@ requires \valid_read(buffer+(0..tiff_size-1));
+ @ ensures \result <= 0xffff;
+ @ assigns \nothing;
+ @ */
+static unsigned int get_nbr_fields_le(const unsigned char *buffer, const unsigned int tiff_size, const unsigned int offset_hdr)
+{
+ const unsigned char *ptr_hdr;
+ const struct ifd_header *hdr;
+ if(sizeof(struct ifd_header) > tiff_size)
+ return 0;
+ /*@ assert tiff_size >= sizeof(struct ifd_header); */
+ if(offset_hdr > tiff_size - sizeof(struct ifd_header))
+ return 0;
+ /*@ assert offset_hdr + sizeof(struct ifd_header) <= tiff_size; */
+ ptr_hdr=&buffer[offset_hdr];
+ /*@ assert \valid_read(ptr_hdr + (0 .. sizeof(struct ifd_header)-1)); */
+ hdr=(const struct ifd_header *)ptr_hdr;
+ /*@ assert \valid_read(hdr); */
+ return le16(hdr->nbr_fields);
+}
+
+/*@
+ @ requires \valid_read(buffer+(0..tiff_size-1));
@ requires \valid(potential_error);
@ requires \separated(potential_error, buffer+(..));
+ @ assigns *potential_error;
@
*/
static unsigned int find_tag_from_tiff_header_le_aux(const unsigned char *buffer, const unsigned int tiff_size, const unsigned int tag, const unsigned char**potential_error, const unsigned int offset_hdr)
@@ -146,6 +169,24 @@ unsigned int find_tag_from_tiff_header_le(const unsigned char *buffer, const uns
if(tmp)
return tmp;
}
+ {
+ const unsigned int nbr_fields=get_nbr_fields_le(buffer, tiff_size, offset_ifd0);
+ unsigned int offset_tiff_next_diroff;
+ offset_tiff_next_diroff=offset_ifd0 + 2 + nbr_fields * sizeof(TIFFDirEntry);
+ if(offset_tiff_next_diroff < tiff_size - 4)
+ {
+ const unsigned char *ptr_hdr;
+ /*@ assert offset_tiff_next_diroff + 4 <= tiff_size; */
+ ptr_hdr=&buffer[offset_tiff_next_diroff];
+ /*@ assert \valid_read(ptr_hdr + (0 .. 4-1)); */
+ const uint32_t *tiff_next_diroff=(const uint32_t *)ptr_hdr;
+ /*@ assert \valid_read(tiff_next_diroff); */
+ /* IFD1 */
+ const unsigned int offset_ifd1=le32(*tiff_next_diroff);
+ if(offset_ifd1 > 0)
+ return find_tag_from_tiff_header_le_aux(buffer, tiff_size, tag, potential_error, offset_ifd1);
+ }
+ }
/*@ assert \valid_read(buffer+(0..tiff_size-1)); */
return 0;
}