--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on November 2014 ---
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?