Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Arbitrary size fixed integer math

Hello Kurt.

On Sat, Oct 24, 2015 at 2:04 PM, Kurt Roeckx <kurt at roeckx.be> wrote:

>
> I was wondering if it would be possible to verify the math of the
> BN library in OpenSSL. So I tried a little test program to see
> what would happen.
>

Your simplified program is definitely in scope for the deductive
verification plug-ins WP and Jessie, and I say this with the serenity of
one who does not have access to these tools today and is only going to
provide vague hints and guesses throughout this message.

One thing that is not clear on the other hand is whether the existing
automatic provers would be able to prove all the resulting proof
obligations if we write all the necessary annotations.


If you are using WP or Jessie, then you do not need to write a driver such
as the main() function in your file. The main() function that you wrote is
useful to the value analysis plug-in, but that one will never prove a
sophisticated property like the one you are aiming for anyway.


Your file contains this loop:

    /*@ loop invariant 0 <= i <= BN_SIZE;
      @ loop assigns i, ll, r->num[0 .. BN_SIZE-1];
      @*/
    for (i = 0; i < BN_SIZE; i++) {
        ll += (uint64_t) a->num[i] + b->num[i];
        r->num[i] = (uint32_t)ll & BN_MASK2;
        ll >>= 32;
    }

First, using a fixed small value for BN_SIZE does not simplify things for
Jessie and WP as much as one would like. A loop remains in the program, and
the way these plug-ins reason about loops involves a general “inductive
loop invariant” that you have begun writing, even when it is obvious the
loop is making exactly two iterations.

So one way to simplify the program even more and check whether the
automatic provers will be able to handle the mix of arithmetic and logic
operations would be, since you have already fixed BN_SIZE to 2, to unroll
the loop. Let us do it manually for simplicity, although there exists a
Frama-C option to do this automatically, -ulevel:

i = 0;

        ll += (uint64_t) a->num[i] + b->num[i];
        r->num[i] = (uint32_t)ll & BN_MASK2;
        ll >>= 32;

i++

        ll += (uint64_t) a->num[i] + b->num[i];
        r->num[i] = (uint32_t)ll & BN_MASK2;
        ll >>= 32;

In the above code no loop remains, and thus any failure of the automatic
provers is not caused by insufficient or wrong annotations on our part.
Proving that this code computes 64-bit addition using 32-bit additions
would be an encouraging first step (but see the remarks at the end of this
message).

The code uses & and >> in a way that really means / and %. Both
logical-operations-as-part-of-arithmetic-computations and division are
tricky for automatic provers, but if the formulation with logical
operations does not work, it may be worth trying the other one:

r->num[i] = ll % 0x100000000ULL;
ll = ll / 0x100000000ULL;


Assuming either version worked, it would be time to look at the loop
invariant that would eventually allow to tackle arbitrary values of BN_SIZE.

“loop assigns i, ll, r->num[0 .. BN_SIZE-1];” is correct and should not be
what prevents WP from reasoning about the loop, although it is also correct
to write “r->num[0 .. i-1]” instead of “r->num[0 .. BN_SIZE-1]”

Reference:
http://blog.frama-c.com/index.php?post/2010/10/06/Specification-of-loop-assigns

0 <= i <= BN_SIZE is an inductive invariant of the loop, but this
invariant, instantiated with i <- BN_SIZE and put together with i >=
BN_SIZE (the condition for exiting the loop), is not strong enough to prove
the property we would like to show after the loop.

The reason we expect the loop, when it exits, to have computed the sum of a
and b is that at the beginning of the i-th iteration (counting from zero),
ll times 2^(i*32) plus the first i words of r is the sum of the first i
words of a and the first i words of b. This is the property the loop needs
to be annotated with.

It is what makes the conclusion true, when the conclusion is true. And
thinking about the loop in this way brings forth a couple of remarks:

- this only works when there is sufficiently little aliasing between r and
a (resp. b). A sufficient condition is that they have no overlap at all,
that is, \separated(r, a) and \separated(r, b). Aliasing is a very annoying
notion when reasoning backwards on the program, and WP and Jessie handle it
differently. I would start by assuming the complete absence of overlap and
only after having proved correctness under this hypothesis would I move on
to the case where r overlaps with either or both.

- this only works when ll contains zero when the loop is exited. Otherwise,
the invariant does not imply the conclusion (in other words, the addition
overflows).

- speaking of ll, another inductive invariant is that ll < 0x100000000.
Without this additional property, the important property we want to express
about the partial sums is not inductive.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20151025/49101c01/attachment.html>