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