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

src/file_riff.c: add Frama-C annotations, stricter checks

Browse Source
This commit is contained in:
Christophe Grenier 2021-03-03 18:18:15 +01:00
parent 08875f5581
commit 03844caa4f
4 changed files with 162 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Makefile.am
View File

@ -389,7 +389,7 @@ file_C = filegen.c \
file_zip.c \
file_zpr.c
file_H = ext2.h hfsp_struct.h filegen.h file_doc.h file_jpg.h file_gz.h file_sp3.h file_tar.h file_tiff.h file_txt.h luks_struct.h ntfs_struct.h ole.h pe.h suspend.h
file_H = ext2.h hfsp_struct.h filegen.h file_doc.h file_jpg.h file_gz.h file_riff.h file_sp3.h file_tar.h file_tiff.h file_txt.h luks_struct.h ntfs_struct.h ole.h pe.h suspend.h
photorec_C = photorec.c phcfg.c addpart.c chgarch.c chgtype.c dir.c exfatp.c ext2grp.c ext2_dir.c ext2p.c fat_dir.c fatp.c file_found.c geometry.c ntfs_dir.c ntfsp.c pdisksel.c poptions.c sessionp.c dfxml.c partgptro.c

4
src/file_jpg.c
View File

@ -55,6 +55,9 @@
#include "common.h"
#include "log.h"
#include "file_jpg.h"
#if !defined(MAIN_jpg) && !defined(SINGLE_FORMAT)
#include "file_riff.h"
#endif
#include "file_tiff.h"
#include "setdate.h"
#if defined(__FRAMAC__)
@ -67,7 +70,6 @@ extern const file_hint_t file_hint_indd;
extern const file_hint_t file_hint_mov;
extern const file_hint_t file_hint_riff;
extern const file_hint_t file_hint_rw2;
extern data_check_t data_check_avi_stream(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
#endif
/*@ requires \valid(file_stat); */

142
src/file_riff.c
View File

@ -31,11 +31,12 @@
#include "types.h"
#include "filegen.h"
#include "common.h"
#include "file_riff.h"
#ifdef DEBUG_RIFF
#include "log.h"
#endif
data_check_t data_check_avi_stream(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
/*@ requires \valid(file_stat); */
static void register_header_check_riff(file_stat_t *file_stat);
const file_hint_t file_hint_riff= {
@ -58,10 +59,10 @@ typedef struct {
uint32_t dwSize;
uint32_t dwFourCC;
// char data[dwSize-4];
} riff_list_header;
} riff_list_header_t;
#ifdef DEBUG_RIFF
static void log_riff_list(const uint64_t offset, const unsigned int depth, const riff_list_header *list_header)
static void log_riff_list(const uint64_t offset, const unsigned int depth, const riff_list_header_t *list_header)
{
unsigned int i;
log_info("0x%08lx - 0x%08lx ", offset, offset + 8 - 1 + le32(list_header->dwSize));
@ -79,7 +80,7 @@ static void log_riff_list(const uint64_t offset, const unsigned int depth, const
le32(list_header->dwSize));
}
static void log_riff_chunk(const uint64_t offset, const unsigned int depth, const riff_list_header *list_header)
static void log_riff_chunk(const uint64_t offset, const unsigned int depth, const riff_list_header_t *list_header)
{
unsigned int i;
if(le32(list_header->dwSize)==0)
@ -96,53 +97,102 @@ static void log_riff_chunk(const uint64_t offset, const unsigned int depth, cons
}
#endif
/*@
@ requires \valid(fr);
@ requires valid_file_recovery(fr);
@ requires \valid(fr->handle);
@ requires \separated(fr, fr->handle, fr->extension, &errno, &Frama_C_entropy_source);
@ requires end <= PHOTOREC_MAX_FILE_SIZE;
@ ensures valid_file_recovery(fr);
@ ensures \valid(fr->handle);
@ assigns *fr->handle, errno;
@ assigns fr->offset_error;
@ assigns Frama_C_entropy_source;
@*/
static void check_riff_list(file_recovery_t *fr, const unsigned int depth, const uint64_t start, const uint64_t end)
{
uint64_t file_size;
riff_list_header list_header;
if(depth>5)
return;
/*@
@ loop invariant valid_file_recovery(fr);
@ loop invariant \valid(fr->handle);
@ loop assigns *fr->handle, errno;
@ loop assigns fr->offset_error;
@ loop assigns Frama_C_entropy_source;
@ loop assigns file_size;
@*/
for(file_size=start; file_size < end;)
{
char buf[sizeof(riff_list_header_t)];
uint64_t next_fs;
const riff_list_header_t *list_header=(const riff_list_header_t *)&buf;
if(my_fseek(fr->handle, file_size, SEEK_SET)<0)
{
fr->offset_error=file_size;
return;
}
if (fread(&list_header, sizeof(list_header), 1, fr->handle)!=1)
if (fread(buf, sizeof(buf), 1, fr->handle)!=1)
{
fr->offset_error=file_size;
return;
}
if(memcmp(&list_header.dwList, "LIST", 4) == 0)
#if defined(__FRAMAC__)
Frama_C_make_unknown(buf, sizeof(buf));
#endif
/*@ assert \initialized((char *)list_header+ (0 .. sizeof(riff_list_header_t)-1)); */
next_fs=file_size + (uint64_t)8 + le32(list_header->dwSize);
if(next_fs > end)
{
fr->offset_error=file_size;
return;
}
/*@ assert valid_file_recovery(fr); */
if(memcmp(&list_header->dwList, "LIST", 4) == 0)
{
#ifdef DEBUG_RIFF
log_riff_list(file_size, depth, &list_header);
log_riff_list(file_size, depth, list_header);
#endif
check_riff_list(fr, depth+1, file_size + sizeof(list_header), file_size + 8 - 1 + le32(list_header.dwSize));
check_riff_list(fr, depth+1, file_size + sizeof(riff_list_header_t), next_fs-1);
}
else
{
#ifdef DEBUG_RIFF
/* It's a chunk */
log_riff_chunk(file_size, depth, &list_header);
log_riff_chunk(file_size, depth, list_header);
#endif
}
file_size += (uint64_t)8 + le32(list_header.dwSize);
file_size = next_fs;
/* align to word boundary */
file_size += (file_size&1);
file_size = (file_size&1);
}
}
/*@
@ requires \valid(fr);
@ requires valid_file_recovery(fr);
@ requires \separated(fr, fr->handle, fr->extension, &errno, &Frama_C_entropy_source);
@ requires fr->file_check == &file_check_avi;
@ ensures \valid(fr->handle);
@ assigns *fr->handle, errno, fr->file_size;
@ assigns fr->offset_error, fr->offset_ok;
@ assigns Frama_C_entropy_source;
@*/
static void file_check_avi(file_recovery_t *fr)
{
fr->file_size = 0;
fr->offset_error=0;
fr->offset_ok=0;
/*@
@ loop assigns *fr->handle, errno, fr->file_size;
@ loop assigns fr->offset_error, fr->offset_ok;
@ loop assigns Frama_C_entropy_source;
@*/
while(fr->file_size!=fr->calculated_file_size)
{
const uint64_t file_size=fr->file_size;
riff_list_header list_header;
riff_list_header_t list_header;
uint64_t calculated_file_size;
if(my_fseek(fr->handle, fr->file_size, SEEK_SET)<0)
{
fr->file_size=0;
@ -161,22 +211,42 @@ static void file_check_avi(file_recovery_t *fr)
fr->offset_error=fr->file_size;
return;
}
check_riff_list(fr, 1, file_size + sizeof(list_header), file_size + 8 - 1 + le32(list_header.dwSize));
calculated_file_size=file_size + 8 + le32(list_header.dwSize);
if(calculated_file_size > PHOTOREC_MAX_FILE_SIZE)
{
fr->file_size=0;
return;
}
/*@ assert calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */
check_riff_list(fr, 1, file_size + sizeof(list_header), calculated_file_size - 1);
if(fr->offset_error > 0)
{
fr->file_size=0;
return;
}
fr->file_size=file_size + 8 + le32(list_header.dwSize);
fr->file_size=calculated_file_size;
}
}
/*@
@ requires buffer_size > 0;
@ requires (buffer_size&1)==0;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \valid(file_recovery);
@ requires file_recovery->data_check==&data_check_avi;
@ requires file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE;
@ requires \separated(buffer, file_recovery);
@ ensures \result == DC_CONTINUE || \result == DC_STOP;
@ assigns file_recovery->calculated_file_size;
@*/
static data_check_t data_check_avi(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
/*@ loop assigns file_recovery->calculated_file_size; */
while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size &&
file_recovery->calculated_file_size + 12 < file_recovery->file_size + buffer_size/2)
file_recovery->calculated_file_size + 12 <= file_recovery->file_size + buffer_size/2)
{
const unsigned int i=file_recovery->calculated_file_size - file_recovery->file_size + buffer_size/2;
const unsigned int i=file_recovery->calculated_file_size + buffer_size/2 - file_recovery->file_size;
/*@ assert 0 <= i <= buffer_size - 12; */
const riff_chunk_header *chunk_header=(const riff_chunk_header*)&buffer[i];
if(memcmp(&buffer[i], "RIFF", 4)==0 && memcmp(&buffer[i+8], "AVIX", 4)==0)
file_recovery->calculated_file_size += (uint64_t)8 + le32(chunk_header->dwSize);
@ -188,10 +258,12 @@ static data_check_t data_check_avi(const unsigned char *buffer, const unsigned i
data_check_t data_check_avi_stream(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
/*@ loop assigns file_recovery->calculated_file_size; */
while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size &&
file_recovery->calculated_file_size + 8 < file_recovery->file_size + buffer_size/2)
file_recovery->calculated_file_size + 8 <= file_recovery->file_size + buffer_size/2)
{
const unsigned int i=file_recovery->calculated_file_size - file_recovery->file_size + buffer_size/2;
const unsigned int i=file_recovery->calculated_file_size + buffer_size/2 - file_recovery->file_size;
/*@ assert 0 <= i <= buffer_size - 8; */
const riff_chunk_header *chunk_header=(const riff_chunk_header*)&buffer[i];
if(buffer[i+2]!='d' || buffer[i+3]!='b') /* Video Data Binary ?*/
{
@ -208,12 +280,16 @@ data_check_t data_check_avi_stream(const unsigned char *buffer, const unsigned i
return DC_CONTINUE;
}
static void file_check_size_rifx(file_recovery_t *file_recovery)
{
if(file_recovery->file_size<file_recovery->calculated_file_size)
file_recovery->file_size=0;
}
/*@
@ requires buffer_size >= 12;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires valid_file_recovery(file_recovery);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ requires separation: \separated(&file_hint_riff, buffer+(..), file_recovery, file_recovery_new);
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@ assigns *file_recovery_new;
@*/
static int header_check_riff(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)
{
uint64_t size;
@ -252,7 +328,7 @@ static int header_check_riff(const unsigned char *buffer, const unsigned int buf
size+=8;
if(memcmp(&buffer[8],"AVI ",4)==0)
{
const riff_list_header list_movi={
const riff_list_header_t list_movi={
.dwList=be32(0x4c495354), /* LIST */
.dwSize=le32(4),
.dwFourCC=be32(0x6d6f7669) /* movi */
@ -260,7 +336,7 @@ static int header_check_riff(const unsigned char *buffer, const unsigned int buf
reset_file_recovery(file_recovery_new);
file_recovery_new->extension="avi";
/* Is it a raw avi stream with Data Binary chunks ? */
if(size < buffer_size - 4 &&
if(size >= sizeof(list_movi) && size <= buffer_size - 4 &&
memcmp(&buffer[size - sizeof(list_movi)], &list_movi, sizeof(list_movi)) ==0 &&
buffer[size+2]=='d' &&
buffer[size+3]=='b')
@ -315,13 +391,23 @@ static int header_check_riff(const unsigned char *buffer, const unsigned int buf
return 1;
}
/*@
@ requires buffer_size >= 12;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires valid_file_recovery(file_recovery);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ requires separation: \separated(&file_hint_riff, buffer+(..), file_recovery, file_recovery_new);
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@ assigns *file_recovery_new;
@*/
static int header_check_rifx(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)
{
if(memcmp(&buffer[8],"Egg!",4)==0)
{
/* After Effects */
reset_file_recovery(file_recovery_new);
file_recovery_new->file_check=&file_check_size_rifx;
file_recovery_new->file_check=&file_check_size_min;
file_recovery_new->calculated_file_size=(uint64_t)buffer[7]+(((uint64_t)buffer[6])<<8)+(((uint64_t)buffer[5])<<16)+(((uint64_t)buffer[4])<<24)+8;
file_recovery_new->extension="aep";
return 1;

44
src/file_riff.h Normal file
View File

@ -0,0 +1,44 @@
/*
File: file_riff.h
Copyright (C) 2021 Christophe GRENIER <grenier@cgsecurity.org>
This software is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License along
with this program; if not, write the Free Software Foundation, Inc., 51
Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*/
#ifndef _FILE_RIFF_H
#define _FILE_RIFF_H
#ifdef __cplusplus
extern "C" {
#endif
/*@
@ requires buffer_size > 0;
@ requires (buffer_size&1)==0;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \valid(file_recovery);
@ requires file_recovery->data_check==&data_check_avi_stream;
@ requires file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE;
@ requires \separated(buffer, file_recovery);
@ ensures \result == DC_CONTINUE || \result == DC_STOP;
@ assigns file_recovery->calculated_file_size;
@*/
data_check_t data_check_avi_stream(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
#ifdef __cplusplus
} /* closing brace for extern "C" */
#endif
#endif