# Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# [Frama-c-discuss] OpenSSL SHA256

*Subject*: [Frama-c-discuss] OpenSSL SHA256*From*: kurt at roeckx.be (Kurt Roeckx)*Date*: Mon, 28 Sep 2015 23:34:24 +0200

Hi, I've been looking at using frama-c for OpenSSL to see if it's useful. I started with the SHA256 code and then found that at least others looked at skein and keccak, so it looks like I at least found a good starting point to look at it. But I'm running in some problems getting things validated and I'm not really sure how to fix it. I also seem to be getting some weird results, but I think getting into all of them here is going to make this way to long. I think one of the problems comes from casting an unsigned char * to a void * and then back to an unsigned char *. Should Wp be able to handle that? It clearly seems to have a problem if my parameter "void *data" is ends up in a "\valid_read((char *) data_+(0..len-1));", while Value is happy with that. One of the strange results is that I have those 2: /*@ assert \valid((p+n)+(0 .. HASH_CBLOCK-1-n)); */ /*@ assert \valid((unsigned char *)((void *)(p+n))+(0 .. HASH_CBLOCK-1-n)); */ For the first one Wp shows surely_valid, for the 2nd valid_under_hyp, but for both it shows "/*@ assert \valid((p+n)+(0 .. (16*4-1)-n)); */ ;" in the GUI. After a lot of trying (and turning everything in unsigned char *), I got Wp to prove the requires \valid_read(in+(0 .. num*(16*4)-1)) in sha256_block_data_order() (valid_under_hyp). This code: SHA_LONG l; int i; const unsigned char *data = in; [...] /*@ loop invariant 0 <= i <= 16; */ for (i = 0; i < 16; i++) { HOST_c2l(data, l); /* do something with l, no longer touch data. */ } With HOST_c2l being: # define HOST_c2l(c,l) (l =(((unsigned long)(*((c)++))) ), \ l|=(((unsigned long)(*((c)++)))<< 8), \ l|=(((unsigned long)(*((c)++)))<<16), \ l|=(((unsigned long)(*((c)++)))<<24) ) It was turned into: i = 0; /*@ loop invariant 0 <= i <= 16; */ while (i < 16) { { unsigned char const *tmp; unsigned char const *tmp_0; unsigned char const *tmp_1; unsigned char const *tmp_2; unsigned int tmp_3; { /*sequence*/ tmp = data; data ++; /*@ assert Value: initialisation: \initialized(tmp); */ /*@ assert Value: mem_access: \valid_read(tmp); */ l = (unsigned int)((unsigned long)*tmp << 24); } { /*sequence*/ tmp_0 = data; data ++; /*@ assert Value: initialisation: \initialized(tmp_0); */ /*@ assert Value: mem_access: \valid_read(tmp_0); */ l = (unsigned int)((unsigned long)l | ((unsigned long)*tmp_0 << 16)); } { /*sequence*/ tmp_1 = data; data ++; /*@ assert Value: initialisation: \initialized(tmp_1); */ /*@ assert Value: mem_access: \valid_read(tmp_1); */ l = (unsigned int)((unsigned long)l | ((unsigned long)*tmp_1 << 8)); } { /*sequence*/ tmp_2 = data; data ++; /*@ assert Value: initialisation: \initialized(tmp_2); */ /*@ assert Value: mem_access: \valid_read(tmp_2); */ l = (unsigned int)((unsigned long)l | (unsigned long)*tmp_2); } And even though I've proved the valid_read() and there are exactly 16 such HOST_c2l() calls neither Wp nor Value seems to be able to prove any of those, and Value first complains about accessing uninitliazed data, completely indeterminate value and out of bounds read on that HOST_c2l() line. But Value always seems to be running before Wp and I can't seem to figure out how to run it again from the gui, it just doesn't seem to do anything. Would it make sense to run Value again after Wp proved the \value_read()? Does someone have a suggestion on how to continue? Kurt

**Follow-Ups**:**[Frama-c-discuss] OpenSSL SHA256***From:*kurt at roeckx.be (Kurt Roeckx)

**[Frama-c-discuss] OpenSSL SHA256***From:*boris at yakobowski.org (Boris Yakobowski)

- Prev by Date:
**[Frama-c-discuss] JFLA 2016 : premier appel à communications** - Next by Date:
**[Frama-c-discuss] OpenSSL SHA256** - Previous by thread:
**[Frama-c-discuss] JFLA 2016 : premier appel à communications** - Next by thread:
**[Frama-c-discuss] OpenSSL SHA256** - Index(es):