Hi,
I wonder if anyone on this list has experience with formal verification,
or cbmc (https://www.cprover.org/cbmc/) in particular?
Inspiration from Jade Philipoom's nice talk at 39c3 a few days ago.
My interest is verifying arithmetic functions in gmp (and nettle). But
I'm having difficulties getting started, I probably don't understand
proper usage of the tools. I've installed cbmc 6.6.0 (debian package),
with the default "minisat" backend. I'm trying the "goto-analyzer" tool
in this package, which as I understand it aims to find strict proofs
that code under analysis satisfies claimed properties.
I'm starting with something I think should be easy: Verifying memory
read and written by mpn_copyi. Complete input file:
#include <stddef.h>
typedef unsigned long mp_limb_t;
typedef mp_limb_t *mp_ptr;
typedef const mp_limb_t *mp_srcptr;
typedef long mp_size_t;
void
mpn_copyi (mp_ptr d, mp_srcptr s, mp_size_t n)
__CPROVER_requires (n > 0)
__CPROVER_requires (s != NULL)
__CPROVER_requires (d != NULL)
__CPROVER_requires (__CPROVER_is_fresh (s, n * sizeof(*s)))
__CPROVER_requires (__CPROVER_is_fresh (d, n * sizeof(*d)))
__CPROVER_assigns (__CPROVER_object_upto (d, n * sizeof (*d)))
{
mp_size_t i;
for (i = 0; i < n; i++)
d[i] = s[i];
}
I then run the analyzer as
goto-analyzer --verify --function mpn_copyi copyi.c
But I then get a bunch of errors that I think should be excluded by the
declarered requirements, including:
[mpn_copyi.pointer_dereference.7] line 18 dereference failure: pointer NULL
in s[i]: UNKNOWN
[mpn_copyi.pointer_dereference.8] line 18 dereference failure: pointer
invalid in s[i]: UNKNOWN
[mpn_copyi.overflow.1] line 17 arithmetic overflow on signed + in i + 1l:
UNKNOWN
(__CPROVER_requires say that pointers are non-null, and the i++
operation is on a code path where i < n (i and n of same signed type),
so it can't overflow).
So I'm most likely doing something wrong. Any help with solving these
newbie issues is much appreciated.
I then have a few more open questions on what is supported by cbmc, and
if that is a suitable tool for my use.
1. From the manual, I think __CPROVER_is_fresh expresses that the area
is properly allocated, and not overlapping with any other area declared
as __CPROVER_is_fresh (see
https://diffblue.github.io/cbmc/contracts-memory-predicates.html). Is
it possible to express that certain kinds of overlaps are allowed,
e.g., for mpn_copyi above??
2. To express what a gmp function is doing, it would help to define a
mapping from limb array to a more abstract bignum integer, and then
express requirements in terms of arithmetic properties. E.g., if I
want to express the expected modulo relation between inputs and
outputs of mpn_mod_1.
3. I'd also like to apply verification to functions implemented in
assembly (initially x86_64 and arm, but I'm interested in all
achitectures with assembly code in gmp or nettle). Does cbmc support
that in some way? Or would it be reasonable to decompile an assembly
function into C, and apply verification to that?
Regards,
/Niels
--
Niels Möller. PGP key CB4962D070D77D7FCB8BA36271D8F1FF368C6677.
Internet email is subject to wholesale government surveillance.
_______________________________________________
gmp-devel mailing list
[email protected]
https://gmplib.org/mailman/listinfo/gmp-devel
