# 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

*Subject*: [Frama-c-discuss] Arbitrary size fixed integer math*From*: pascal.cuoq at gmail.com (Pascal Cuoq)*Date*: Sun, 25 Oct 2015 18:05:09 +0100*In-reply-to*: <20151024120430.GA20528@roeckx.be>*References*: <20151024120430.GA20528@roeckx.be>

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>

**Follow-Ups**:**[Frama-c-discuss] Arbitrary size fixed integer math***From:*kurt at roeckx.be (Kurt Roeckx)

**References**:**[Frama-c-discuss] Arbitrary size fixed integer math***From:*kurt at roeckx.be (Kurt Roeckx)

- Prev by Date:
**[Frama-c-discuss] Arbitrary size fixed integer math** - Next by Date:
**[Frama-c-discuss] Arbitrary size fixed integer math** - Previous by thread:
**[Frama-c-discuss] Arbitrary size fixed integer math** - Next by thread:
**[Frama-c-discuss] Arbitrary size fixed integer math** - Index(es):