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

PhotoRec: stricter check when recovering .pf files

Browse source
This commit is contained in:
Christophe Grenier 2019-10-13 11:33:25 +02:00
parent 62c0d6c34d
commit b65fc363fe
1 changed files with 114 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

115
src/file_pf.c
View file

@ -31,6 +31,9 @@
#include "types.h"
#include "filegen.h"
#include "common.h"
#if defined(__FRAMAC__)
#include "__fc_builtin.h"
#endif
static void register_header_check_pf(file_stat_t *file_stat);
@ -54,6 +57,10 @@ struct pf_header
uint32_t unknown2;
} __attribute__ ((gcc_struct, __packed__));
/*@
@ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename);
@*/
static void file_rename_pf(file_recovery_t *file_recovery)
{
FILE *file;
@ -69,12 +76,29 @@ static void file_rename_pf(file_recovery_t *file_recovery)
file_rename_unicode(file_recovery, &hdr.name, sizeof(hdr.name), 0, "pf", 0);
}
/*@
@ requires buffer_size >= sizeof(struct pf_header);
@ 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 separation: \separated(file_recovery, file_recovery_new);
@ ensures \result == 0 || \result == 1;
@ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_pf.extension);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= sizeof(struct pf_header));
@ ensures (\result == 1) ==> (file_recovery_new->file_rename==&file_rename_pf);
@ ensures (\result == 1) ==> (file_recovery_new->data_check==&data_check_size);
@ ensures (\result == 1) ==> (file_recovery_new->file_check==&file_check_size);
@*/
static int header_check_pf(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 struct pf_header *pf=(const struct pf_header *)buffer;
const unsigned int size=le32(pf->size);
if(size < sizeof(struct pf_header))
return 0;
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_pf.extension;
file_recovery_new->calculated_file_size=(uint64_t)le32(pf->size);
file_recovery_new->calculated_file_size=size;
file_recovery_new->file_rename=&file_rename_pf;
file_recovery_new->data_check=&data_check_size;
file_recovery_new->file_check=&file_check_size;
@ -86,3 +110,92 @@ static void register_header_check_pf(file_stat_t *file_stat)
static const unsigned char pf_header[7] = {0x00, 0x00, 0x00, 'S', 'C', 'C', 'A'};
register_header_check(1, pf_header,sizeof(pf_header), &header_check_pf, file_stat);
}
#if defined(MAIN_pf)
#define BLOCKSIZE 65536u
int main()
{
const char *fn = "recup_dir.1/f0000000.pf";
unsigned char buffer[BLOCKSIZE];
file_recovery_t file_recovery_new;
file_recovery_t file_recovery;
file_stat_t file_stats;
/*@ assert \valid(buffer + (0 .. (BLOCKSIZE - 1))); */
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
#endif
reset_file_recovery(&file_recovery);
file_recovery.blocksize=BLOCKSIZE;
file_recovery_new.blocksize=BLOCKSIZE;
file_recovery_new.data_check=NULL;
file_recovery_new.file_stat=NULL;
file_recovery_new.file_check=NULL;
file_recovery_new.file_rename=NULL;
file_recovery_new.calculated_file_size=0;
file_recovery_new.file_size=0;
file_recovery_new.location.start=0;
file_stats.file_hint=&file_hint_pf;
file_stats.not_recovered=0;
file_stats.recovered=0;
register_header_check_pf(&file_stats);
if(header_check_pf(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
return 0;
/*@ assert valid_read_string(fn); */
strcpy(file_recovery_new.filename, fn);
/*@ assert file_recovery_new.file_size == 0; */
/*@ assert file_recovery_new.extension == file_hint_pf.extension; */
/*@ assert file_recovery_new.file_rename==&file_rename_pf; */
/*@ assert file_recovery_new.file_check == &file_check_size; */
/*@ assert file_recovery_new.data_check == &data_check_size; */
file_recovery_new.file_stat=&file_stats;
/*@ assert valid_read_string((char *)file_recovery_new.filename); */
if(file_recovery_new.file_stat!=NULL && file_recovery_new.file_stat->file_hint!=NULL &&
file_recovery_new.data_check!=NULL)
{
unsigned char big_buffer[2*BLOCKSIZE];
data_check_t res_data_check=DC_CONTINUE;
memset(big_buffer, 0, BLOCKSIZE);
memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
/*@ assert file_recovery_new.data_check == &data_check_size; */
/*@ assert file_recovery_new.file_size == 0; */;
res_data_check=data_check_size(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
file_recovery_new.file_size+=BLOCKSIZE;
if(res_data_check == DC_CONTINUE)
{
memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
#endif
data_check_size(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
}
}
{
file_recovery_t file_recovery_new2;
/* Test when another file of the same is detected in the next block */
file_recovery_new2.blocksize=BLOCKSIZE;
file_recovery_new2.file_stat=NULL;
file_recovery_new2.file_check=NULL;
file_recovery_new2.location.start=BLOCKSIZE;
file_recovery_new.handle=NULL; /* In theory should be not null */
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
#endif
/*@ assert valid_read_string((char *)file_recovery_new.filename); */
header_check_pf(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
}
file_recovery_new.handle=fopen(fn, "rb");
/*@ assert file_recovery_new.file_check == &file_check_size; */
if(file_recovery_new.handle!=NULL)
{
file_check_size(&file_recovery_new);
fclose(file_recovery_new.handle);
}
/*@ assert file_recovery_new.file_rename==&file_rename_pf; */
/*@ assert valid_read_string((char *)file_recovery_new.filename); */
file_rename_pf(&file_recovery_new);
return 0;
}
#endif