summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-09-10 17:15:12 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2020-09-10 17:15:12 +0200
commit4ba942d12e7094004074b6808f2532b8f877019e (patch)
tree8964510d607ad54e6bdb1f88314a2bc63bb69d10
parente07e4692d578783cc78c4ea52138930b8084a961 (diff)
src/file_ace.c: add frama-c annotations
-rw-r--r--src/file_ace.c130
1 files changed, 98 insertions, 32 deletions
diff --git a/src/file_ace.c b/src/file_ace.c
index 582e6ca..372af29 100644
--- a/src/file_ace.c
+++ b/src/file_ace.c
@@ -20,6 +20,7 @@
*/
+#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_ace)
#ifdef HAVE_CONFIG_H
#include <config.h>
#endif
@@ -32,9 +33,15 @@
#include "common.h"
#include "log.h"
#include "crc.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
/* #define DEBUG_ACE */
+/*@
+ @ requires \valid(file_stat);
+ @*/
static void register_header_check_ace(file_stat_t *file_stat);
const file_hint_t file_hint_ace= {
@@ -61,34 +68,62 @@ struct header_ace {
typedef struct header_ace ace_header_t;
#define BUF_SIZE 4096
+/*@
+ @ requires \valid(handle);
+ @ requires \separated(handle, &errno, &Frama_C_entropy_source);
+ @ assigns *handle, errno;
+ @ assigns Frama_C_entropy_source;
+ @*/
static int check_ace_crc(FILE *handle, const unsigned int len, const unsigned int crc32_low)
{
- unsigned char buffer[BUF_SIZE];
+ char buffer[BUF_SIZE];
uint32_t crc32=0xFFFFFFFF;
unsigned int remaining=len;
+ /*@
+ @ loop assigns *handle, errno;
+ @ loop assigns Frama_C_entropy_source;
+ @ loop assigns buffer[0 .. BUF_SIZE-1], crc32, remaining;
+ @*/
while (remaining>0)
{
const unsigned int count = ((remaining>BUF_SIZE) ? BUF_SIZE : remaining);
if(fread(buffer, 1, count, handle) != count)
{
#ifdef DEBUG_ACE
- log_trace("file_ace: truncated file\n");
+ log_info("file_ace: truncated file\n");
#endif
return 1;
}
+#ifdef __FRAMAC__
+ Frama_C_make_unknown(&buffer, sizeof(buffer));
+#endif
crc32=get_crc32(buffer, count, crc32);
remaining -= count;
}
if (crc32_low != (crc32&0xFFFF))
{
#ifdef DEBUG_ACE
- log_trace("file_ace: bad CRC: %04X vs %04X\n", crc32_low, crc32&0xFFFF);
+ log_info("file_ace: bad CRC: %04X vs %04X\n", crc32_low, crc32&0xFFFF);
#endif
return 1;
}
return 0;
}
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires \valid_read(&file_recovery->extension);
+ @ requires valid_read_string(file_recovery->extension);
+ @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
+ @ requires \initialized(&file_recovery->time);
+ @
+ @ requires file_recovery->file_check == &file_check_ace;
+ @ assigns *file_recovery->handle, errno, file_recovery->file_size, file_recovery->offset_error, file_recovery->offset_ok;
+ @ assigns Frama_C_entropy_source;
+ @
+ @ ensures \valid(file_recovery->handle);
+ @*/
static void file_check_ace(file_recovery_t *file_recovery)
{
file_recovery->offset_error = 0;
@@ -96,58 +131,52 @@ static void file_check_ace(file_recovery_t *file_recovery)
file_recovery->file_size = 0;
if(my_fseek(file_recovery->handle, 0, SEEK_SET)<0)
return ;
-#ifdef DEBUG_ACE
- log_trace("file_check_ace\n");
-#endif
+ /*@
+ @ loop assigns *file_recovery->handle, errno, file_recovery->file_size, file_recovery->offset_error;
+ @ loop assigns Frama_C_entropy_source;
+ @*/
while (!feof(file_recovery->handle))
{
- ace_header_t h;
- size_t res;
- memset(&h, 0, sizeof(h));
- res=fread(&h, 1, sizeof(h), file_recovery->handle);
- if(res==0)
- return ;
- if(res != sizeof(h))
+ char buffer[sizeof(ace_header_t)];
+ const ace_header_t *h=(const ace_header_t *)&buffer;
+ if(fread(&buffer, sizeof(buffer), 1, file_recovery->handle)!= 1)
{
- file_recovery->offset_error=file_recovery->file_size;
- file_recovery->file_size=0;
return ;
}
+#ifdef __FRAMAC__
+ Frama_C_make_unknown(&buffer, sizeof(buffer));
+#endif
#ifdef DEBUG_ACE
- log_trace("file_ace: Block header at 0x%08lx: CRC16=0x%04X size=%u type=%u"
+ log_info("file_ace: Block header at 0x%08lx: CRC16=0x%04X size=%u type=%u"
" flags=0x%04X addsize=%u\n",
(long unsigned) file_recovery->file_size,
- le16(h.crc16), le16(h.size), h.type, le16(h.flags),
- (le16(h.flags)&1) ? le32(h.addsize):0);
+ le16(h->crc16), le16(h->size), h->type, le16(h->flags),
+ (le16(h->flags)&1) ? le32(h->addsize):0);
#endif
/* Type 0=Archive header, 1=File block, 2=Recovery Record, 5 new_recovery ? */
- if (h.type==0 && le16(h.size)==0)
+ if (h->type==0 && le16(h->size)==0)
{
return ;
}
- if (h.type!=0 && h.type!=1 && h.type!=2 && h.type!=5)
+ if (h->type!=0 && h->type!=1 && h->type!=2 && h->type!=5)
{
#ifdef DEBUG_ACE
- log_trace("file_ace: Invalid block type %u\n", h.type);
+ log_info("file_ace: Invalid block type %u\n", h->type);
#endif
- file_recovery->offset_error=file_recovery->file_size;
- file_recovery->file_size=0;
return ;
}
/* Minimal size is type+flags */
- if (le16(h.size) < 1U + 2U)
+ if (le16(h->size) < 1U + 2U)
{
#ifdef DEBUG_ACE
- log_trace("file_ace: Invalid block size %u\n", le16(h.size));
+ log_info("file_ace: Invalid block size %u\n", le16(h->size));
#endif
- file_recovery->offset_error=file_recovery->file_size;
- file_recovery->file_size=0;
return ;
}
- if(my_fseek(file_recovery->handle, -sizeof(h)+4, SEEK_CUR)<0 ||
- check_ace_crc(file_recovery->handle, le16(h.size), le16(h.crc16)) != 0)
+ if(my_fseek(file_recovery->handle, -(off_t)sizeof(h)+(off_t)4, SEEK_CUR)<0 ||
+ check_ace_crc(file_recovery->handle, le16(h->size), le16(h->crc16)) != 0)
{
file_recovery->offset_error=file_recovery->file_size;
file_recovery->file_size=0;
@@ -155,11 +184,17 @@ static void file_check_ace(file_recovery_t *file_recovery)
}
/* Add its header size */
- file_recovery->file_size += (uint64_t)4 + le16(h.size); /* +2: CRC16, +2: size */
+ file_recovery->file_size += (uint64_t)4 + le16(h->size); /* +2: CRC16, +2: size */
+
+ if(file_recovery->file_size >= 0x8000000000000000-0x100000000)
+ {
+ file_recovery->file_size=0;
+ return ;
+ }
/* If addsize flag, add complementary size */
- if (le16(h.flags)&1)
+ if (le16(h->flags)&1)
{
- file_recovery->file_size += le32(h.addsize);
+ file_recovery->file_size += le32(h->addsize);
if(my_fseek(file_recovery->handle, file_recovery->file_size, SEEK_SET)<0)
{
file_recovery->offset_error=file_recovery->file_size;
@@ -170,6 +205,36 @@ static void file_check_ace(file_recovery_t *file_recovery)
}
}
+/*@
+ @ requires buffer_size > 0;
+ @ 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 buffer_size >= sizeof(ace_header_t);
+ @ requires separation: \separated(&file_hint_ace, 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) ==> \initialized(&file_recovery_new->time);
+ @ ensures (\result == 1) ==> \initialized(&file_recovery_new->calculated_file_size);
+ @ ensures (\result == 1) ==> file_recovery_new->file_size == 0;
+ @ ensures (\result == 1) ==> \initialized(&file_recovery_new->min_filesize);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null || \valid_function(file_recovery_new->data_check));
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == \null || \valid_function(file_recovery_new->file_check));
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null || \valid_function(file_recovery_new->file_rename));
+ @ ensures (\result != 0) ==> file_recovery_new->extension != \null;
+ @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
+ @
+ @ ensures (\result == 1) ==> (file_recovery_new->time == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_ace.extension);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_ace);
+ @*/
static int header_check_ace(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 ace_header_t *h=(const ace_header_t *)buffer;
@@ -193,3 +258,4 @@ static void register_header_check_ace(file_stat_t *file_stat)
static const unsigned char ace_header[7] = { '*','*','A','C','E','*','*'};
register_header_check(7, ace_header,sizeof(ace_header), &header_check_ace, file_stat);
}
+#endif