--- layout: fc_discuss_archives title: Message 7 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



Probably the same problem as 
http://lists.gforge.inria.fr/pipermail/why-discuss/2014-October/000697.html

You should run fram-c with extra option: -cpp-extra-args="-I$(frama-c 
-print-share-path)/libc"

- Claude

Le 04/11/2014 00:14, Gregory Maxwell a ?crit :
> 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 invoke frama-c with:
>
> frama-c -main secp256k1_fe_mul_inner -lib-entry -wp -wp-timeout 300
> -wp-par 1 -wp-rte a.c
>
> And get some successful proof for memory access, followed by alt-ergo
> returning unknown on the overflow checks:
> [...]
> [wp] [Alt-Ergo] Goal
> typed_secp256k1_fe_mul_inner_assert_rte_mem_access_20 : Valid
> (Qed:1ms) (93ms) (74)
> [wp] [Alt-Ergo] Goal
> typed_secp256k1_fe_mul_inner_assert_rte_unsigned_overflow : Unknown
> (Qed:4ms) (4s)
> [wp] [Alt-Ergo] Goal
> typed_secp256k1_fe_mul_inner_assert_rte_unsigned_overflow_2 : Unknown
> (Qed:5ms) (4s)
>
> This is obviously free of overflows, since  1073741824*1073741824*8 +
> 1073741824*67108864*2 < 2^64
>
> (but the non-reduced code, is less trivial
> http://0bin.net/paste/tTR7910ESfwij7Ib#pZwnZkivigEp+73f4D4yWQpXMaEWCmVFTb4XxE6vRUN
> ... which is why I'm starting with just proving overflows since the
> hand verifiable correctness proof in the comments assumes no
> overflow).
>
> I'm using alt-ergo 0.95.1 and frama-c Neon-20140301
>
> Any suggestions?
> _______________________________________________
> 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
>

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |