summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-12-07 20:30:40 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2019-12-07 20:30:40 +0100
commit1f77cbec99dcfe25d7a1d951fed82f5344d95de7 (patch)
treeef7a4896eab5eb4f37b34154c78e262e6c2a8caf
parent410c20224cedb38a3fbae66cd1188e02bd168829 (diff)
src/file_spe.c: check using frama-c
-rw-r--r--src/file_spe.c174
1 files changed, 158 insertions, 16 deletions
diff --git a/src/file_spe.c b/src/file_spe.c
index 9130cf1..d276953 100644
--- a/src/file_spe.c
+++ b/src/file_spe.c
@@ -31,6 +31,9 @@
#include "filegen.h"
#include "common.h"
#include "log.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
static void register_header_check_spe(file_stat_t *file_stat);
static int header_check_spe(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);
@@ -237,30 +240,169 @@ struct header_spe
int16_t lastvalue; /* 4098 Always the LAST value in the header */
} __attribute__ ((gcc_struct, __packed__));
-static const unsigned char spe_header[4]= {0x67, 0x45, 0x23, 0x01};
+/*@
+ @ 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;
+ @ requires separation: \separated(&file_hint_spe, buffer+(..), file_recovery, file_recovery_new);
+ @ 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) ==> (file_recovery_new->extension == file_hint_spe.extension);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= 4100);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 4100);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
+ @ assigns file_recovery_new->filename[0];
+ @ assigns file_recovery_new->time;
+ @ assigns file_recovery_new->file_stat;
+ @ assigns file_recovery_new->handle;
+ @ assigns file_recovery_new->file_size;
+ @ assigns file_recovery_new->location.list.prev;
+ @ assigns file_recovery_new->location.list.next;
+ @ assigns file_recovery_new->location.end;
+ @ assigns file_recovery_new->location.data;
+ @ assigns file_recovery_new->extension;
+ @ assigns file_recovery_new->min_filesize;
+ @ assigns file_recovery_new->calculated_file_size;
+ @ assigns file_recovery_new->data_check;
+ @ assigns file_recovery_new->file_check;
+ @ assigns file_recovery_new->file_rename;
+ @ assigns file_recovery_new->offset_error;
+ @ assigns file_recovery_new->offset_ok;
+ @ assigns file_recovery_new->checkpoint_status;
+ @ assigns file_recovery_new->checkpoint_offset;
+ @ assigns file_recovery_new->flags;
+ @ assigns file_recovery_new->extra;
+ @*/
+static int header_check_spe(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 tmp;
+ const struct header_spe *spe;
+ if(buffer_size < 4100)
+ return 0;
+ /*@ assert buffer_size >= 4100; */
+ spe=(const struct header_spe*)buffer;
+ /*@ assert \valid_read(spe); */
+ if(le32(spe->WinView_id)!=0x01234567L || le16(spe->lastvalue)!=0x5555 || le32(spe->NumFrames)<0)
+ return 0;
+ tmp=(uint64_t)le16(spe->xdim)*le16(spe->ydim)*le32(spe->NumFrames);
+ if((tmp&0xc000000000000000)!=0)
+ return 0;
+ tmp*=(le16(spe->datatype)<=1?4:2);
+ if((tmp&0x8000000000000000)!=0)
+ return 0;
+ tmp+=4100;
+
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->extension=file_hint_spe.extension;
+ file_recovery_new->min_filesize=4100;
+ file_recovery_new->calculated_file_size=tmp;
+#ifndef __FRAMAC__
+ log_debug("spe xdim=%u ydim=%u NumFrames=%u datatype=%u size=%llu\n",
+ le16(spe->xdim), le16(spe->ydim), (unsigned int)le32(spe->NumFrames), le16(spe->datatype),
+ (long long unsigned) file_recovery_new->calculated_file_size);
+#endif
+ file_recovery_new->data_check=&data_check_size;
+ file_recovery_new->file_check=&file_check_size;
+ return 1;
+}
static void register_header_check_spe(file_stat_t *file_stat)
{
+ static const unsigned char spe_header[4]= {0x67, 0x45, 0x23, 0x01};
register_header_check(0xbb4, spe_header,sizeof(spe_header), &header_check_spe, file_stat);
}
-static int header_check_spe(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 defined(MAIN_spe)
+#define BLOCKSIZE 65536u
+int main()
{
- const struct header_spe *spe=(const struct header_spe*)buffer;
- if(le32(spe->WinView_id)==0x01234567L && le16(spe->lastvalue)==0x5555)
+ const char fn[] = "recup_dir.1/f0000000.spe";
+ 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);
+ /*@ assert file_recovery.file_stat == \null; */
+ 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_spe;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+ register_header_check_spe(&file_stats);
+ if(header_check_spe(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ assert valid_read_string((char *)&fn); */
+ memcpy(file_recovery_new.filename, fn, sizeof(fn));
+ file_recovery_new.file_stat=&file_stats;
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ /*@ assert file_recovery_new.extension == file_hint_spe.extension; */
+ /*@ assert file_recovery_new.calculated_file_size >= 4100; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.min_filesize == 4100; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.data_check == &data_check_size; */
+ /*@ assert file_recovery_new.file_stat->file_hint!=NULL; */
{
- reset_file_recovery(file_recovery_new);
- file_recovery_new->extension=file_hint_spe.extension;
- file_recovery_new->min_filesize=4100;
- file_recovery_new->calculated_file_size=(uint64_t)le16(spe->xdim)*le16(spe->ydim)*le32(spe->NumFrames);
- file_recovery_new->calculated_file_size*=(le16(spe->datatype)<=1?4:2);
- file_recovery_new->calculated_file_size+=4100;
- log_debug("spe xdim=%u ydim=%u NumFrames=%u datatype=%u size=%llu\n",
- le16(spe->xdim), le16(spe->ydim), (unsigned int)le32(spe->NumFrames), le16(spe->datatype),
- (long long unsigned) file_recovery_new->calculated_file_size);
- file_recovery_new->data_check=&data_check_size;
- file_recovery_new->file_check=&file_check_size;
- return 1;
+ 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; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ 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;
+ 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_spe(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ 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);
}
return 0;
}
+#endif