luisgulo/testdisk
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

PhotoRec - file_tiff*.c: Reintroduce fixed IFD1 parsing.

Browse source 
Buggy version was removed by commit 7e8f99aa92
This commit is contained in:
Christophe Grenier 2020-01-18 10:18:17 +01:00
parent 611da961b3
commit 9b51c2aeb0
3 changed files with 104 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/file_tiff.h
View file

@ -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

42
src/file_tiff_be.c
View file

@ -52,10 +52,33 @@ static const char *extension_nef="nef";
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;
}

41
src/file_tiff_le.c
View file

@ -56,10 +56,33 @@ static const char *extension_nef="nef";
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;
}