3 ms·

@ pron This is a great write-up I learn quite a bit from but way, way, too long. There's a lot of redundancy in here much like my first sentence. You should tr

@ pron This is a great write-up I learn quite a bit from but way, way, too long. There's a lot of redundancy in here much like my first sentence. You should try to condense this since the redundancy might make a chunk of the modern crowd think the rest of what they see in the scrollbar will be the same and move on to next article. The last write-up you sent me didn't have that problem. I'm glad I saw this, too, as I recently watched your video citing all the mathematical evidence that correctness may not decompose. I got one or two counterpoints to email you later but overall want your data peer reviewed by people highly experienced in abstractions in large, verification efforts and making VCG's given their output will have to compose, too. Let all the pro's duke it out with arguments, proofs, and attempts at actual projects. I'll reserve judgment until the dust settles. :)

jacobparker 9y ago
> I recently watched your video citing all the mathematical evidence that correctness may not decompose For myself and others, are you referring to the video here: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity ?
- nickpsecurity 9y ago
  Yeah, that was it.
pron 9y ago
You are absolutely right about the repetition (and part 1 is my least favorite installment in the series), but reducing it in size took too much time. If you have any editing suggestions, please email me. As to the the "mathematical evidence", it is a published, peer reviewed, 2005 proof, and a rather simple one. Practical experience has little to do with it, because we need to separate two things: the computational complexity of the worst case -- which is provably exponential not only in the number of components but also in the size of the state space of each component -- and cases that arise in practice. This is just like the halting theorem, that states the worst-case undecidability, but does not claim that every instance is undecidable. However, the interesting question is how far are commonly encountered cases from the worst case. When it comes to symbolic model checking (i.e., taking advantage of syntactic structure), even though we would have thought the problem is essentially easier (in the worst case), it is provably just as hard, and moreover, we have years of experience (cited in my post) that common cases are close to the worst-case. When it comes to "decomposability of correctness", I cited no empirical evidence. Nevertheless, it should be noted that no large or even medium-sized software has ever been fully verified, so I don't think anyone believes the problem is easy.
- nickpsecurity 9y ago
  " it is a published, peer reviewed, 2005 proof, and a rather simple one." Proofs can be wrong or irrelevant in practice. An example is not being able to prove the tetmination of executing arbitrary programs. Sure I can: it's called a watch-dog timer. So, Im wanting it peer reviewed. Plus, it's critical to know for sure that and correctness composition to determine what to invest in for software assurance R&D. "Nevertheless, it should be noted that no large or even medium-sized software has ever been fully verified, so I don't think anyone believes the problem is easy." Never easy. :) However, I still think we should consider counting the deep verifications. You keep saying they havent went upward to verify a program of certain size as if it means something. I know only one that tried (Verisoft for Hyper-V). Most went downward toward the gate level including Verisoft where Microsoft's was just a side item. Verisoft did app correctness to some degree, down to C code, its compiler, the OS, the microkernel, and CPU tying it all together. DeepSpec just tied piles of high-level and low-level code together. So, such methods should allow us to achieve the same amount of complexity going upward using same abstraction and shortcut techniques. We havent done that much upward because they just been working the other way. Now, what they'll ultimately achieve may or may not be that good. Best approach might be to throw DeepSpec's DSL's and tooling at a large, complex application whose code is FOSS and accessible. I suggest an application server with compression, encryption, caching, and error handling as a good way to stress that project from multiple angles.
  - pron 9y ago
    > An example is not being able to prove the termination of executing arbitrary programs The theorem states that you cannot prove a program's termination any faster than running it. You're not violating any theorems. > So, Im wanting it peer reviewed. But it has been peer reviewed. Here is the publication http://www.sciencedirect.com/science/article/pii/S0022000005001297 http://www.sciencedirect.com/science/article/pii/S0022000005... in this journal https://en.wikipedia.org/wiki/Journal_of_Computer_and_System_Sciences https://en.wikipedia.org/wiki/Journal_of_Computer_and_System... > So, such methods should allow us to achieve the same amount of complexity going upward using same abstraction and shortcut techniques. First, I think you're misinterpreting (and exaggerating) what has actually been achieved. Looking at Hyper-V[1], 30KLOC of (preexisting and tested) C code have been verified in a year (out of a total of just 100KLOC), but only function-by-function, rather than global correctness properties. They wrote some global invariants, but didn't verify them. As I understand, such similar verification of various layers has been done, but no global end-to-end work. Whether low-level or high-level, there has been no composition across abstraction layers. Second, such methods would not allow us to go "upward", because there's a reason why people concentrate on the lower level. The state space is smaller there. Finally, I think you're also misinterpreting DeepSpec's work. It is at the forefront of verification of a certain kind, but if you look at their papers, when they talk about end-to-end verification, they're discussing programs that are 3KLOC C. These programs are smaller than many JavaScript libraries. Also, Coq is not really a tool engineers can put to everyday use. This is what Simon Pyton-Jones, one of Haskell's designers, has to say about Coq and Isabelle: https://youtu.be/re96UgMk6GQ?t=50m56s https://youtu.be/re96UgMk6GQ?t=50m56s Formal methods are starting to work, but we are roughly in the same stage as aviation in WWI, while you are talking about "using the same methods" to get a manned craft to Mars. We may well get there, but it will take a while, and the methods will not be exactly the same. [1]: http://d3s.mff.cuni.cz/research/seminar/download/2010-02-23-Tobies-HypervisorVerification.pdf http://d3s.mff.cuni.cz/research/seminar/download/2010-02-23-... and https://link.springer.com/chapter/10.1007/978-3-642-05089-3_51 https://link.springer.com/chapter/10.1007/978-3-642-05089-3_...

jacobparker 9y ago

> I recently watched your video citing all the mathematical evidence that correctness may not decompose For myself and others, are you referring to the video here: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity ?

nickpsecurity 9y ago
Yeah, that was it.

pron 9y ago

You are absolutely right about the repetition (and part 1 is my least favorite installment in the series), but reducing it in size took too much time. If you have any editing suggestions, please email me. As to the the "mathematical evidence", it is a published, peer reviewed, 2005 proof, and a rather simple one. Practical experience has little to do with it, because we need to separate two things: the computational complexity of the worst case -- which is provably exponential not only in the number of components but also in the size of the state space of each component -- and cases that arise in practice. This is just like the halting theorem, that states the worst-case undecidability, but does not claim that every instance is undecidable. However, the interesting question is how far are commonly encountered cases from the worst case. When it comes to symbolic model checking (i.e., taking advantage of syntactic structure), even though we would have thought the problem is essentially easier (in the worst case), it is provably just as hard, and moreover, we have years of experience (cited in my post) that common cases are close to the worst-case. When it comes to "decomposability of correctness", I cited no empirical evidence. Nevertheless, it should be noted that no large or even medium-sized software has ever been fully verified, so I don't think anyone believes the problem is easy.

nickpsecurity 9y ago
" it is a published, peer reviewed, 2005 proof, and a rather simple one." Proofs can be wrong or irrelevant in practice. An example is not being able to prove the tetmination of executing arbitrary programs. Sure I can: it's called a watch-dog timer. So, Im wanting it peer reviewed. Plus, it's critical to know for sure that and correctness composition to determine what to invest in for software assurance R&D. "Nevertheless, it should be noted that no large or even medium-sized software has ever been fully verified, so I don't think anyone believes the problem is easy." Never easy. :) However, I still think we should consider counting the deep verifications. You keep saying they havent went upward to verify a program of certain size as if it means something. I know only one that tried (Verisoft for Hyper-V). Most went downward toward the gate level including Verisoft where Microsoft's was just a side item. Verisoft did app correctness to some degree, down to C code, its compiler, the OS, the microkernel, and CPU tying it all together. DeepSpec just tied piles of high-level and low-level code together. So, such methods should allow us to achieve the same amount of complexity going upward using same abstraction and shortcut techniques. We havent done that much upward because they just been working the other way. Now, what they'll ultimately achieve may or may not be that good. Best approach might be to throw DeepSpec's DSL's and tooling at a large, complex application whose code is FOSS and accessible. I suggest an application server with compression, encryption, caching, and error handling as a good way to stress that project from multiple angles.
- pron 9y ago
  > An example is not being able to prove the termination of executing arbitrary programs The theorem states that you cannot prove a program's termination any faster than running it. You're not violating any theorems. > So, Im wanting it peer reviewed. But it has been peer reviewed. Here is the publication http://www.sciencedirect.com/science/article/pii/S0022000005001297 http://www.sciencedirect.com/science/article/pii/S0022000005... in this journal https://en.wikipedia.org/wiki/Journal_of_Computer_and_System_Sciences https://en.wikipedia.org/wiki/Journal_of_Computer_and_System... > So, such methods should allow us to achieve the same amount of complexity going upward using same abstraction and shortcut techniques. First, I think you're misinterpreting (and exaggerating) what has actually been achieved. Looking at Hyper-V[1], 30KLOC of (preexisting and tested) C code have been verified in a year (out of a total of just 100KLOC), but only function-by-function, rather than global correctness properties. They wrote some global invariants, but didn't verify them. As I understand, such similar verification of various layers has been done, but no global end-to-end work. Whether low-level or high-level, there has been no composition across abstraction layers. Second, such methods would not allow us to go "upward", because there's a reason why people concentrate on the lower level. The state space is smaller there. Finally, I think you're also misinterpreting DeepSpec's work. It is at the forefront of verification of a certain kind, but if you look at their papers, when they talk about end-to-end verification, they're discussing programs that are 3KLOC C. These programs are smaller than many JavaScript libraries. Also, Coq is not really a tool engineers can put to everyday use. This is what Simon Pyton-Jones, one of Haskell's designers, has to say about Coq and Isabelle: https://youtu.be/re96UgMk6GQ?t=50m56s https://youtu.be/re96UgMk6GQ?t=50m56s Formal methods are starting to work, but we are roughly in the same stage as aviation in WWI, while you are talking about "using the same methods" to get a manned craft to Mars. We may well get there, but it will take a while, and the methods will not be exactly the same. [1]: http://d3s.mff.cuni.cz/research/seminar/download/2010-02-23-Tobies-HypervisorVerification.pdf http://d3s.mff.cuni.cz/research/seminar/download/2010-02-23-... and https://link.springer.com/chapter/10.1007/978-3-642-05089-3_51 https://link.springer.com/chapter/10.1007/978-3-642-05089-3_...