--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on November 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow



Hi !

Instead of writing the ?assembly? by hand, you should have a look to the machine-integer model of WP.
Using option ?-wp-model +cint? (+nat is the default, Cf. WP manual), all machine integer operations are converted into a Z-operation followed by an appropriate modulo operator.
For instance, provided 'int a,b ;' expression (a+b) would be interpreted as 'to_sint32 (a+b)?.

By the way, I must notice that WP + RTE is not the best way to check for absence of runtime errors. You should use Value for this purpose.
L.


Le 26 nov. 2014 ? 01:43, Mansour Moufid <mansourmoufid at gmail.com> a ?crit :

> On Mon, 3 Nov 2014 23:14:32 +0000
> Gregory Maxwell <gmaxwell at gmail.com> wrote:
> 
>> Greetings, I haven't used frama-c in some time, it's changed quite a
>> bit (and I've likely forgotten even more...) and I'm having a hard
>> time making progress with it at all this time around.
>> 
>> I'm working on libsecp256k1 a free software cryptographic signature
>> library which will be used by the reference Bitcoin software;
>> verifying that optimized implementations are exactly correct is
>> critical for this application
>> 
>> I'm trying to prove some simple theorems about some inner kernels used
>> for field arithmetic.
>> 
>> To start with, I need to first prove that the code is overflow free,
>> under assumptions. (I don't just need to do this to make WP happy, its
>> required for correctness of the code.
>> 
>> Here is a reduced testcase that I'm trying:
>> 
>> $ cat a.c
>> #include <stdint.h>
>> /*@ requires \valid(a + (0..9));
>>    requires \valid(b + (0..9));
>>    requires (a[0] < 1073741824);
>>    requires (a[1] < 1073741824);
>>    requires (a[2] < 1073741824);
>>    requires (a[3] < 1073741824);
>>    requires (a[4] < 1073741824);
>>    requires (a[5] < 1073741824);
>>    requires (a[6] < 1073741824);
>>    requires (a[7] < 1073741824);
>>    requires (a[8] < 1073741824);
>>    requires (a[9] < 67108864);
>>    requires (b[0] < 1073741824);
>>    requires (b[1] < 1073741824);
>>    requires (b[2] < 1073741824);
>>    requires (b[3] < 1073741824);
>>    requires (b[4] < 1073741824);
>>    requires (b[5] < 1073741824);
>>    requires (b[6] < 1073741824);
>>    requires (b[7] < 1073741824);
>>    requires (b[8] < 1073741824);
>>    requires (b[9] < 67108864);
>> */
>> void static inline secp256k1_fe_mul_inner(const uint32_t *a, const
>> uint32_t *b, uint32_t *r) {
>>    uint64_t d;
>>    d  = (uint64_t)a[0] * b[9]
>>       + (uint64_t)a[1] * b[8]
>>       + (uint64_t)a[2] * b[7]
>>       + (uint64_t)a[3] * b[6]
>>       + (uint64_t)a[4] * b[5]
>>       + (uint64_t)a[5] * b[4]
>>       + (uint64_t)a[6] * b[3]
>>       + (uint64_t)a[7] * b[2]
>>       + (uint64_t)a[8] * b[1]
>>       + (uint64_t)a[9] * b[0];
>> }
> 
> I have attempted to do something similar with the reference Curve25519
> implementation.
> 
> The strategy I found works well with the WP plugin is to break down
> complex arithmetic expressions into basic functions, kind of like you
> would write assembly.
> 
> So your example code would look like this:
> 
>    #include <stdint.h>
>    /*@ 
>        ensures \result == a * b;
>     */
>    static inline uint64_t
>    _uint32_mul(const uint32_t a, const uint32_t b)
>    {
>        return (uint64_t) a * (uint64_t) b;
>    }
>    /*@ 
>        requires a <= UINT64_MAX / 2;
>        requires b <= UINT64_MAX / 2;
>        ensures \result == a + b;
>     */
>    static inline uint64_t
>    _uint64_sum(const uint64_t a, const uint64_t b)
>    {
>        return a + b;
>    }
>    /*@ 
>        requires a <= UINT64_MAX / 10;
>        requires b <= UINT64_MAX / 10;
>        requires c <= UINT64_MAX / 10;
>        requires d <= UINT64_MAX / 10;
>        requires e <= UINT64_MAX / 10;
>        requires f <= UINT64_MAX / 10;
>        requires g <= UINT64_MAX / 10;
>        requires h <= UINT64_MAX / 10;
>        requires i <= UINT64_MAX / 10;
>        requires j <= UINT64_MAX / 10;
>        ensures \result == a + b + c + d + e + f + g + h + i + j;
>     */
>    static inline uint64_t
>    _uint64_sum_10(const uint64_t a, const uint64_t b,
>        const uint64_t c, const uint64_t d,
>        const uint64_t e, const uint64_t f,
>        const uint64_t g, const uint64_t h,
>        const uint64_t i, const uint64_t j)
>    {
>        return (_uint64_sum(a,
>                _uint64_sum(b,
>                _uint64_sum(c,
>                _uint64_sum(d,
>                _uint64_sum(e,
>                _uint64_sum(f,
>                _uint64_sum(g,
>                _uint64_sum(h,
>                _uint64_sum(i,j))))))))));
>    }
>    /*@ 
>        requires \valid(a + (0..9));
>        requires \valid(b + (0..9));
>        requires (a[0] < 1073741824);
>        requires (a[1] < 1073741824);
>        requires (a[2] < 1073741824);
>        requires (a[3] < 1073741824);
>        requires (a[4] < 1073741824);
>        requires (a[5] < 1073741824);
>        requires (a[6] < 1073741824);
>        requires (a[7] < 1073741824);
>        requires (a[8] < 1073741824);
>        requires (a[9] < 67108864);
>        requires (b[0] < 1073741824);
>        requires (b[1] < 1073741824);
>        requires (b[2] < 1073741824);
>        requires (b[3] < 1073741824);
>        requires (b[4] < 1073741824);
>        requires (b[5] < 1073741824);
>        requires (b[6] < 1073741824);
>        requires (b[7] < 1073741824);
>        requires (b[8] < 1073741824);
>        requires (b[9] < 67108864);
>    */
>    static inline void
>    secp256k1_fe_mul_inner(const uint32_t a[10], const uint32_t b[10])
>    {
>        uint64_t d;
>        d = _uint64_sum_10(
>                _uint32_mul(a[0], b[9]),
>                _uint32_mul(a[1], b[8]),
>                _uint32_mul(a[2], b[7]),
>                _uint32_mul(a[3], b[6]),
>                _uint32_mul(a[4], b[5]),
>                _uint32_mul(a[5], b[4]),
>                _uint32_mul(a[6], b[3]),
>                _uint32_mul(a[7], b[2]),
>                _uint32_mul(a[8], b[1]),
>                _uint32_mul(a[9], b[0])
>            );
>    }
> 
> Check it with the WP and RTE plugins:
> 
>    $ frama-c -machdep $(uname -m) -pp-annot -wp -wp-rte \
>        -wp-prop @ensures,unsigned_overflow a.c 
>    ...
>    [wp] Proved goals:    7 / 7
>         Qed:             3  (4ms-32ms)
>         Alt-Ergo:        4  (76ms-80ms) (13)
> 
> It works, but it's very verbose.  You may find that the value analysis
> plugin is less tedious, I don't know.
> 
> Best of luck.
> 
> Mansour
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

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