Hacker News new | comments | show | ask | jobs | submit login

The proof appears to be incorrect.

Consider the case where c2,c1,c0 are all UINT_MAX.

In OpenSSL that can't be the case because the outside environment constrains the accumulator; but I see nothing on that page showing such a constraint there.

I'm not familiar with the z3 python interface, clearly something interesting implicit must be going on there. (As it does appear to be expressing that the values are finitely ranged, and doesn't appear to be expressing a constraint for ref)

In general I've had bad luck getting results out of SMT solvers on finite ranged problems-- often they just get stuck. If you can ensure there is no overflow then its easier, but then again it's also easer to reason about them absent the mechanical prover in that case too.

The other major hurdles is extracting the code in a way that can be usefully presented to solvers without a lot of potential for human error or extreme effort (e.g. OpenSSL is 400k lines of code, good luck with making progress if you're hand rewriting things for the prover). Frama-C (http://frama-c.com/) can help with this and I've used it to good effect on very small pieces of code.

Hopefully in the future we'll see more programming languages with better accordances for using formal methods-- ATS is pretty interesting in that respect--, and also bridging the usability gap enough to see them widely used in industry.




The proof is implicitly modulo 2^96, which I believed to be the intention of the original code, but it does miss a possible overflow when c is too large, which shouldn't happen in its intended use: c2 is already meant to be the overflow limb. I've added an addendum to the post describing, and fixing, this.


Thanks!

One of the things I find useful for avoiding overconfidence in proof results, beyond making sure to test the proof on multiple broken versions, is to spell out many additional implications of the function that I and/or the caller might expect of it and ask for proofs on them too, even if they seem somewhat redundant.

For example, cout = 2ab + cin; I would also prove that for all a,b,cin that cout >= cin; for a or b ==0 that cout == cin, etc.


Help me understand your objection with the proof. Are you saying that the set of values c2, c1, c0, a, b can take in OpenSSL is a subset of the values that they can take in the SMT formulation? Why does this invalidate the proof, though?

Edit: In response to this edit of yours:

> The other major hurdles is extracting the code in a way that can be usefully presented to solvers without a lot of potential for human error or extreme effort (e.g. OpenSSL is 400k lines of code, good luck with making progress if you're hand rewriting things for the prover). Frama-C (http://frama-c.com/) can help with this and I've used it to good effect on very small pieces of code.

Not even the most hardcore formal verification supporter will suggest a complete verification suite based on automated verification tools. Generally, you pick a subset of the code that is critical, poorly understood and is amenable to formal verification and expend some effort in proving properties about it. There's obviously a lot of subjective judgement here both in choosing the subset of the code you want to look as well what properties you attempt to prove. But that's what we get paid for, right?


The function in OpenSSL would be incorrect if it were asked to work on the full range of possible inputs. E.g. in my trivial example if the accumulator (C_n) at the maximum value, it would overflow for any non-zero input, and wrap around and give an incorrect result.

OpenSSL doesn't demand that of the function-- the ranges of the inputs are limited-- but nothing in the z3py example on the page appears to express that precondition. If OpenSSL's demands were different the code would be incorrect, but it passes the verification.

> in proving properties about it

In proving something about something. :) If the process involves hand transcribing the code ... well. I don't say to argue that this isn't interesting or useful.

I use formal methods some in my own development and would like to use them more heavily. But I've found that the state of the tools right now is exceptionally limited: A lot of effort, to prove very narrow properties-- ones which might be misleading about the correctness of the software, on models which may not well match the actual software, and which gives assurance that rots a bit over time because it's not sufficiently automatic.

In spite of these things, if we don't apply formal tools I believe we'll never be able to escape the orgy of failure that we have with software today. But it's best to go in with eyes wide open. :)


> in my trivial example if the accumulator (C_n) at the maximum value, it would overflow for any non-zero input

Depends on what you mean by "incorrect". :)

The SMT formulation isn't doing infinite precision arithmetic. It's just proving that the result computed by (the SMT encoding of) the C macro is equivalent to the 64-bit SMT bitvector defined by "Concat(c2, c1, c0) + 2 * ZeroExt(2W, a) ZeroExt(2W, b)".

> A lot of effort, to prove very narrow properties-- ones which might be misleading about the correctness of the software, on models which may not well match the actual software, and which gives assurance that rots a bit over time because it's not sufficiently automatic.*

To some extent, I agree with you. It is a little difficult to find off-the-shelf tools that work well directly on the source code, especially for software. But I think it's a just a matter of time before these issues are resolved. The hardware scenario has certainly improved in leaps and bounds. A group I've worked with has been somewhat successful in pushing the use of the JasperGold model checker at Intel, and I've heard quite a few people with no background in using formal tools tell me that they're happy with the tool and are much more confident in their code thanks to use of this tool.




Applications are open for YC Winter 2018

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | DMCA | Apply to YC | Contact

Search: