4 ms·

> But deductive methods scale well enough to definitively establish integrity and confidentiality for an entire OS kernel. ... Deductive methods scale well enou

by pron 7y ago

> But deductive methods scale well enough to definitively establish integrity and confidentiality for an entire OS kernel. ... Deductive methods scale well enough to verify (completely automaticallly, without human intervention) that the compiled binaries faithfully implement a given C program, so the compiler and linker need not be trusted. Unfortunately, they do not. The two projects you mentioned are positively tiny -- they correspond to about 10KLOC of C, or less than 1/5th the size of jQuery -- and they each took world experts years of effort. Both, BTW, required serious limitations in the algorithms used to keep them simple. That's like saying that transmuting lead into gold scales well because we can transmute ten gold atoms in a billion-dollar particle accelerator. > You're welcome to give examples of model checking or concolic testing establishing comparably deep properties of actual code of comparable length Concolic tests are unsound, which is why they scale so well. Model checking routinely verifies much larger codebases, so much so that people don't bothering writing papers about it. When deductive methods are used to verify a 10KLOC program that's news. You can buy off-the-shelf model checkers that do more in industry pretty much all the time. > More researchers are doing type theory than ever. Grants are pouring in, some labs can offer 20+ PhD scholarships per year. Perhaps, but when you look at FM conferences, deductive methods in general and type systems in particular are significantly more represented. > No widely cited research aeticles express the sentiment that "type theory has failed and we should look elsewhere" There's no need to abandon something that has yet to break through in the first place. Most FM research is just done elsewhere. > No other subfields are ezperiencing comparable growth. Automated methods are.

