4 ms·

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

by wsxcde 12y ago

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/ 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?

nullc 12y ago
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. :)
- wsxcde 12y ago
  > 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.

by wsxcde 12y ago

nullc 12y ago

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. :)

wsxcde 12y ago
> 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.