4 ms·

> The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability tha

> The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods Model checking is great, and many tools developed by the model checking community are marvellous (especially the TLA+ model checker). But deductive methods scale well enough to definitively establish integrity and confidentiality for an entire OS kernel. They scale well enough to show that that said kernel has no in-kernel storage channels that can be exploited in a side channel attack. 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. These are deep properties. You're welcome to give examples of model checking or concolic testing establishing comparably deep properties of actual code of comparable length (not algorithm sketches or high-level system descriptions, actual code that compiles and runs). That's for deductive approaches in general. But sone of your specific claims about type theory are dubious as well. Elsewhere you claim that > The fact that even current formal verification research is mostly looking elsewhere seems to suggest that the answer is likely negative Your claim that formal methods research is mostly looking elsewhere is really stretching it. More researchers are doing type theory than ever. Grants are pouring in, some labs can offer 20+ PhD scholarships per year. The number of submissions to ICFP's TyDe track had over 30% growth last year. TYPES already dwarfs the biggest conferences devoted to model checking or any other specific formal method. No widely cited research aeticles express the sentiment that "type theory has failed and we should look elsewhere". No other subfields are ezperiencing comparable growth.

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.

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.