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

Hello again,

Here are some answers on your question regarding HOST_c2l. This is the code
I used for Value:

#  define HOST_c2l(c,l)   (l =(((unsigned long)(*((c)++)))    ),          \
                         l|=(((unsigned long)(*((c)++)))<< 8),          \
                         l|=(((unsigned long)(*((c)++)))<<16),          \
                         l|=(((unsigned long)(*((c)++)))<<24)           )

void f(unsigned char *in) {
  unsigned long l;
  int i;
  const unsigned char *data = in;

  for (i = 0; i < 16; i++) {
    HOST_c2l(data, l);
    /* do something with l, no longer touch data. */
  }
}

extern  unsigned char t1[64];

#define SIZE 1000
extern unsigned char t2[SIZE];

//@ assigns \nothing;
int rand();

void main(unsigned int i, unsigned int j) {
  if (rand ()) f(t1); // (1): OK

  if (rand () && i <= SIZE - 64) // (2)
    f(t2+i); // Ok

  if (rand () && i + 64 <= SIZE) // (3)
    f(t2+i); // not ok: rewrite into (2) or (4)

  if (rand () && i + 64 <= SIZE) { // (4)
    /*@ assert i <= SIZE - 64; */ // Provable by WP
    f(t2+i); // Ok
  }

  if (rand ()) {
    unsigned char *p = t2+i; // (5)
    //@ assert \valid_read(p+j+(0..63)); // currently, no effect on Value
    f(p+j); /* not ok. Disjunction on p and/or j needed, _before_ the
assertion,
               or on i before the assignment to p */
  }
}


The different calls to f are sorted by complexity for Value, regarding the
validity of the memory access inside f. (The calls to rand are there to
make sure all cases are handled in isolation.) The analysis must be done
with -slevel 16 to unroll the loop in f. The four first patterns can be
proven valid with relatively little effort. In fact, in Frama-C Aluminium,
pattern 3 and 4 should be handled automatically by Value.

Pattern 5 is much more tricky. The assertion does not necessarily hold, but
is sufficient to prove that all accesses within the call to f are valid. In
a perfect world, Value would gain some precision on p, j and p+j through
the assertion, and use this knowledge inside f. This is not currently not
done, and the only possibility is to use a big case analysis on p and j, or
on i and j.


Regarding WP, I annotated f in the following way:

//@ requires \valid_read(in+(0..63));
void f(unsigned char *in) {
  unsigned long l;
  int i;
  const unsigned char *data = in;

  /*@ loop assigns l, i, data;
    loop invariant 0 <= i <= 16;
    loop invariant data == \at(in,Pre)+4*i;
  */
  for (i = 0; i < 16; i++) {
    HOST_c2l(data, l);
    /* do something with l, no longer touch data. */
  }
}

runnning
   frama-c test.c -val -slevel 16 -then -wp

proves every memory access and all preconditions of f. The only thing not
proven by WP is the 'assume' in pattern 5, which is not provable. The loop
invariant 0 <= i <= 16 is proven by both Value and WP. But you must write
it for WP, as it is used together with the other loop invariant to prove
that the memory accesses are in bound.

HTH,



On Mon, Sep 28, 2015 at 11:34 PM, Kurt Roeckx <kurt at roeckx.be> wrote:

> 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
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss




-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150930/8e094901/attachment.html>