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

On Mon, Sep 28, 2015 at 11:34:24PM +0200, Kurt Roeckx wrote:
> 
> 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).
[...]
> 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.

At least in the case of Value I think I understand why it's not
working.  In the case of a previous HASH_UPDATE() call that didn't
fill the whole block (HASH_CBLOCK, 64), it copied the remaining
part to a temporary place.  In the next call it then copies data
from the new incomming data to the temporary place to fill in the
whole HASH_CBLOCK.  The incomming data and length is then updated
with the part already processed, and things seem to go wrong from
there.

With some asserts added, it can properly limit the length of what
is possible.  I'm testing with values up to 1024, and it says the
length can be in the range of 0 .. 1024.  And the data pointer can
be the base pointer + 0 .. 63.  And that's all correct, but not
all combinations are possible, while in the analysis of the
sha256_block_data_order() call it seems to assume all combinations
are possible, and that it can access bytes outside the 1024 range.

If I do something like /*@ assert len <= \at(len,Pre); */ it will
actually limit length to be in the right range, changing it from
all possible values to 0 .. 1024.  (Also see issue 2166.)

But I've been adding various other assert, including things like
/*@ assert \valid_read(data+(0 .. len-1)); */ but that does not
seem to have an effect on Value.

But like I said before, I can prove that \valid_read() using Wp,
but then I can't get any further with Wp in
sha256_block_data_order() for some reason I don't understand yet.

It might be related to being unable to prove either the loop
assigns or assert in this code:
        unsigned char s[1024];
        n = Frama_C_interval(0, 1024);
        /*@ loop invariant 0 <= i <= n;
            loop assigns s[0 .. n-1]; */
        for (i=0; i<n; i++)
            s[i]=Frama_C_interval(0, 255);
        /*@ assert \initialized(s+(0 .. n-1)); */


Kurt