Frama-C-discuss mailing list archives

boris at yakobowski.org (Boris Yakobowski) · Wed, 30 Sep 2015 20:04:28 +0200

On Wed, Sep 30, 2015 at 12:11 PM, Boris Yakobowski <boris at yakobowski.org>
wrote:

>   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
>   }
>
>
Those two examples are flawed, because the tests fail to guard against
values of i so big that i+64 overflows on unsigned integers. Apologies for
this. Thankfully, they are proved by WP only when unsigned computations are
assumed not to overflow, an assumption that Value does not make (and
verify) by default. The user is warned that the verification is incomplete
by the message "Missing RTE guards". With model Typed+cint, the message
disappears but the assertion or the precondition remain unproven. Of
course, performing the comparison on unsigned long long fixes the code.

On Wed, Sep 30, 2015 at 12:11 PM, Boris Yakobowski <boris at yakobowski.org>
wrote:

> 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
>

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

Frama-C-discuss mailing list archives

[Frama-c-discuss] OpenSSL SHA256