summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-06-18 18:54:35 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2020-06-18 18:54:35 +0200
commitdf92a1f0ef118f8ae1ed14f899db4206b9e6bb8f (patch)
tree67a065526b95dc1867656bcc8f227cbee97927bd
parentefd46ac6da9299b955ddd99acb292328411b19ee (diff)
src/file_swf.c: add frama-c annotations
-rw-r--r--src/file_swf.c181
1 files changed, 179 insertions, 2 deletions
diff --git a/src/file_swf.c b/src/file_swf.c
index a098215..17d743a 100644
--- a/src/file_swf.c
+++ b/src/file_swf.c
@@ -19,10 +19,15 @@
Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*/
-
#ifdef HAVE_CONFIG_H
#include <config.h>
#endif
+
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_ZLIB_H
+#undef HAVE_LIBZ
+#endif
+
#ifdef HAVE_STRING_H
#include <string.h>
#endif
@@ -33,7 +38,11 @@
#endif
#include "filegen.h"
#include "common.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
+static const char *extension_swc="swc";
static void register_header_check_swf(file_stat_t *file_stat);
const file_hint_t file_hint_swf= {
@@ -66,18 +75,36 @@ struct swfz_header
// compressedLen does not include header (4+4+4 bytes) or lzma props (5 bytes)
// compressedLen does include LZMA end marker (6 bytes)
+/*@
+ @ requires \valid(data);
+ @ requires \valid_read(*data + (0..3));
+ @ requires \valid(offset_bit);
+ @ requires 0 <= *offset_bit <= 7;
+ @ requires 2 <= nbit <= 31;
+ @ requires separation: \separated(data, offset_bit, *data + (0..(nbit+*offset_bit)/8));
+ @ ensures 0 <= *offset_bit <= 7;
+ @ assigns *data, *offset_bit;
+ @*/
static int read_SB(const unsigned char **data, unsigned int *offset_bit, unsigned int nbit)
{
int res=0;
const unsigned int sign=((**data) >>(7 - (*offset_bit)))&1;
+ /*@
+ loop unroll 31;
+ loop assigns nbit, *offset_bit, *data, res;
+ loop variant nbit;
+ */
while(nbit>1)
{
+ /*@ assert 0 <= *offset_bit <= 7; */
(*offset_bit)++;
+ /*@ assert 1 <= *offset_bit <= 8; */
if(*offset_bit==8)
{
(*data)++;
*offset_bit=0;
}
+ /*@ assert 0 <= *offset_bit <= 7; */
res=(res<<1)|((**data>>(7 - *offset_bit))&1);
nbit--;
}
@@ -86,6 +113,24 @@ static int read_SB(const unsigned char **data, unsigned int *offset_bit, unsigne
return res;
}
+/*@
+ @ requires buffer_size >= 512;
+ @ 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_swf, 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->data_check == &data_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size_max);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == extension_swc);
+ @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
+ @*/
static int header_check_swfc(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 swf_header *hdr=(const struct swf_header *)buffer;
@@ -138,8 +183,10 @@ static int header_check_swfc(const unsigned char *buffer, const unsigned int buf
if(d_stream.total_out < 16)
return 0;
nbit=(*data)>>3;
+ /* assert nbit <= 31; */
if(nbit<=1)
return 0;
+ /* assert 2 <= nbit <= 31; */
Xmin=read_SB(&data, &offset_bit, nbit);
Xmax=read_SB(&data, &offset_bit, nbit);
Ymin=read_SB(&data, &offset_bit, nbit);
@@ -149,13 +196,31 @@ static int header_check_swfc(const unsigned char *buffer, const unsigned int buf
}
#endif
reset_file_recovery(file_recovery_new);
- file_recovery_new->extension="swc";
+ file_recovery_new->extension=extension_swc;
file_recovery_new->calculated_file_size=le32(hdr->size);
file_recovery_new->data_check=&data_check_size;
file_recovery_new->file_check=&file_check_size_max;
return 1;
}
+/*@
+ @ requires buffer_size >= sizeof(struct swf_header);
+ @ 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_swf, 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->data_check == &data_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_swf.extension);
+ @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
+ @*/
static int header_check_swf(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)
{
/* http://www.adobe.com/go/swfspec */
@@ -189,6 +254,24 @@ static int header_check_swf(const unsigned char *buffer, const unsigned int buff
return 1;
}
+/*@
+ @ requires buffer_size >= sizeof(struct swfz_header);
+ @ 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_swf, 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->data_check == &data_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size_max);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_swf.extension);
+ @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
+ @*/
static int header_check_swfz(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 swfz_header *hdr=(const struct swfz_header *)buffer;
@@ -204,9 +287,103 @@ static int header_check_swfz(const unsigned char *buffer, const unsigned int buf
return 1;
}
+/*@
+ @ requires \valid(file_stat);
+ @*/
static void register_header_check_swf(file_stat_t *file_stat)
{
register_header_check(0, "CWS", 3, &header_check_swfc, file_stat);
register_header_check(0, "FWS", 3, &header_check_swf, file_stat);
register_header_check(0, "ZWS", 3, &header_check_swfz, file_stat);
}
+
+#if defined(MAIN_swf)
+#define BLOCKSIZE 65536u
+int main(void)
+{
+ const char fn[] = "recup_dir.1/f0000000.swf";
+ 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_swf;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+ register_header_check_swf(&file_stats);
+ if(header_check_swf(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1 ||
+ header_check_swfc(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1 ||
+ header_check_swfz(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_swf.extension || file_recovery_new.extension == extension_swc; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.file_check == &file_check_size || file_recovery_new.file_check == &file_check_size_max; */
+ /*@ assert file_recovery_new.data_check == &data_check_size; */
+ /*@ assert file_recovery_new.file_stat->file_hint!=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; */;
+ /*@ 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_swf(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 || file_recovery_new.file_check == &file_check_size_max; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ if(file_recovery_new.file_check == &file_check_size)
+ file_check_size(&file_recovery_new);
+ else
+ file_check_size_max(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+#endif