luisgulo/testdisk
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

src/file_gpg.c: improve Frama-C annotations

Browse source
This commit is contained in:
Christophe Grenier 2021-06-15 17:08:36 +02:00
parent af8d241441
commit 385b83b52e
1 changed files with 43 additions and 49 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

92
src/file_gpg.c
View file

@ -39,7 +39,7 @@
#endif
static const char *extension_pgp="pgp";
/*@ requires \valid(file_stat); */
/*@ requires valid_register_header_check(file_stat); */
static void register_header_check_gpg(file_stat_t *file_stat);
const file_hint_t file_hint_gpg= {
@ -102,6 +102,7 @@ static unsigned int openpgp_packet_tag(const unsigned char buf)
/*@ requires \valid_read(buf+(0..5));
@ requires \valid(length_type);
@ requires \valid(indeterminate_length);
@ requires \separated(buf+(..), indeterminate_length, length_type);
@ ensures (*length_type == 1) || (*length_type == 2) || (*length_type==3)|| (*length_type==5);
@ assigns *length_type, *indeterminate_length;
*/
@ -283,6 +284,7 @@ static int is_valid_S2K(const unsigned int algo)
/*@
@ requires \valid(handle);
@ requires offset + tmp2 < 0x8000000000000000;
@ requires \separated(handle, &errno, &Frama_C_entropy_source);
@ assigns *handle, errno;
@ assigns Frama_C_entropy_source;
@*/
@ -307,13 +309,10 @@ static unsigned int file_check_gpg_pubkey(FILE *handle, const uint64_t offset, c
}
/*@
@ requires \valid(file_recovery);
@ requires \valid(file_recovery->handle);
@ requires valid_file_recovery(file_recovery);
@ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
@ requires file_recovery->file_check == &file_check_gpg;
@ ensures \valid(file_recovery->handle);
@ ensures valid_file_recovery(file_recovery);
@ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
@ requires valid_file_check_param(file_recovery);
@ ensures valid_file_check_result(file_recovery);
@ assigns *file_recovery->handle, errno, file_recovery->file_size;
@ assigns Frama_C_entropy_source;
@*/
@ -328,12 +327,15 @@ static void file_check_gpg(file_recovery_t *file_recovery)
file_recovery->file_size=0;
/*@
@ loop invariant \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
@ loop invariant valid_file_recovery(file_recovery);
@ loop assigns *file_recovery->handle, errno, file_recovery->file_size;
@ loop assigns Frama_C_entropy_source;
@ loop assigns tag, nbr, partial_body_length, stop, offset;
@*/
while(stop==0)
{
unsigned char buffer[32];
char sbuffer[32];
const unsigned char *buffer=(const unsigned char *)&sbuffer;
unsigned int i=0;
unsigned int length_type=0;
unsigned int length;
@ -342,16 +344,15 @@ static void file_check_gpg(file_recovery_t *file_recovery)
return;
/*@ assert offset < 0x7000000000000000; */
if(my_fseek(file_recovery->handle, offset, SEEK_SET) < 0 ||
fread(&buffer, sizeof(buffer), 1, file_recovery->handle) != 1)
fread(&sbuffer, sizeof(sbuffer), 1, file_recovery->handle) != 1)
{
if(nbr>=2 && offset <= org_file_size)
file_recovery->file_size=org_file_size;
return;
}
#ifdef __FRAMAC__
Frama_C_make_unknown((char *)&buffer, sizeof(buffer));
Frama_C_make_unknown(&sbuffer, sizeof(sbuffer));
#endif
if(partial_body_length==0)
{
if((buffer[0]&0x80)==0)
@ -389,9 +390,12 @@ static void file_check_gpg(file_recovery_t *file_recovery)
i+=length_type;
/*@ assert 0 < i <= 6; */
offset+=length_type;
if(offset >= 0x7000000000000000 || offset + length >= 0x7000000000000000)
if(offset >= 0x7000000000000000)
return ;
/*@ assert offset < 0x7000000000000000; */
/*@ assert length < 0x7000000000000000; */
if(offset + length >= 0x7000000000000000)
return ;
/*@ assert offset + length < 0x7000000000000000; */
if(old_partial_body_length==0)
{
@ -513,15 +517,8 @@ static void file_check_gpg(file_recovery_t *file_recovery)
/*@
@ requires buffer_size >= 23;
@ 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_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);
@ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
@ ensures valid_header_check_result(\result, file_recovery_new);
@ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_gpg.extension || file_recovery_new->extension == extension_pgp);
@ ensures (\result == 1) ==> (file_recovery_new->time == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
@ -530,11 +527,8 @@ static void file_check_gpg(file_recovery_t *file_recovery)
@ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_gpg);
@ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@*/
// @ assigns *file_recovery_new;
// X assigns *file_recovery_new;
static int header_check_gpg(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 i=0;
@ -543,6 +537,7 @@ static int header_check_gpg(const unsigned char *buffer, const unsigned int buff
int partial_body_length=0;
int stop=0;
memset(packet_tag, 0, sizeof(packet_tag));
/*@ assert \initialized(packet_tag + (0 .. 15)); */
/*@
@ loop invariant 0 <= nbr <=16;
@ loop assigns i, packet_tag[0..nbr], nbr, partial_body_length, stop;
@ -745,30 +740,29 @@ static int header_check_gpg(const unsigned char *buffer, const unsigned int buff
file_recovery_new->extension=extension_pgp;
return 1;
}
if( /* encrypted_data.gpg */
((packet_tag[0]==OPENPGP_TAG_PUBKEY_ENC_SESSION_KEY ||
/* encrypted_data.gpg */
if(((packet_tag[0]==OPENPGP_TAG_PUBKEY_ENC_SESSION_KEY ||
packet_tag[0]==OPENPGP_TAG_SYMKEY_ENC_SESSION_KEY) &&
(packet_tag[1]==OPENPGP_TAG_SYM_ENC_DATA ||
packet_tag[1]==OPENPGP_TAG_SYM_ENC_INTEGRITY)) ||
/* pubring.gpg */
(packet_tag[0]==OPENPGP_TAG_PUB_KEY &&
packet_tag[1]==OPENPGP_TAG_USER_ID &&
packet_tag[2]==OPENPGP_TAG_SIGNATURE &&
packet_tag[3]==OPENPGP_TAG_TRUST) ||
(packet_tag[0]==OPENPGP_TAG_PUB_KEY &&
packet_tag[1]==OPENPGP_TAG_USER_ID &&
packet_tag[2]==OPENPGP_TAG_SIGNATURE &&
packet_tag[3]==OPENPGP_TAG_PUB_SUBKEY) ||
/* secring.gpg */
(packet_tag[0]==OPENPGP_TAG_SEC_KEY &&
packet_tag[1]==OPENPGP_TAG_USER_ID &&
packet_tag[2]==OPENPGP_TAG_SIGNATURE &&
packet_tag[3]==OPENPGP_TAG_TRUST) ||
(packet_tag[0]==OPENPGP_TAG_SEC_KEY &&
packet_tag[1]==61 &&
packet_tag[2]==61 &&
packet_tag[3]==61)
)
(packet_tag[1]==OPENPGP_TAG_SYM_ENC_DATA ||
packet_tag[1]==OPENPGP_TAG_SYM_ENC_INTEGRITY)) ||
/* pubring.gpg */
(packet_tag[0]==OPENPGP_TAG_PUB_KEY &&
packet_tag[1]==OPENPGP_TAG_USER_ID &&
packet_tag[2]==OPENPGP_TAG_SIGNATURE &&
packet_tag[3]==OPENPGP_TAG_TRUST) ||
(packet_tag[0]==OPENPGP_TAG_PUB_KEY &&
packet_tag[1]==OPENPGP_TAG_USER_ID &&
packet_tag[2]==OPENPGP_TAG_SIGNATURE &&
packet_tag[3]==OPENPGP_TAG_PUB_SUBKEY) ||
/* secring.gpg */
(packet_tag[0]==OPENPGP_TAG_SEC_KEY &&
packet_tag[1]==OPENPGP_TAG_USER_ID &&
packet_tag[2]==OPENPGP_TAG_SIGNATURE &&
packet_tag[3]==OPENPGP_TAG_TRUST) ||
(packet_tag[0]==OPENPGP_TAG_SEC_KEY &&
packet_tag[1]==61 &&
packet_tag[2]==61 &&
packet_tag[3]==61))
{
reset_file_recovery(file_recovery_new);
file_recovery_new->file_check=&file_check_gpg;
@ -785,7 +779,7 @@ static int header_check_gpg(const unsigned char *buffer, const unsigned int buff
}
/*@
@ requires \valid(file_stat);
@ requires valid_register_header_check(file_stat);
@*/
static void register_header_check_gpg(file_stat_t *file_stat)
{