summaryrefslogtreecommitdiffstats
path: root/src/file_gpg.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/file_gpg.c')
-rw-r--r--src/file_gpg.c271
1 files changed, 213 insertions, 58 deletions
diff --git a/src/file_gpg.c b/src/file_gpg.c
index 387e168..84a5587 100644
--- a/src/file_gpg.c
+++ b/src/file_gpg.c
@@ -33,9 +33,12 @@
#ifdef DEBUG_GPG
#include "log.h"
#endif
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
+static const char *extension_pgp="pgp";
static void register_header_check_gpg(file_stat_t *file_stat);
-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);
const file_hint_t file_hint_gpg= {
.extension="gpg",
@@ -82,31 +85,22 @@ const file_hint_t file_hint_gpg= {
static const unsigned char pgp_header[5]= {0xa8, 0x03, 'P', 'G', 'P'};
-static void register_header_check_gpg(file_stat_t *file_stat)
-{
- static const unsigned char gpg_header_pkey_enc[1]= {0x85};
- static const unsigned char gpg_header_symkey_enc[1]= {0x8c};
- static const unsigned char gpg_header_seckey[1]= {0x95};
-#if 1
- static const unsigned char gpg_header_pkey[1]= {0x99};
-#endif
- register_header_check(0, gpg_header_seckey, sizeof(gpg_header_seckey), &header_check_gpg, file_stat);
- register_header_check(0, gpg_header_symkey_enc, sizeof(gpg_header_symkey_enc), &header_check_gpg, file_stat);
- register_header_check(0, gpg_header_pkey_enc, sizeof(gpg_header_pkey_enc), &header_check_gpg, file_stat);
- register_header_check(0, pgp_header, sizeof(pgp_header), &header_check_gpg, file_stat);
-#if 1
- register_header_check(0, gpg_header_pkey, sizeof(gpg_header_pkey), &header_check_gpg, file_stat);
-#endif
-}
-
-static unsigned int openpgp_packet_tag(const unsigned char *buf)
+/*@
+ @ ensures 0 <= \result <= 0x3f;
+ @*/
+static unsigned int openpgp_packet_tag(const unsigned char buf)
{
/* Bit 7 -- Always one */
- if((buf[0]&0x80)==0)
+ if((buf&0x80)==0)
return 0; /* Invalid */
- return ((buf[0]&0x40)==0?((buf[0]>>2)&0x0f):(buf[0]&0x3f));
+ return ((buf&0x40)==0?((buf>>2)&0x0f):(buf&0x3f));
}
+/*@ requires \valid_read(buf+(0..5));
+ @ requires \valid(length_type);
+ @ requires \valid(indeterminate_length);
+ @ ensures (*length_type == 1) || (*length_type == 2) || (*length_type==3)|| (*length_type==5);
+ */
static unsigned int old_format_packet_length(const unsigned char *buf, unsigned int *length_type, int *indeterminate_length)
{
/* Old format */
@@ -119,8 +113,11 @@ static unsigned int old_format_packet_length(const unsigned char *buf, unsigned
*length_type=3;
return (buf[1] << 8) | buf[2];
case 2:
- *length_type=5;
- return (buf[1] << 24) |(buf[2] << 16) | (buf[3] << 8) | buf[4];
+ {
+ const uint32_t *tmp32_ptr=(const uint32_t *)&buf[1];
+ *length_type=5;
+ return be32(*tmp32_ptr);
+ }
default:
*length_type=1;
*indeterminate_length=1;
@@ -128,6 +125,12 @@ static unsigned int old_format_packet_length(const unsigned char *buf, unsigned
}
}
+/*@ requires \valid_read(buf+(0..5));
+ @ requires \valid(length_type);
+ @ requires \valid(partial_body_length);
+ @ ensures (*length_type == 1) || (*length_type == 2) || (*length_type==5);
+ @ ensures (*partial_body_length==0) || (*partial_body_length==1);
+ */
static unsigned int new_format_packet_length(const unsigned char *buf, unsigned int *length_type, int *partial_body_length)
{
*partial_body_length=0;
@@ -135,34 +138,53 @@ static unsigned int new_format_packet_length(const unsigned char *buf, unsigned
if(buf[0]<=191)
{
*length_type=1;
+ /*@ assert 0 <= buf[0] <= 191; */
return buf[0];
}
/* Two-Octet Body Length */
if(buf[0]<=223)
{
+ /*@ assert 192 <= buf[0] <= 223; */
+ unsigned int tmp=buf[0];
+ /*@ assert 192 <= tmp <= 223; */
+ tmp = ((tmp-192) << 8) + buf[1] + 192;
+ /*@ assert 192 <= tmp <= ((223-192) << 8) + 255 + 192; */
*length_type=2;
- return ((buf[0] - 192) << 8) + buf[1] + 192;
+ return tmp;
}
/* Five-Octet Body Length */
if(buf[0]==255)
{
+ const uint32_t *tmp32=(const uint32_t *)&buf[1];
+ const unsigned int tmp=be32(*tmp32);
*length_type=5;
- return (buf[1] << 24) | (buf[2] << 16) | (buf[3] << 8) | buf[4];
+ return tmp;
+ }
+ {
+ /*@ assert 224 <= buf[0] <= 254; */
+ const unsigned int tmp=buf[0]&0x1fu;
+ /* Partial Body Lengths */
+ *length_type=1;
+ *partial_body_length=1;
+ return 1u << tmp;
}
- /* Partial Body Lengths */
- *length_type=1;
- *partial_body_length=1;
- return 1 << (buf[0]& 0x1F);
}
-static int is_valid_mpi(const uint16_t *size)
+/*@
+ @ ensures \result == -1 || 0 <= \result <= 2048;
+ @*/
+static int is_valid_mpi(const uint16_t size)
{
- if(be16(*size) <= 16384)
- return (be16(*size)+7)/8;
+ const uint16_t tmp=be16(size);
+ if(tmp <= 16384)
+ return (tmp+7)/8;
return -1;
}
-static int is_valid_pubkey_algo(const int algo)
+/*@
+ @ ensures \result == 0 || \result == 1;
+ @*/
+static int is_valid_pubkey_algo(const int algo)
{
/* 1 - RSA (Encrypt or Sign)
* 2 - RSA Encrypt-Only
@@ -189,6 +211,9 @@ static int is_valid_pubkey_algo(const int algo)
}
}
+/*@
+ @ ensures \result == 0 || \result == 1;
+ @*/
static int is_valid_sym_algo(const int algo)
{
/*
@@ -222,6 +247,9 @@ static int is_valid_sym_algo(const int algo)
}
}
+/*@
+ @ ensures \result == 0 || \result == 1;
+ @*/
static int is_valid_S2K(const unsigned int algo)
{
/* ID S2K Type
@@ -235,48 +263,62 @@ static int is_valid_S2K(const unsigned int algo)
return (algo==0 || algo==1 || algo==3);
}
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @*/
static void file_check_gpg(file_recovery_t *file_recovery)
{
unsigned int tag=0;
unsigned int nbr=0;
int partial_body_length=0;
int stop=0;
- off_t offset=0;
- unsigned char buffer[32];
+ uint64_t offset=0;
const uint64_t org_file_size=file_recovery->file_size;
file_recovery->file_size=0;
while(stop==0)
{
+ unsigned char buffer[32];
unsigned int i=0;
unsigned int length_type=0;
unsigned int length;
const int old_partial_body_length=partial_body_length;
+ if(nbr >=0xffffffff || offset + 6 >= 0x8000000000000000)
+ return;
+ /*@ assert offset < 0x8000000000000000 - 6; */
if(my_fseek(file_recovery->handle, offset, SEEK_SET) < 0 ||
fread(&buffer, sizeof(buffer), 1, file_recovery->handle) != 1)
return;
+#ifdef __FRAMAC__
+ Frama_C_make_unknown((char *)&buffer, sizeof(buffer));
+#endif
if(partial_body_length==0)
{
- if((buffer[i]&0x80)==0)
+ if((buffer[0]&0x80)==0)
break; /* Invalid */
- tag=openpgp_packet_tag(&buffer[i]);
- if((buffer[i]&0x40)==0)
+ tag=openpgp_packet_tag(buffer[0]);
+ if((buffer[0]&0x40)==0)
{
- length=old_format_packet_length(&buffer[i], &length_type, &stop);
+ length=old_format_packet_length(&buffer[0], &length_type, &stop);
+ /*@ assert (length_type == 1) || (length_type == 2) || (length_type==3) || (length_type==5); */
}
else
{
- length=new_format_packet_length(&buffer[i+1], &length_type, &partial_body_length);
+ length=new_format_packet_length(&buffer[1], &length_type, &partial_body_length);
length_type++;
+ /*@ assert (length_type == 2) || (length_type == 3) || (length_type==6); */
}
}
else
{
- length=new_format_packet_length(&buffer[i], &length_type, &partial_body_length);
+ length=new_format_packet_length(&buffer[0], &length_type, &partial_body_length);
+ /*@ assert (length_type == 1) || (length_type == 2) || (length_type==5); */
}
+ /*@ assert 0 <= length_type <= 6; */
#ifdef DEBUG_GPG
log_info("GPG 0x%04x: %02u tag=%2u, size=%u + %u)\n",
- i, nbr, tag, length_type, length);
+ 0, nbr, tag, length_type, length);
#endif
#if 0
if(tag==0 || tag==15 || (tag>19 && tag!=61)) /* Reserved or unused */
@@ -284,14 +326,19 @@ static void file_check_gpg(file_recovery_t *file_recovery)
#endif
if(length_type==0)
break; /* Don't know how to find the size */
+ /*@ assert 0 < length_type <= 6; */
i+=length_type;
+ /*@ assert 0 < i <= 6; */
offset+=length_type;
+ /*@ assert offset < 0x8000000000000000; */
+ if(offset + length >= 0x8000000000000000)
+ return ;
if(old_partial_body_length==0)
{
if(tag==OPENPGP_TAG_PUBKEY_ENC_SESSION_KEY)
{
- const uint16_t *mpi=(const uint16_t *)&buffer[i+1+8+1];
- const int len=is_valid_mpi(mpi);
+ const uint16_t *mpi_ptr=(const uint16_t *)&buffer[i+1+8+1];
+ const int len=is_valid_mpi(*mpi_ptr);
/* uint8_t version must be 3
* uint64_t pub_key_id
* uint8_t pub_key_algo
@@ -311,14 +358,16 @@ static void file_check_gpg(file_recovery_t *file_recovery)
if(buffer[i+1+8]==16 || buffer[i+1+8]==20)
{
int len2;
- unsigned char tmp[2];
+ uint16_t mpi2;
if(my_fseek(file_recovery->handle, offset+1+8+1+2+len, SEEK_SET) < 0 ||
- fread(&tmp, sizeof(tmp), 1, file_recovery->handle) != 1)
+ fread(&mpi2, sizeof(mpi2), 1, file_recovery->handle) != 1)
return;
- mpi=(const uint16_t *)&tmp[0];
- len2=is_valid_mpi(mpi);
+#ifdef __FRAMAC__
+ Frama_C_make_unknown((char *)&mpi2, sizeof(mpi2));
+#endif
+ len2=is_valid_mpi(mpi2);
#ifdef DEBUG_GPG
- log_info(" data: [ %u bits]\n", be16(*mpi));
+ log_info(" data: [ %u bits]\n", be16(*mpi2));
#endif
if(len2 <= 0)
return ;
@@ -408,6 +457,18 @@ static void file_check_gpg(file_recovery_t *file_recovery)
file_recovery->file_size=(stop==0?org_file_size:(uint64_t)offset);
}
+/*@
+ @ 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_check == &file_check_gpg);
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_gpg.extension || file_recovery_new->extension == extension_pgp);
+ @*/
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;
@@ -416,8 +477,12 @@ 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));
- while(nbr<16 && i < buffer_size - 20 && stop==0)
+ /*@
+ @ loop invariant 0 <= nbr <=16;
+ @*/
+ while(nbr<16 && i < buffer_size - 23 && stop==0)
{
+ /*@ assert 0 <= i < buffer_size - 23; */
unsigned int length_type=0;
unsigned int tag;
unsigned int length;
@@ -426,21 +491,25 @@ static int header_check_gpg(const unsigned char *buffer, const unsigned int buff
{
if((buffer[i]&0x80)==0)
break; /* Invalid */
- packet_tag[nbr]=openpgp_packet_tag(&buffer[i]);
+ packet_tag[nbr]=openpgp_packet_tag(buffer[i]);
if((buffer[i]&0x40)==0)
{
length=old_format_packet_length(&buffer[i], &length_type, &stop);
+ /*@ assert (length_type == 1) || (length_type == 2) || (length_type==3) || (length_type==5); */
}
else
{
length=new_format_packet_length(&buffer[i+1], &length_type, &partial_body_length);
length_type++;
+ /*@ assert (length_type == 2) || (length_type == 3) || (length_type==6); */
}
}
else
{
length=new_format_packet_length(&buffer[i], &length_type, &partial_body_length);
+ /*@ assert (length_type == 1) || (length_type == 2) || (length_type==5); */
}
+ /*@ assert 0 <= length_type <= 6; */
tag=packet_tag[nbr];
#ifdef DEBUG_GPG
log_info("GPG 0x%04x: %02u tag=%2u, size=%u + %u)\n",
@@ -452,13 +521,15 @@ static int header_check_gpg(const unsigned char *buffer, const unsigned int buff
#endif
if(length_type==0)
break; /* Don't know how to find the size */
+ /*@ assert 0 < length_type <= 6; */
i+=length_type;
+ /*@ assert 0 <= i < buffer_size - 23 + 6; */
if(old_partial_body_length==0)
{
if(tag==OPENPGP_TAG_PUBKEY_ENC_SESSION_KEY)
{
- const uint16_t *mpi=(const uint16_t *)&buffer[i+1+8+1];
- const int len=is_valid_mpi(mpi);
+ const uint16_t *mpi_ptr=(const uint16_t *)&buffer[i+1+8+1];
+ const int len=is_valid_mpi(*mpi_ptr);
/* uint8_t version must be 3
* uint64_t pub_key_id
* uint8_t pub_key_algo
@@ -466,6 +537,7 @@ static int header_check_gpg(const unsigned char *buffer, const unsigned int buff
if(buffer[i]==3 && is_valid_pubkey_algo(buffer[i+1+8]) &&
len>0)
{
+ const unsigned int offset_mpi=i+1+8+1+2+len;
#ifdef DEBUG_GPG
log_info("GPG :pubkey enc packet: version %u, algo %u, keyid %02X%02X%02X%02X%02X%02X%02X%02X\n",
buffer[i], buffer[i+1+8],
@@ -473,14 +545,15 @@ static int header_check_gpg(const unsigned char *buffer, const unsigned int buff
buffer[i+5], buffer[i+6], buffer[i+7], buffer[i+8]);
log_info(" data: [ %u bits]\n", be16(*mpi));
#endif
- if((unsigned)(1+8+1+2+len) > length)
+ if(offset_mpi +2 > length)
return 0;
if((buffer[i+1+8]==16 || buffer[i+1+8]==20) &&
- i+1+8+1+2+len+2<buffer_size)
+ offset_mpi + 2 <= buffer_size)
{
int len2;
- mpi=(const uint16_t *)&buffer[i+1+8+1+2+len];
- len2=is_valid_mpi(mpi);
+ /*@ assert 0 <= offset_mpi + 2 <= buffer_size; */
+ mpi_ptr=(const uint16_t *)&buffer[offset_mpi];
+ len2=is_valid_mpi(*mpi_ptr);
#ifdef DEBUG_GPG
log_info(" data: [ %u bits]\n", be16(*mpi));
#endif
@@ -600,7 +673,7 @@ static int header_check_gpg(const unsigned char *buffer, const unsigned int buff
{
reset_file_recovery(file_recovery_new);
file_recovery_new->file_check=&file_check_gpg;
- file_recovery_new->extension="pgp";
+ file_recovery_new->extension=extension_pgp;
return 1;
}
if( /* encrypted_data.gpg */
@@ -641,3 +714,85 @@ static int header_check_gpg(const unsigned char *buffer, const unsigned int buff
#endif
return 0;
}
+
+/*@
+ @ requires \valid(file_stat);
+ @*/
+static void register_header_check_gpg(file_stat_t *file_stat)
+{
+ static const unsigned char gpg_header_pkey_enc[1]= {0x85};
+ static const unsigned char gpg_header_symkey_enc[1]= {0x8c};
+ static const unsigned char gpg_header_seckey[1]= {0x95};
+ static const unsigned char gpg_header_pkey[1]= {0x99};
+ register_header_check(0, gpg_header_seckey, sizeof(gpg_header_seckey), &header_check_gpg, file_stat);
+ register_header_check(0, gpg_header_symkey_enc, sizeof(gpg_header_symkey_enc), &header_check_gpg, file_stat);
+ register_header_check(0, gpg_header_pkey_enc, sizeof(gpg_header_pkey_enc), &header_check_gpg, file_stat);
+ register_header_check(0, pgp_header, sizeof(pgp_header), &header_check_gpg, file_stat);
+ register_header_check(0, gpg_header_pkey, sizeof(gpg_header_pkey), &header_check_gpg, file_stat);
+}
+
+#if defined(MAIN_gpg)
+#define BLOCKSIZE 65536u
+int main()
+{
+ const char fn[] = "recup_dir.1/f0000000.gpg";
+ unsigned char buffer[BLOCKSIZE];
+ int res;
+ 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_gpg;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+ register_header_check_gpg(&file_stats);
+ if(header_check_gpg(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_gpg.extension || file_recovery_new.extension == extension_pgp; */
+ /*@ assert file_recovery_new.file_check == &file_check_gpg; */
+ /*@ assert file_recovery_new.file_stat->file_hint!=NULL; */
+ {
+ 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_gpg(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_gpg; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_gpg(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+#endif