saithound 7y ago
> You can buy off-the-shelf model checkers that do more in industry pretty much all the time. When you establish actual deep properties, that's news. You can't buy any model checker that verifies confidentiality for actual kernels. At all. There is no such model checker. Again, if non-deductive formal methods are routinely used to establish comparably deep properties of programs of comparable size (as you claim), you should have no trouble naming at least one example. You don't need research papers to justify that claim, just a few statements of the form "Global Property P of 10k line C Program Q was established by model checker R". > That's like saying that transmuting lead into gold scales well because we can transmute ten gold atoms in a billion-dollar particle accelerator. No, not really. NICTA kept tabs on this, and got that producing seL4 costs about 50% more per line of code than other commercial L4 microkernels. While that is a significant expense, there is no order of magnitude difference, much less something in the "billion dollar particle accelerator" territory. Especially since it delivered global correctness properties that are out of reach for any other method.
- pron 7y ago
  > you should have no trouble naming at least one example. Model checkers don't usually beat deductive proofs in both size and depth, but they often easily beat them on any one of these. In terms of code size, model checkers have verified reachability on C programs of over 50KLOC in less than an hour for at least 15 years now (BLAST). Some bugs found in the past few years Linux kernel with a model checker are here: http://linuxtesting.org/results/ldv-cpachecker http://linuxtesting.org/results/ldv-cpachecker In terms of depth -- there are too many to choose from. Both SCADE and Simulink are routinely used in industry to verify LTL. TLC, a model checker for TLA+ was used to develop and verify deep properties of the OpenComRTOS kernel https://en.wikipedia.org/wiki/OpenComRTOS https://en.wikipedia.org/wiki/OpenComRTOS > You can't buy any model checker that verifies confidentiality for actual kernels. At all. There is no such model checker. There is no real method like this of any kind. A heroic effort by teams of PhD candidate proof monkeys working for some years isn't a technique. > not really. NICTA kept tabs on this, and got that producing seL4 costs about 50% more per line of code than other commercial L4 microkernels. I don't know what the cost of producing commercial L4 microkernels, but that 10KLOC program took 12 person years, plus another 12 for tooling. 2 years per KLOC, and even half of that, is well beyond the reach of 99% of software, plus no one has ever managed to use deductive verification for programs that are significantly larger than that in any amount of time. That's about three (!) orders of magnitude behind ordinary business software. This gap has remained pretty much constant over the last forty years. I think it is possible that deductive proofs may become viable in industry in some high-assurance, high-cost domains, provided that the programs are very small. But there is no sign that it could reasonably be a basis for increasing correctness of more ordinary software.
  - saithound 7y ago
    TLC checks models, not implementations, so the compariaon is not really appropriate at all. Using TLA+ on actual code is yet to be a success story: Deductive methods the assembly refinement proof of seL4 (binary verification) is completely automated, and takes less than two hours on a modern PC. OpenComRTOS is much much smaller and simpler than seL4 (comparable to eChronos). It's important work, and a neat example at how formal modeling allows one to _design better products_ even in well-explored domains, but it's a really poor example for illustrating the supposed scalability of model checking compared to deductive methods. Especially ehen the book on the system emphasizes how they kept experiencing state explosions which broke the checker during development. In any case, TLC checks specifications, not implementations; it's not appropriate to compare them to deductive methods that work on actual source code (cf. the properties of the _specification_ account for less than 5% of total proof obligations, and establish global properties that are stronger and deeper than model checking could provide). Attempts to use TLA+ on implementations such as C2TLA+ are far less successful, it's not been demonstrated to scale well (no case studies above 1 kloc at all). Writing and checking specifications is useful, and leads to more reliable software, and you're free to argue that there is far more low-hanging fruit to be found in this area than in dependent type systems. But it's not the same as checking 50kloc _programs_, and you should not conflate these activiities. Not to say that many deductive tools are completely automated and have been shown to work at scale too: SydTV verifies the correspondence between thr seL4 binary and the corresponding sourcr in under two hours on a modern PC. And what you're competing against (dependent types) has the potential to scale far better: even the 3.5kloc Agda program I'm working on can be checked in under a minute, and Agda is very far from optimal with respect to type checking. > But there is no sign that it could reasonably be a basis for increasing correctness of more ordinary software. You're entitled to that opinion. Just don't conflate that with general trends and sentiments in the formal methods community. Contrary to your earlier claims, there is no agreement in the field that one should "look elsewhere". The same goes for your claim that non-deductive techniques scale better and establish deeper properties than deductive ones: if you believe this will be shown decisively true in the future, that's a perfectly alright opinion to have, and you'll find plenty of peiple who share it. But don't act as if it's an empirical fact when the evidence shows no such scalability advantage at this point in time, and most deep properties that deductive, proof-producing methods can establish are still out of reach for non-deductive methods. (ps. Writing these posts took me a lot of time, so I'll have to limit myself to one more comment in this thread.)

by pron 7y ago

saithound 7y ago

> You can buy off-the-shelf model checkers that do more in industry pretty much all the time. When you establish actual deep properties, that's news. You can't buy any model checker that verifies confidentiality for actual kernels. At all. There is no such model checker. Again, if non-deductive formal methods are routinely used to establish comparably deep properties of programs of comparable size (as you claim), you should have no trouble naming at least one example. You don't need research papers to justify that claim, just a few statements of the form "Global Property P of 10k line C Program Q was established by model checker R". > That's like saying that transmuting lead into gold scales well because we can transmute ten gold atoms in a billion-dollar particle accelerator. No, not really. NICTA kept tabs on this, and got that producing seL4 costs about 50% more per line of code than other commercial L4 microkernels. While that is a significant expense, there is no order of magnitude difference, much less something in the "billion dollar particle accelerator" territory. Especially since it delivered global correctness properties that are out of reach for any other method.

pron 7y ago
> you should have no trouble naming at least one example. Model checkers don't usually beat deductive proofs in both size and depth, but they often easily beat them on any one of these. In terms of code size, model checkers have verified reachability on C programs of over 50KLOC in less than an hour for at least 15 years now (BLAST). Some bugs found in the past few years Linux kernel with a model checker are here: http://linuxtesting.org/results/ldv-cpachecker http://linuxtesting.org/results/ldv-cpachecker In terms of depth -- there are too many to choose from. Both SCADE and Simulink are routinely used in industry to verify LTL. TLC, a model checker for TLA+ was used to develop and verify deep properties of the OpenComRTOS kernel https://en.wikipedia.org/wiki/OpenComRTOS https://en.wikipedia.org/wiki/OpenComRTOS > You can't buy any model checker that verifies confidentiality for actual kernels. At all. There is no such model checker. There is no real method like this of any kind. A heroic effort by teams of PhD candidate proof monkeys working for some years isn't a technique. > not really. NICTA kept tabs on this, and got that producing seL4 costs about 50% more per line of code than other commercial L4 microkernels. I don't know what the cost of producing commercial L4 microkernels, but that 10KLOC program took 12 person years, plus another 12 for tooling. 2 years per KLOC, and even half of that, is well beyond the reach of 99% of software, plus no one has ever managed to use deductive verification for programs that are significantly larger than that in any amount of time. That's about three (!) orders of magnitude behind ordinary business software. This gap has remained pretty much constant over the last forty years. I think it is possible that deductive proofs may become viable in industry in some high-assurance, high-cost domains, provided that the programs are very small. But there is no sign that it could reasonably be a basis for increasing correctness of more ordinary software.
- saithound 7y ago
  TLC checks models, not implementations, so the compariaon is not really appropriate at all. Using TLA+ on actual code is yet to be a success story: Deductive methods the assembly refinement proof of seL4 (binary verification) is completely automated, and takes less than two hours on a modern PC. OpenComRTOS is much much smaller and simpler than seL4 (comparable to eChronos). It's important work, and a neat example at how formal modeling allows one to _design better products_ even in well-explored domains, but it's a really poor example for illustrating the supposed scalability of model checking compared to deductive methods. Especially ehen the book on the system emphasizes how they kept experiencing state explosions which broke the checker during development. In any case, TLC checks specifications, not implementations; it's not appropriate to compare them to deductive methods that work on actual source code (cf. the properties of the _specification_ account for less than 5% of total proof obligations, and establish global properties that are stronger and deeper than model checking could provide). Attempts to use TLA+ on implementations such as C2TLA+ are far less successful, it's not been demonstrated to scale well (no case studies above 1 kloc at all). Writing and checking specifications is useful, and leads to more reliable software, and you're free to argue that there is far more low-hanging fruit to be found in this area than in dependent type systems. But it's not the same as checking 50kloc _programs_, and you should not conflate these activiities. Not to say that many deductive tools are completely automated and have been shown to work at scale too: SydTV verifies the correspondence between thr seL4 binary and the corresponding sourcr in under two hours on a modern PC. And what you're competing against (dependent types) has the potential to scale far better: even the 3.5kloc Agda program I'm working on can be checked in under a minute, and Agda is very far from optimal with respect to type checking. > But there is no sign that it could reasonably be a basis for increasing correctness of more ordinary software. You're entitled to that opinion. Just don't conflate that with general trends and sentiments in the formal methods community. Contrary to your earlier claims, there is no agreement in the field that one should "look elsewhere". The same goes for your claim that non-deductive techniques scale better and establish deeper properties than deductive ones: if you believe this will be shown decisively true in the future, that's a perfectly alright opinion to have, and you'll find plenty of peiple who share it. But don't act as if it's an empirical fact when the evidence shows no such scalability advantage at this point in time, and most deep properties that deductive, proof-producing methods can establish are still out of reach for non-deductive methods. (ps. Writing these posts took me a lot of time, so I'll have to limit myself to one more comment in this thread.)