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

Hi,

You are asking very interesting questions, but the discussion is sometimes
a bit too abstract. Can you post more complete (parseable) snippets of what
you are trying to prove, in which the unimportant parts have been elided?
Tiis would help us what is "normal" -- given the current capabilities of
the plugins -- and what warrants more investigation. I will try to make a
few general remarks.


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

The front-end tries to discard redundant pointer casts. If p has type
unsigned char *, this explains why both casts get simplified. However, it
is a bit strange to see one assert proven and not the other. In the GUI, in
the properties tab, can you double-click on the assert with status
'valid_under_hyp' and tell us what hypothesis the proof depends on?

As a general question regarding casts and WP, did you try the model
Typed+cast that was suggested a few weeks back on this list?

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

You can sequence plugins on the command-line using -then, e.g. frama-c ...
-wp -then -val. If Value has already run, running it "again" in the GUI
will have no effect because all the results are memoized, and Frama-C's
kernel will detect that there is no need to perform another analysis. What
results did you expect by re-running Value? Also, on what function are you
starting you analysis (option -main) ?

> Would it make sense to run Value again after Wp proved the \value_read()?

No. When Value emits a \valid or \valid_read alarm, it automatically takes
it into account for the remainder of the analysis. Regarding pre-written
assertion, they are taken into account regardless of the fact they are
proven by another plugin. Every 'assert' clause is assumed to be true by
any plugin.


On Tue, Sep 29, 2015 at 11:49 PM, Kurt Roeckx <kurt at roeckx.be> wrote:

> 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
>
> _______________________________________________
> 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/baf76b43/attachment.html>