PhotoRec: exe - rewrite the resource parser.

This commit is contained in:
Christophe Grenier 2019-09-26 20:38:23 +02:00
parent 0f09fa0121
commit 806a1f4bb5

View file

@ -35,6 +35,9 @@
#include "filegen.h"
#include "pe.h"
#include "log.h"
#if defined(__FRAMAC__)
#include "__fc_builtin.h"
#endif
static void register_header_check_exe(file_stat_t *file_stat);
static void file_rename_pe_exe(file_recovery_t *file_recovery);
@ -48,8 +51,18 @@ const file_hint_t file_hint_exe= {
.register_header_check=&register_header_check_exe
};
static const char *extension_dll="dll";
static const unsigned char exe_header[2] = {'M','Z'};
/*@
@ requires buffer_size >= 2;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \valid_read(file_recovery);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ ensures \result == 0 || \result == 1;
@ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_exe.extension || file_recovery_new->extension == extension_dll);
@*/
static int header_check_exe(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 dos_image_file_hdr *dos_hdr=(const struct dos_image_file_hdr*)buffer;
@ -64,6 +77,7 @@ static int header_check_exe(const unsigned char *buffer, const unsigned int buff
/* NE Win16 */
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_exe.extension;
file_recovery_new->min_filesize=le32(dos_hdr->e_lfanew) + sizeof(struct pe_image_file_hdr);
return 1;
}
if((le32(pe_hdr->Magic) & 0xffff) == IMAGE_NT_SIGNATURE)
@ -73,7 +87,7 @@ static int header_check_exe(const unsigned char *buffer, const unsigned int buff
{
/* Dynamic Link Library */
reset_file_recovery(file_recovery_new);
file_recovery_new->extension="dll";
file_recovery_new->extension=extension_dll;
}
else if(le16(pe_hdr->Characteristics) & 0x02)
{
@ -92,6 +106,9 @@ static int header_check_exe(const unsigned char *buffer, const unsigned int buff
{
const struct pe_image_optional_hdr32 *pe_image_optional32=(const struct pe_image_optional_hdr32 *)
(((const unsigned char*)pe_hdr + sizeof(struct pe_image_file_hdr)));
if((const unsigned char*)(pe_image_optional32+1) <= buffer+buffer_size)
{
/*@ assert \valid_read(pe_image_optional32); */
if(le16(pe_image_optional32->Magic)==IMAGE_NT_OPTIONAL_HDR_MAGIC)
{
log_debug("SizeOfCode %lx\n", (long unsigned)le32(pe_image_optional32->SizeOfCode));
@ -105,10 +122,11 @@ static int header_check_exe(const unsigned char *buffer, const unsigned int buff
log_debug("PE image opt 0x%lx-0x%lx\n", (long unsigned)sizeof(struct pe_image_file_hdr),
(long unsigned)(sizeof(struct pe_image_file_hdr) + le16(pe_hdr->SizeOfOptionalHeader) - 1));
}
}
#endif
{
unsigned int i;
uint64_t sum=0;
uint64_t sum=le32(dos_hdr->e_lfanew) + sizeof(struct pe_image_file_hdr);
const struct pe_image_section_hdr *pe_image_section=(const struct pe_image_section_hdr*)
((const unsigned char*)pe_hdr + sizeof(struct pe_image_file_hdr) + le16(pe_hdr->SizeOfOptionalHeader));
for(i=0;
@ -132,7 +150,9 @@ static int header_check_exe(const unsigned char *buffer, const unsigned int buff
}
if(le16(pe_image_section->NumberOfRelocations)>0)
{
/*@ assert le16(pe_image_section->NumberOfRelocations)>0; */
const uint64_t tmp=(uint64_t)le32(pe_image_section->PointerToRelocations)+ 1*le16(pe_image_section->NumberOfRelocations);
/*@ assert tmp > 0; */
#ifdef DEBUG_EXE
log_debug("relocations 0x%lx-0x%lx\n",
(unsigned long)le32(pe_image_section->PointerToRelocations),
@ -144,7 +164,9 @@ static int header_check_exe(const unsigned char *buffer, const unsigned int buff
}
if(le32(pe_hdr->NumberOfSymbols)>0)
{
/*@ assert le32(pe_hdr->NumberOfSymbols)>0; */
const uint64_t tmp=(uint64_t)le32(pe_hdr->PointerToSymbolTable)+ IMAGE_SIZEOF_SYMBOL*(uint64_t)le32(pe_hdr->NumberOfSymbols);
/*@ assert tmp > 0; */
#ifdef DEBUG_EXE
log_debug("Symboles 0x%lx-0x%lx\n", (long unsigned)le32(pe_hdr->PointerToSymbolTable),
(long unsigned)(tmp-1));
@ -179,25 +201,38 @@ static int header_check_exe(const unsigned char *buffer, const unsigned int buff
{ /* COFF_I386MAGIC */
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_exe.extension;
file_recovery_new->min_filesize=coff_offset+2;
return 1;
}
#ifdef DEBUG_EXE
{
unsigned int i;
const struct exe_reloc *exe_reloc;
const struct exe_reloc *exe_relocs;
const unsigned int reloc_table_offset=le16(dos_hdr->reloc_table_offset);
const unsigned int num_relocs=le16(dos_hdr->num_relocs);
log_info("Maybe a DOS EXE\n");
log_info("blocks %llu\n", (long long unsigned)coff_offset);
log_info("data start %llx\n", (long long unsigned)16*le16(dos_hdr->header_paragraphs));
log_info("reloc %u\n", le16(dos_hdr->num_relocs));
for(i=0, exe_reloc=(const struct exe_reloc *)(buffer+le16(dos_hdr->reloc_table_offset));
i < le16(dos_hdr->num_relocs) &&
le16(dos_hdr->reloc_table_offset)+ (i+1)*sizeof(struct exe_reloc) < buffer_size;
i++, exe_reloc++)
log_info("reloc %u\n", num_relocs);
if(reloc_table_offset + num_relocs * sizeof(struct exe_reloc) <= buffer_size)
{
unsigned int i;
/*@ assert reloc_table_offset + num_relocs * sizeof(struct exe_reloc) <= buffer_size; */
exe_relocs=(const struct exe_reloc *)(buffer+reloc_table_offset);
/*@ assert \valid_read(exe_relocs + (0 .. num_relocs-1)); */
/*@
@ loop invariant 0 <= i <= num_relocs;
@ loop variant num_relocs -i;
@ */
for(i=0; i < num_relocs; i++)
{
/*@ assert 0 <= i <= num_relocs; */
const struct exe_reloc *exe_reloc=&exe_relocs[i];
/*@ assert \valid_read(exe_reloc); */
log_info("offset %x, segment %x\n",
le16(exe_reloc->offset), le16(exe_reloc->segment));
}
}
}
#endif
}
return 0;
@ -209,11 +244,17 @@ struct rsrc_entries_s
uint32_t Pos;
} __attribute__ ((gcc_struct, __packed__));
struct rsrc_offlen
{
uint32_t off;
uint32_t len;
} __attribute__ ((gcc_struct, __packed__));
struct PE_index
{
uint16_t len;
uint16_t val_len;
uint16_t type;
uint16_t type; /* 0=binary data, 1=text*/
} __attribute__ ((gcc_struct, __packed__));
static char vs_version_info[32]={
@ -237,276 +278,586 @@ static char InternalName[24]={
'N', 0x0, 'a', 0x0, 'm', 0x0, 'e', 0x0
};
static unsigned int ReadUnicodeStr(const char *buffer, unsigned int pos, const unsigned int len)
{
for(; pos+2<len && (buffer[pos]!='\0' || buffer[pos+1]!='\0'); pos+=2)
{
#ifdef DEBUG_EXE
log_info("%c", buffer[pos]);
#endif
}
pos+=2;
if((pos & 0x03)!=0)
pos+=2;
return pos;
}
static int PEVersion_aux(file_recovery_t *file_recovery, const char*buffer, const unsigned int end, const char *needle, const unsigned int needle_len, const int force_ext)
{
unsigned int pos=0;
while(1)
/*@
@ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename);
@ requires needle_len > 0;
@ requires \valid_read(buffer+(0..end-1));
@ requires \valid_read(needle+(0..needle_len-1));
@*/
static int parse_String(file_recovery_t *file_recovery, const char*buffer, const unsigned int end, const char *needle, const unsigned int needle_len, const int force_ext)
{
const struct PE_index *PE_index;
pos=(pos + 3) & 0xfffffffc; /* align on a 4-byte boundary */
if(pos + 6 > end)
unsigned int len;
unsigned int val_len;
unsigned int type;
if(6 > end)
{
return -1;
}
PE_index=(const struct PE_index*)&buffer[pos];
if(le16(PE_index->len)==0 && le16(PE_index->val_len)==0)
{
PE_index=(const struct PE_index*)buffer;
len=le16(PE_index->len);
val_len=le16(PE_index->val_len);
type=le16(PE_index->type);
log_info("parse_String len=%u val_len=%u type=%u\n", len, val_len, type);
if(len > end)
return -1;
}
if(6 + 2 * val_len > len)
return -1;
dump_log(buffer, len);
// type=1 => text
if(6+needle_len < end && type==1 && memcmp(&buffer[6], needle, needle_len)==0)
{
const char *stringName=&buffer[pos+6];
if(pos + 6 + sizeof(vs_version_info) < end &&
memcmp(stringName, vs_version_info, sizeof(vs_version_info))==0)
{
pos+=6+sizeof(vs_version_info);
if((pos & 0x03)!=0)
pos+=2;
pos+=le16(PE_index->val_len);
}
else if(pos + 6 + sizeof(StringFileInfo) < end &&
memcmp(stringName, StringFileInfo, sizeof(StringFileInfo))==0 &&
le16(PE_index->val_len)==0)
{
unsigned int i;
unsigned int pt=pos+6+sizeof(StringFileInfo);
pos+=le16(PE_index->len);
for(i=0; pt + 6 < pos; i++)
{
if(i==0)
{
pt=ReadUnicodeStr(buffer, pt+6, pos);
}
else
{
int do_rename=0;
PE_index=(const struct PE_index*)&buffer[pt];
if(pt+6+needle_len < end &&
memcmp(&buffer[pt+6], needle, needle_len)==0)
{
do_rename=1;
}
pt=ReadUnicodeStr(buffer, pt+6, pos);
if(le16(PE_index->val_len)>0)
{
if(do_rename)
{
file_rename_unicode(file_recovery, buffer, end, pt, NULL, force_ext);
return 0;
}
#ifdef DEBUG_EXE
log_info(": ");
#endif
pt=ReadUnicodeStr(buffer, pt, pos);
}
}
#ifdef DEBUG_EXE
log_info("\n");
#endif
}
}
else
{
pos+=le16(PE_index->len)+le16(PE_index->val_len);
}
}
if(6 + needle_len + 2 * val_len > len)
return -1;
file_rename_unicode(file_recovery, buffer, end, 6+needle_len, NULL, force_ext);
}
return len;
}
/*@
@ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename);
@ requires needle_len > 0;
@ requires \valid_read(buffer+(0..end-1));
@ requires \valid_read(needle+(0..needle_len-1));
@*/
static int parse_StringArray(file_recovery_t *file_recovery, const char*buffer, const unsigned int end, const char *needle, const unsigned int needle_len, const int force_ext)
{
unsigned int pos=0;
log_info("parse_StringArray end=%u\n", end);
/*@
@ loop variant end - pos;
@*/
while(pos<end)
{
const int res=parse_String(file_recovery, &buffer[pos], end - pos, needle, needle_len, force_ext);
if(res <= 0)
return -1;
/*@ assert res > 0; */
pos+=res;
/* Padding */
if((pos & 0x03)!=0)
pos+=2;
}
return 0;
}
/*@
@ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename);
@ requires needle_len > 0;
@ requires \valid_read(buffer+(0..end-1));
@ requires \valid_read(needle+(0..needle_len-1));
@*/
static int parse_StringTable(file_recovery_t *file_recovery, const char*buffer, const unsigned int end, const char *needle, const unsigned int needle_len, const int force_ext)
{
const struct PE_index *PE_index;
unsigned int pos;
unsigned int len;
unsigned int val_len;
if(6 > end)
{
return -1;
}
PE_index=(const struct PE_index*)buffer;
/*@ assert \valid_read(PE_index); */
len=le16(PE_index->len);
val_len=le16(PE_index->val_len);
log_info("parse_StringTable len=%u val_len=%u type=%u\n", len, val_len, le16(PE_index->type));
if(len > end)
return -1;
/* szKey: language identifier + code page */
pos = 6 + 2*8 + 2;
/* Padding */
if((pos & 0x03)!=0)
pos+=2;
if(pos > len)
return -1;
/* An array of one or more String structures */
return parse_StringArray(file_recovery, &buffer[pos], len - pos, needle, needle_len, force_ext);
}
/*@
@ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename);
@ requires needle_len > 0;
@ requires \valid_read(buffer+(0..end-1));
@ requires \valid_read(needle+(0..needle_len-1));
@*/
static int parse_StringFileInfo(file_recovery_t *file_recovery, const char*buffer, const unsigned int end, const char *needle, const unsigned int needle_len, const int force_ext)
{
/* https://docs.microsoft.com/en-us/windows/win32/menurc/stringfileinfo */
const struct PE_index *PE_index;
unsigned int pos;
unsigned int len;
unsigned int val_len;
if(6 > end)
{
return -1;
}
PE_index=(const struct PE_index*)buffer;
/*@ assert \valid_read(PE_index); */
len=le16(PE_index->len);
val_len=le16(PE_index->val_len);
log_info("parse_StringFileInfo len=%u val_len=%u type=%u\n", len, val_len, le16(PE_index->type));
if(len > end)
return -1;
if(6 + sizeof(StringFileInfo) > end)
return 0;
/* szKey == StringFileInfo ? */
if(memcmp(&buffer[6], StringFileInfo, sizeof(StringFileInfo))!=0)
return 0;
if(val_len!=0)
return -1;
pos=6 + sizeof(StringFileInfo);
/* Padding */
if((pos & 0x03)!=0)
pos+=2;
if(pos > len)
return -1;
return parse_StringTable(file_recovery, &buffer[pos], len - pos, needle, needle_len, force_ext);
}
/*@
@ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename);
@ requires end > 0;
@ requires needle_len > 0;
@ requires \valid_read(buffer+(0..end-1));
@ requires \valid_read(needle+(0..needle_len-1));
@*/
static int parse_VS_VERSIONINFO(file_recovery_t *file_recovery, const char*buffer, const unsigned int end, const char *needle, const unsigned int needle_len, const int force_ext)
{
/* https://docs.microsoft.com/en-us/windows/win32/menurc/vs-versioninfo */
unsigned int pos=0;
const struct PE_index *PE_index;
const char *stringName;
unsigned int len;
unsigned int val_len;
if(6 > end)
{
return -1;
}
PE_index=(const struct PE_index*)buffer;
/*@ assert \valid_read(PE_index); */
len=le16(PE_index->len);
val_len=le16(PE_index->val_len);
log_info("parse_VS_VERSIONINFO len=%u val_len=%u type=%u\n", len, val_len, le16(PE_index->type));
if(len==0 && val_len==0)
{
return -1;
}
if(val_len > len)
return -1;
if(len > end)
return -1;
/*@ assert len <= end; */
pos+=6;
if(pos + sizeof(vs_version_info) >= len)
return -1;
stringName=&buffer[pos];
/* szKey */
if(memcmp(stringName, vs_version_info, sizeof(vs_version_info))!=0)
return -1;
pos+=sizeof(vs_version_info);
/* Padding1 */
if((pos & 0x03)!=0)
pos+=2;
/* VS_FIXEDFILEINFO */
pos+=val_len;
/* Padding2 */
if((pos & 0x03)!=0)
pos+=2;
if(pos > len)
return -1;
/* Children */
/* An array of zero or one StringFileInfo structures, and zero or one
* VarFileInfo structures that are children of the current VS_VERSIONINFO structure. */
if(parse_StringFileInfo(file_recovery, &buffer[pos], len - pos, needle, needle_len, force_ext) < 0)
return -1;
return 0;
}
/*@
@ requires \valid(file);
@ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename);
@*/
static void PEVersion(FILE *file, const unsigned int offset, const unsigned int length, file_recovery_t *file_recovery)
{
char *buffer;
char buffer[1024*1024];
log_info("PEVersion(file, %u, %u, file_recovery)\n", offset, length);
if(length==0 || length > 1024*1024)
return;
if(fseek(file, offset, SEEK_SET)<0)
return ;
buffer=(char*)MALLOC(length);
if(fread(buffer, length, 1, file) != 1)
if(fread(&buffer, length, 1, file) != 1)
{
free(buffer);
return ;
}
if(PEVersion_aux(file_recovery, buffer, length, OriginalFilename, sizeof(OriginalFilename), 0)==0)
#if defined(__FRAMAC__)
Frama_C_make_unknown(&buffer, sizeof(buffer));
#endif
if(parse_VS_VERSIONINFO(file_recovery, (const char *)&buffer, length, OriginalFilename, sizeof(OriginalFilename), 0)==0)
{
free(buffer);
return;
}
PEVersion_aux(file_recovery, buffer, length, InternalName, sizeof(InternalName), 1);
free(buffer);
parse_VS_VERSIONINFO(file_recovery, buffer, length, InternalName, sizeof(InternalName), 1);
}
static void file_exe_ressource(FILE *file, const unsigned int base, const unsigned int dir_start, const unsigned int size, const unsigned int rsrcType, const unsigned int level, const struct pe_image_section_hdr *pe_sections, unsigned int nbr_sections, file_recovery_t *file_recovery)
/*@
@ requires \valid(file);
@ requires base <= 0x7fffffff;
@ requires dir_start <= 0x7fffffff;
@ requires \valid_read(pe_sections);
@ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename);
@*/
static void pe_resource_language(FILE *file, const unsigned int base, const unsigned int dir_start, const struct pe_image_section_hdr *pe_sections, const unsigned int nbr_sections, file_recovery_t *file_recovery)
{
struct rsrc_entries_s *rsrc_entries;
struct rsrc_entries_s *rsrc_entry;
unsigned char buffer[16];
int buffer_size;
unsigned int nameEntries;
unsigned idEntries;
unsigned int count;
unsigned int i;
#ifdef DEBUG_EXE
log_info("file_exe_ressource(file, %u, %u, %u, %u)\n", base, dir_start, size, level);
log_info("pe_resource_language(file, %u, %u)\n", base, dir_start);
#endif
if(level > 2)
return ;
{
unsigned char buffer[16];
unsigned int nameEntries;
unsigned int idEntries;
if(fseek(file, base + dir_start, SEEK_SET)<0)
return ;
buffer_size=fread(buffer, 1, sizeof(buffer), file);
if(buffer_size<16)
if(fread(buffer, 1, sizeof(buffer), file) != sizeof(buffer))
return ;
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)buffer, sizeof(buffer));
#endif
nameEntries = buffer[12]+(buffer[13]<<8);
idEntries = buffer[14]+(buffer[15]<<8);
count = nameEntries + idEntries;
}
log_info("pe_resource_language count=%u\n", count);
if(count==0 || count > 1024)
return ;
/*@ assert 0 < count <= 1024; */
#ifdef __FRAMAC__
rsrc_entries=(struct rsrc_entries_s *)MALLOC(1024 * sizeof(struct rsrc_entries_s));
#else
rsrc_entries=(struct rsrc_entries_s *)MALLOC(count * sizeof(struct rsrc_entries_s));
#endif
/*@ assert \valid((char *)rsrc_entries + (0 .. (unsigned long)((unsigned long)count * sizeof(struct rsrc_entries_s)) - 1)); */
if(fread(rsrc_entries, sizeof(struct rsrc_entries_s), count, file) != count)
{
free(rsrc_entries);
return ;
}
for(i=0, rsrc_entry=rsrc_entries; i<count; i++, rsrc_entry++)
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)rsrc_entries, count * sizeof(struct rsrc_entries_s));
#endif
/*@
@ loop invariant 0 <= i <= count;
@ loop variant count - i;
@*/
for(i=0; i<count; i++)
{
const unsigned int rsrcType_new=(level==0?le32(rsrc_entry->Type):rsrcType);
const struct rsrc_entries_s *rsrc_entry=&rsrc_entries[i];
#ifdef DEBUG_EXE
log_info("ressource %u, %x, offset %u\n",
rsrcType_new,
log_info("resource lang=%u, %x, offset %u\n",
le32(rsrc_entry->Type),
le32(rsrc_entry->Pos),
base + (le32(rsrc_entry->Pos) & 0x7fffffff));
#endif
/* Only intersted by version resources */
if(rsrcType_new==16)
{
if((le32(rsrc_entry->Pos) & 0x80000000)!=0)
{
file_exe_ressource(file,
base,
le32(rsrc_entry->Pos) & 0x7fffffff,
size,
(level==0?le32(rsrc_entry->Type):rsrcType),
level + 1,
pe_sections, nbr_sections, file_recovery);
}
if(level==2)
{
unsigned int off;
struct rsrc_offlen buffer;
uint64_t off;
unsigned int len;
unsigned int j;
if(fseek(file, base + (le32(rsrc_entry->Pos) & 0x7fffffff), SEEK_SET)<0)
{
free(rsrc_entries);
return ;
}
buffer_size=fread(buffer, 1, sizeof(buffer), file);
if(buffer_size<16)
if(fread(&buffer, 1, sizeof(buffer), file) != sizeof(buffer))
{
free(rsrc_entries);
return ;
}
off=buffer[0]+ (buffer[1]<<8) + (buffer[2]<<16) + (buffer[3]<<24);
len=buffer[4]+ (buffer[5]<<8) + (buffer[6]<<16) + (buffer[7]<<24);
{
const struct pe_image_section_hdr *pe_section;
for(i=0, pe_section=pe_sections; i<nbr_sections; i++,pe_section++)
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)&buffer, sizeof(buffer));
#endif
off=le32(buffer.off);
len=le32(buffer.len);
/*TODO: loop invariant 0 <= j <= nbr_sections; */
for(j=0; j<nbr_sections; j++)
{
const struct pe_image_section_hdr *pe_section=&pe_sections[j];
if(le32(pe_section->VirtualAddress) <= off
&& off < le32(pe_section->VirtualAddress) + le32(pe_section->SizeOfRawData))
&& off < (uint64_t)le32(pe_section->VirtualAddress) + le32(pe_section->SizeOfRawData))
{
PEVersion(file, off - le32(pe_section->VirtualAddress) + base, len, file_recovery);
free(rsrc_entries);
return ;
}
}
}
free(rsrc_entries);
return ;
}
}
free(rsrc_entries);
}
/*@
@ requires \valid(file);
@ requires base <= 0x7fffffff;
@ requires dir_start <= 0x7fffffff;
@ requires \valid_read(pe_sections);
@ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename);
@*/
static void pe_resource_id(FILE *file, const unsigned int base, const unsigned int dir_start, const struct pe_image_section_hdr *pe_sections, const unsigned int nbr_sections, file_recovery_t *file_recovery)
{
struct rsrc_entries_s *rsrc_entries;
unsigned int count;
unsigned int i;
#ifdef DEBUG_EXE
log_info("pe_resource_id(file, %u, %u)\n", base, dir_start);
#endif
{
unsigned char buffer[16];
unsigned int nameEntries;
unsigned int idEntries;
if(fseek(file, base + dir_start, SEEK_SET)<0)
return ;
if(fread(buffer, 1, sizeof(buffer), file) != sizeof(buffer))
return ;
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)buffer, sizeof(buffer));
#endif
nameEntries = buffer[12]+(buffer[13]<<8);
idEntries = buffer[14]+(buffer[15]<<8);
count = nameEntries + idEntries;
}
if(count==0 || count > 1024)
return ;
/*@ assert 0 < count <= 1024; */
#ifdef __FRAMAC__
rsrc_entries=(struct rsrc_entries_s *)MALLOC(1024 * sizeof(struct rsrc_entries_s));
#else
rsrc_entries=(struct rsrc_entries_s *)MALLOC(count * sizeof(struct rsrc_entries_s));
#endif
/*@ assert \valid((char *)rsrc_entries + (0 .. (unsigned long)((unsigned long)count * sizeof(struct rsrc_entries_s)) - 1)); */
if(fread(rsrc_entries, sizeof(struct rsrc_entries_s), count, file) != count)
{
free(rsrc_entries);
return ;
}
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)rsrc_entries, count * sizeof(struct rsrc_entries_s));
#endif
for(i=0; i<count; i++)
{
const struct rsrc_entries_s *rsrc_entry=&rsrc_entries[i];
#ifdef DEBUG_EXE
log_info("resource id=%u, %x, offset %u\n",
le32(rsrc_entry->Type),
le32(rsrc_entry->Pos),
base + (le32(rsrc_entry->Pos) & 0x7fffffff));
#endif
if((le32(rsrc_entry->Pos) & 0x80000000)!=0)
{
pe_resource_language(file,
base,
le32(rsrc_entry->Pos) & 0x7fffffff,
pe_sections, nbr_sections, file_recovery);
}
}
free(rsrc_entries);
}
/*@
@ requires \valid(file);
@ requires \valid_read(pe_sections);
@ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename);
@*/
static void pe_resource_type(FILE *file, const unsigned int base, const unsigned int dir_start, const struct pe_image_section_hdr *pe_sections, const unsigned int nbr_sections, file_recovery_t *file_recovery)
{
struct rsrc_entries_s *rsrc_entries;
unsigned int count;
unsigned int i;
#ifdef DEBUG_EXE
log_info("pe_resource_type(file, %u, %u)\n", base, dir_start);
#endif
/* TODO: remove these artifical limits ? */
if(base > 0x7fffffff || dir_start > 0x7fffffff)
return ;
/*@ assert base <= 0x7fffffff; */
{
unsigned char buffer[16];
unsigned int nameEntries;
unsigned int idEntries;
if(fseek(file, base, SEEK_SET)<0)
return ;
if(fread(buffer, 1, sizeof(buffer), file) != sizeof(buffer))
return ;
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)buffer, sizeof(buffer));
#endif
nameEntries = buffer[12]+(buffer[13]<<8);
idEntries = buffer[14]+(buffer[15]<<8);
count = nameEntries + idEntries;
}
if(count==0 || count > 1024)
return ;
/*@ assert 0 < count <= 1024; */
#ifdef __FRAMAC__
rsrc_entries=(struct rsrc_entries_s *)MALLOC(1024 * sizeof(struct rsrc_entries_s));
#else
rsrc_entries=(struct rsrc_entries_s *)MALLOC(count * sizeof(struct rsrc_entries_s));
#endif
/*@ assert \valid((char *)rsrc_entries + (0 .. (unsigned long)((unsigned long)count * sizeof(struct rsrc_entries_s)) - 1)); */
if(fread(rsrc_entries, sizeof(struct rsrc_entries_s), count, file) != count)
{
free(rsrc_entries);
return ;
}
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)rsrc_entries, count * sizeof(struct rsrc_entries_s));
#endif
for(i=0; i<count; i++)
{
const struct rsrc_entries_s *rsrc_entry=&rsrc_entries[i];
const unsigned int rsrcType=le32(rsrc_entry->Type);
#ifdef DEBUG_EXE
log_info("resource type=%u, %x, offset %u\n",
rsrcType,
le32(rsrc_entry->Pos),
base + (le32(rsrc_entry->Pos) & 0x7fffffff));
#endif
/* https://docs.microsoft.com/en-us/windows/win32/menurc/resource-types
* RT_CURSOR=1, RT_ICON=3, RT_VERSION=16 */
/* Only interested by version resources */
if(rsrcType==16)
{
if((le32(rsrc_entry->Pos) & 0x80000000)!=0)
{
pe_resource_id(file,
base,
le32(rsrc_entry->Pos) & 0x7fffffff,
pe_sections, nbr_sections, file_recovery);
}
}
}
free(rsrc_entries);
}
/*@
@ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename);
@*/
static void file_rename_pe_exe(file_recovery_t *file_recovery)
{
unsigned char buffer[4096];
FILE *file;
int buffer_size;
const struct dos_image_file_hdr *dos_hdr=(const struct dos_image_file_hdr*)buffer;
const struct dos_image_file_hdr *dos_hdr;
const struct pe_image_file_hdr *pe_hdr;
unsigned int e_lfanew;
if((file=fopen(file_recovery->filename, "rb"))==NULL)
return;
buffer_size=fread(buffer, 1, sizeof(buffer), file);
/*@ assert buffer_size <= sizeof(buffer); */
if(buffer_size < (int)sizeof(struct dos_image_file_hdr))
{
fclose(file);
return ;
}
/*@ assert buffer_size >= sizeof(struct dos_image_file_hdr); */
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)buffer, sizeof(buffer));
#endif
if(memcmp(buffer,exe_header,sizeof(exe_header))!=0)
{
fclose(file);
return ;
}
if((unsigned int)buffer_size < le32(dos_hdr->e_lfanew)+sizeof(struct pe_image_file_hdr))
dos_hdr=(const struct dos_image_file_hdr*)buffer;
e_lfanew=le32(dos_hdr->e_lfanew);
if((unsigned int)buffer_size < e_lfanew+sizeof(struct pe_image_file_hdr))
{
fclose(file);
return ;
}
pe_hdr=(const struct pe_image_file_hdr *)(buffer+le32(dos_hdr->e_lfanew));
if(le32(dos_hdr->e_lfanew)==0 ||
le32(dos_hdr->e_lfanew) > buffer_size-sizeof(struct pe_image_file_hdr) ||
le32(pe_hdr->Magic) != IMAGE_NT_SIGNATURE)
if(e_lfanew==0 ||
e_lfanew > buffer_size-sizeof(struct pe_image_file_hdr))
{
fclose(file);
return ;
}
pe_hdr=(const struct pe_image_file_hdr *)(buffer+e_lfanew);
if(le32(pe_hdr->Magic) != IMAGE_NT_SIGNATURE)
{
fclose(file);
return ;
}
{
const uint64_t offset_sections=e_lfanew + sizeof(struct pe_image_file_hdr) + le16(pe_hdr->SizeOfOptionalHeader);
/* https://docs.microsoft.com/en-us/windows/win32/debug/pe-format
* Windows loader limits the number of sections to 96
*/
const unsigned int nbr_sections=(le16(pe_hdr->NumberOfSections) < 96?le16(pe_hdr->NumberOfSections) : 96);
struct pe_image_section_hdr pe_sections[96];
unsigned int i;
const struct pe_image_section_hdr *pe_sections;
const struct pe_image_section_hdr *pe_section;
unsigned int nbr_sections;
pe_sections=(const struct pe_image_section_hdr*)
((const unsigned char*)pe_hdr + sizeof(struct pe_image_file_hdr) + le16(pe_hdr->SizeOfOptionalHeader));
for(i=0, pe_section=pe_sections;
i<le16(pe_hdr->NumberOfSections) && (const unsigned char*)pe_section < buffer+buffer_size;
i++, pe_section++)
if(nbr_sections == 0)
{
fclose(file);
return ;
}
/*@ assert 0 < nbr_sections <= 96; */
if(fseek(file, offset_sections, SEEK_SET)<0)
{
fclose(file);
return ;
}
if(fread(pe_sections, sizeof(struct pe_image_section_hdr), nbr_sections, file) != nbr_sections)
{
fclose(file);
return ;
}
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)pe_sections, sizeof(pe_sections));
#endif
#ifdef DEBUG_EXE
if(le32(pe_section->SizeOfRawData)>0)
/*@
@ loop invariant 0 <= i <= nbr_sections;
@*/
for(i=0; i<nbr_sections; i++)
{
const struct pe_image_section_hdr *pe_section=&pe_sections[i];
/*@ assert \valid_read(pe_section); */
if(le32(pe_section->VirtualSize)>0)
{
log_info("%s 0x%lx-0x%lx\n", pe_section->Name,
(unsigned long)le32(pe_section->VirtualAddress),
(unsigned long)le32(pe_section->VirtualAddress)+le32(pe_section->VirtualSize)-1);
}
#endif
}
nbr_sections=i;
for(i=0, pe_section=pe_sections;
i<le16(pe_hdr->NumberOfSections) && (const unsigned char*)pe_section < buffer+buffer_size;
i++, pe_section++)
#endif
/*@
@ loop invariant 0 <= i <= nbr_sections;
@*/
for(i=0; i<nbr_sections; i++)
{
const struct pe_image_section_hdr *pe_section=&pe_sections[i];
/*@ assert \valid_read(pe_section); */
if(le32(pe_section->SizeOfRawData)>0)
{
if(memcmp((const char*)pe_section->Name, ".rsrc", 6)==0)
{
file_exe_ressource(file,
pe_resource_type(file,
le32(pe_section->PointerToRawData),
0,
le32(pe_section->SizeOfRawData),
0,
0,
pe_sections, nbr_sections, file_recovery);
fclose(file);
return;
@ -521,3 +872,87 @@ static void register_header_check_exe(file_stat_t *file_stat)
{
register_header_check(0, exe_header,sizeof(exe_header), &header_check_exe, file_stat);
}
#if defined(MAIN_exe)
#define BLOCKSIZE 65536u
int main()
{
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_exe;
file_stats.not_recovered=0;
file_stats.recovered=0;
file_hint_exe.register_header_check(&file_stats);
if(header_check_exe(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
return 0;
strcpy(file_recovery_new.filename, "recup_dir.1/f0000000.exe");
/*@ assert file_recovery_new.file_size == 0; */
/*@ assert file_recovery_new.extension == file_hint_exe.extension || file_recovery_new.extension == extension_dll; */
file_recovery_new.file_stat=&file_stats;
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);
}
}
if(file_recovery_new.file_stat!=NULL)
{
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 */
header_check_exe(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
}
if(file_recovery_new.file_check!=NULL)
{
file_recovery_new.handle=fopen("demo", "rb");
if(file_recovery_new.handle!=NULL)
{
(file_recovery_new.file_check)(&file_recovery_new);
fclose(file_recovery_new.handle);
}
}
if(file_recovery_new.file_rename!=NULL)
{
/*@ assert valid_read_string((char *)&file_recovery_new.filename); */
(file_recovery_new.file_rename)(&file_recovery_new);
}
return 0;
}
#endif