3 ms·

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

by 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 nullc 12y ago

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.