3 ms·

OpenSSL's squaring bug, and opportunistic formal verification

25 points by jsnell 12y ago

nullc 12y ago
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/ 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.
- 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.
- klogic 12y ago
  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.
  - nullc 12y ago
    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.
nanolith 12y ago
Beautiful. Formal verification does take more time over empirical testing methods such as unit testing, but when it comes to mission critical components such as cryptography or system code, this is time well spent.
- wsxcde 12y ago
  edit: just to be clear, I'm responding to this statement: > Formal verification does take more time over empirical testing methods I don't even know if that is true, at least, I'm unconvinced about it being true in hardware verification. The amount of manpower and effort companies like Intel and AMD put into simulation-based verification is insane and a lot of that could be replaced (and has in some case been replaced) by a well-designed formal assertion suite. The real bottleneck is people. It's a lot easier to find competent engineers who can hack around with tests and simulation suites than it is to find people who can hack around with abstractions for scalability in a model checker.
  - nanolith 12y ago
    There is a pragmatic perspective and a theoretic perspective. Pragmatically speaking, empirical methods can get one pretty far. It's better to have full coverage of empirical tests across an entire system than limited coverage of formal tests, for instance. So, on that account, you may be correct from a pragmatic perspective. From an epistemological perspective, a test suite to confirm a property using chosen examples is not nearly as good as a formal proof that guarantees a property over a given domain. For simple cases, such as branch coverage, the test suite may be good enough. As complexity increases, or when testing things like modular arithmetic over an elliptic curve, unit testing leads to false confidence. But, just like in empirical testing, it's possible to build bad proofs. This is where the specialization comes in. There may be plenty of competent engineers who can hack at a test suite, but their results will not be nearly as comprehensive as someone trained in formal verification. It all comes down to epistemology. What do we know, and how do we know it? What possible defects exist in our system, and how bad can they be? Can we ship yet?
    - 12y ago

25 points by jsnell 12y ago

nullc 12y ago

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

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

nanolith 12y ago

Beautiful. Formal verification does take more time over empirical testing methods such as unit testing, but when it comes to mission critical components such as cryptography or system code, this is time well spent.

wsxcde 12y ago
edit: just to be clear, I'm responding to this statement: > Formal verification does take more time over empirical testing methods I don't even know if that is true, at least, I'm unconvinced about it being true in hardware verification. The amount of manpower and effort companies like Intel and AMD put into simulation-based verification is insane and a lot of that could be replaced (and has in some case been replaced) by a well-designed formal assertion suite. The real bottleneck is people. It's a lot easier to find competent engineers who can hack around with tests and simulation suites than it is to find people who can hack around with abstractions for scalability in a model checker.
- nanolith 12y ago
  There is a pragmatic perspective and a theoretic perspective. Pragmatically speaking, empirical methods can get one pretty far. It's better to have full coverage of empirical tests across an entire system than limited coverage of formal tests, for instance. So, on that account, you may be correct from a pragmatic perspective. From an epistemological perspective, a test suite to confirm a property using chosen examples is not nearly as good as a formal proof that guarantees a property over a given domain. For simple cases, such as branch coverage, the test suite may be good enough. As complexity increases, or when testing things like modular arithmetic over an elliptic curve, unit testing leads to false confidence. But, just like in empirical testing, it's possible to build bad proofs. This is where the specialization comes in. There may be plenty of competent engineers who can hack at a test suite, but their results will not be nearly as comprehensive as someone trained in formal verification. It all comes down to epistemology. What do we know, and how do we know it? What possible defects exist in our system, and how bad can they be? Can we ship yet?
  - 12y ago