--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on September 2015 ---
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