summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-09-26 20:38:23 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2019-09-26 20:38:23 +0200
commit806a1f4bb565166392269d5c20254971d2d47775 (patch)
tree99a9ea35bde21fbd50f01d2b426ab574ded6cfb7
parent0f09fa0121746225324e1a5ed70f5705bc1b6042 (diff)
PhotoRec: exe - rewrite the resource parser.
-rw-r--r--src/file_exe.c807
1 files changed, 621 insertions, 186 deletions
diff --git a/src/file_exe.c b/src/file_exe.c
index 12f1400..e0e6386 100644
--- a/src/file_exe.c
+++ b/src/file_exe.c
@@ -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,23 +106,27 @@ 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(le16(pe_image_optional32->Magic)==IMAGE_NT_OPTIONAL_HDR_MAGIC)
- {
- log_debug("SizeOfCode %lx\n", (long unsigned)le32(pe_image_optional32->SizeOfCode));
- log_debug("SizeOfImage %lx\n", (long unsigned)le32(pe_image_optional32->SizeOfImage));
- }
- else if(le16(pe_image_optional32->Magic)==IMAGE_NT_OPTIONAL_HDR64_MAGIC)
+ if((const unsigned char*)(pe_image_optional32+1) <= buffer+buffer_size)
{
- const struct pe_image_optional_hdr64 *pe_image_optional64=(const struct pe_image_optional_hdr64 *)
- (((const unsigned char*)pe_hdr + sizeof(struct pe_image_file_hdr)));
+ /*@ 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));
+ log_debug("SizeOfImage %lx\n", (long unsigned)le32(pe_image_optional32->SizeOfImage));
+ }
+ else if(le16(pe_image_optional32->Magic)==IMAGE_NT_OPTIONAL_HDR64_MAGIC)
+ {
+ const struct pe_image_optional_hdr64 *pe_image_optional64=(const struct pe_image_optional_hdr64 *)
+ (((const unsigned char*)pe_hdr + sizeof(struct pe_image_file_hdr)));
+ }
+ 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));
}
- 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,23 +201,36 @@ 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)
{
- log_info("offset %x, segment %x\n",
- le16(exe_reloc->offset), le16(exe_reloc->segment));
+ 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
@@ -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)
+/*@
+ @ 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)
{
- for(; pos+2<len && (buffer[pos]!='\0' || buffer[pos+1]!='\0'); pos+=2)
+ const struct PE_index *PE_index;
+ unsigned int len;
+ unsigned int val_len;
+ unsigned int type;
+ if(6 > end)
{
-#ifdef DEBUG_EXE
- log_info("%c", buffer[pos]);
-#endif
+ return -1;
+ }
+ 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)
+ {
+ 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;
}
- pos+=2;
+ 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;
- return pos;
+ if(pos > len)
+ return -1;
+ return parse_StringTable(file_recovery, &buffer[pos], len - pos, needle, needle_len, force_ext);
}
-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)
+/*@
+ @ 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;
- while(1)
+ const struct PE_index *PE_index;
+ const char *stringName;
+ unsigned int len;
+ unsigned int val_len;
+ if(6 > end)
{
- const struct PE_index *PE_index;
- pos=(pos + 3) & 0xfffffffc; /* align on a 4-byte boundary */
- if(pos + 6 > end)
- {
- return -1;
- }
- PE_index=(const struct PE_index*)&buffer[pos];
- if(le16(PE_index->len)==0 && le16(PE_index->val_len)==0)
- {
- return -1;
- }
- {
- 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;
- }
+ 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[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 ;
+ if(fread(&buffer, length, 1, file) != 1)
+ {
+ return ;
+ }
+#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)
+ {
+ return;
+ }
+ parse_VS_VERSIONINFO(file_recovery, buffer, length, InternalName, sizeof(InternalName), 1);
+}
+
+/*@
+ @ 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;
+ unsigned int count;
+ unsigned int i;
#ifdef DEBUG_EXE
- log_info(": ");
+ log_info("pe_resource_language(file, %u, %u)\n", base, dir_start);
#endif
- pt=ReadUnicodeStr(buffer, pt, pos);
- }
- }
+ {
+ 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;
+ }
+ 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 ;
+ }
+#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 struct rsrc_entries_s *rsrc_entry=&rsrc_entries[i];
#ifdef DEBUG_EXE
- log_info("\n");
+ log_info("resource lang=%u, %x, offset %u\n",
+ le32(rsrc_entry->Type),
+ le32(rsrc_entry->Pos),
+ base + (le32(rsrc_entry->Pos) & 0x7fffffff));
#endif
- }
+ {
+ 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 ;
}
- else
+ if(fread(&buffer, 1, sizeof(buffer), file) != sizeof(buffer))
+ {
+ free(rsrc_entries);
+ return ;
+ }
+#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++)
{
- pos+=le16(PE_index->len)+le16(PE_index->val_len);
+ const struct pe_image_section_hdr *pe_section=&pe_sections[j];
+ if(le32(pe_section->VirtualAddress) <= off
+ && 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);
}
-static void PEVersion(FILE *file, const unsigned int offset, const unsigned int length, 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_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)
{
- char *buffer;
- if(length==0 || length > 1024*1024)
- return;
- if(fseek(file, offset, SEEK_SET)<0)
+ 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 ;
- buffer=(char*)MALLOC(length);
- if(fread(buffer, length, 1, file) != 1)
+ /*@ 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(buffer);
+ free(rsrc_entries);
return ;
}
- if(PEVersion_aux(file_recovery, buffer, length, OriginalFilename, sizeof(OriginalFilename), 0)==0)
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)rsrc_entries, count * sizeof(struct rsrc_entries_s));
+#endif
+ for(i=0; i<count; i++)
{
- free(buffer);
- return;
+ 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);
+ }
}
- PEVersion_aux(file_recovery, buffer, length, InternalName, sizeof(InternalName), 1);
- free(buffer);
+ free(rsrc_entries);
}
-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 \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;
- 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_type(file, %u, %u)\n", base, dir_start);
#endif
- if(level > 2)
+ /* TODO: remove these artifical limits ? */
+ if(base > 0x7fffffff || dir_start > 0x7fffffff)
return ;
- if(fseek(file, base + dir_start, SEEK_SET)<0)
- return ;
- buffer_size=fread(buffer, 1, sizeof(buffer), file);
- if(buffer_size<16)
- return ;
- nameEntries = buffer[12]+(buffer[13]<<8);
- idEntries = buffer[14]+(buffer[15]<<8);
- count = nameEntries + idEntries;
+ /*@ 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 ;
}
- 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
+ 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];
+ const unsigned int rsrcType=le32(rsrc_entry->Type);
#ifdef DEBUG_EXE
- log_info("ressource %u, %x, offset %u\n",
- rsrcType_new,
+ log_info("resource type=%u, %x, offset %u\n",
+ rsrcType,
le32(rsrc_entry->Pos),
base + (le32(rsrc_entry->Pos) & 0x7fffffff));
#endif
- /* Only intersted by version resources */
- if(rsrcType_new==16)
+ /* 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)
{
- file_exe_ressource(file,
+ pe_resource_id(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;
- unsigned int len;
- 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)
- {
- 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(le32(pe_section->VirtualAddress) <= off
- && off < 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_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 ;
+ }
+ 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+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)
+ 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