6 ms·

Currently stuck between a rock and a hard place with things like this. Many of the other formal verification tools make it very easy to have your implementatio

Currently stuck between a rock and a hard place with things like this. Many of the other formal verification tools make it very easy to have your implementation drift or be entirely unmoored from your specification, but they let you keep working at a level of abstraction from your problem that's still very familiar. Though things like SMACK and DiVinE are helping to decrease the gap between spec and code. Using things like Coq + program extraction brings the overlap between spec and implementation into much, much closer alignment, but brings with it additional problems. Writing a complex program in a very abstract language further away from an engineer's typical problem domain, being fairly limited in types of languages supported for extraction, and/or still having to have an awful lot of faith in the extractor (which itself is unverified as near as I can tell) are all things that are currently keeping me out of Coq for immediate use cases. The good news though is that there's a lot of fairly high-profile work being done (like Verdi) to increasingly bring formal methods to increasingly complex software problems in ways that make using formal methods more approachable and usable, and that's truly wonderful.

nickpsecurity 9y ago
Try TLA+ (learntla.com) for concurrency, Alloy Analyzer for structure, and SPARK or Frama-C for code-level stuff. See if you can feed TLA+ or Alloy properties into stuff like SPARK. E-SPARK did that with Event-B. These are the low-hanging fruit for verification vs full build out in Coq or Isabelle. Then, you write checkers for it to apply testing like KLEE, property-based, or fuzz testing. These will get you close to full verification with less work. Each of the three languages has been used in a lots of CompSci and industrial work. Note that SPIN is similar to TLA+ and you can Google its industrial use for ideas of TLA+ power in concurrency analysis.
- pron 9y ago
  Java also has code-level specification language called JML, with a rich set of verification tools[1] (in fact, Frama-C's specification language, ACSL, was heavily inspired by JML). Also, if you know TLA+, there's little reason to learn Alloy as well, as TLA+ is a superset of its features (as well as of Event-B, and you can compile TLA+ to Event-B to use its tools[2]) SPIN is not so similar to TLA+, as its language, Promella, is relatively low-level, while TLA+ allows an arbitrary level of detail, and so is well suited to specify very large, very complex applications, rather than small, well-contained ones. Also, if you absolutely must write proofs and have the considerable resources, I believe that Promella requires proving in Isabelle (which takes a long time to learn), while TLA+ has its own user-friendly proof language that hides Isabelle under the covers. [1]: E.g. http://www.openjml.org/ http://www.openjml.org/ and there are others. [2]: https://www3.hhu.de/stups/prob/index.php/The_ProB_Animator_and_Model_Checker https://www3.hhu.de/stups/prob/index.php/The_ProB_Animator_a...
  - nickpsecurity 9y ago
    Re Alloy Most people that use these tools told me TLA+ and Alloy do different things with their automated tooling. They usually say TLA+ looks at ordering of things with Alloy looking at structuring. I only found a few people comparing them directly, though. Do you have a resource showing TLA+ does same thing as Alloy or as easily? Re SPIN Im saying they were used similarly. You wrote in one artocle like set theory, model-checking for temporal errors, and so on are new. That was the default in high-assurance decades ago using things like Z specs with SPIN for concurrency. Then, they tried to go for verifying high-level code, then rough code, code then assembly, and so on with refinement proofs. However, it started with algorithmic verification with specs in set theory, first-order logic, and ASM's. Writeups like yours tell me Lamport's concept was to similarly use those easier formalisms leaving off anything but the algorithm. Then add more automation to get more bang for buck for more developers. A good idea since the subset of that which Z and SPIN offered had already prevented serious, sometimes deep, errors in prior systems. Now, far as SPIN, it was used to chech the properties of concurrency models, hardware specs, caching, protocols, standards, and distributed systems. Industry found bugs in all these things using it with relatively little training vs other methods that required rare specialists. Sound familiar? TLA+ now shows up as tool of choice for quite a few of those areas with SPIN still used a lot due to maturity & being well-known. That's why I said they're similar: people are specifying and model checking similar things with them similarly with much less effort than provers. The easier proving on TLA+ and high-level nature are real benefits ovee SPIN. It's why I recommend TLA+. ;)
    - hwayne 9y ago
      The only in-depth study I know about is "Alloy meets TLA+".[1] Their conclusion was that Alloy is much more flexible and easier to use _unless_ your system is dynamic, because you have to manually model time in Alloy. [1] https://arxiv.org/pdf/1603.03599.pdf https://arxiv.org/pdf/1603.03599.pdf
    - pron 9y ago
      > Do you have a resource showing TLA+ does same thing as Alloy or as easily? See, Why Amazon Chose TLA+[1]. They found Alloy pleasant enough but a bit weirder than TLA+, and TLA+ is richer in terms of expressivity and features. I learned Alloy and played with it after knowing TLA+ well, and while I think it is an extremely nice and useful tool (although its syntax is indeed weird), it is absolutely trivial to express anything you can in Alloy in TLA+, and that's without even TLA (i.e., just the +). Their tooling is a bit different, so I guess there may be cases where Alloy would be more convenient even if you already know TLA+. > Im saying they were used similarly. ... Yeah. Deep formal methods are, in general, much more similar to one another than they are different. [1]: https://link.springer.com/chapter/10.1007/978-3-662-43652-3_3 https://link.springer.com/chapter/10.1007/978-3-662-43652-3_...
- palmskog 9y ago
  Design verification using TLA+ and Alloy is a completely different game than verification at the level of code as in Verdi. While there are plenty of studies saying design verification is good in general, I'm not aware of any studies saying that (or quantifying to what degree) it gets you close to implementation verification. On the flip side, the classic paper on the implementation of Paxos hints at just at how wide the gap is between design and running systems: https://research.google.com/archive/paxos_made_live.html https://research.google.com/archive/paxos_made_live.html While Frama-C style verification works well out-of-the-box for proving single-threaded, isolated programs correct, one has to make a major effort to capture assumption-heavy distributed systems behavior using ghost code and other tricks. The only effort I'm aware of in this direction is the following, which uses the VCC tool: http://madhu.cs.illinois.edu/evcons.pdf http://madhu.cs.illinois.edu/evcons.pdf
sanxiyn 9y ago
I don't think having to trust the extractor matters much in practice, since you need to trust the compiler for extracted program anyway. Compared to OCaml compiler, Coq-to-OCaml extractor is simple and small.
naasking 9y ago
> Writing a complex program in a very abstract language further away from an engineer's typical problem domain, being fairly limited in types of languages supported for extraction, and/or still having to have an awful lot of faith in the extractor (which itself is unverified as near as I can tell) are all things that are currently keeping me out of Coq for immediate use cases. Indeed, which is why I think something like Idris will probably be the future. We need to combine programming and theorem proving, and allow us to move the line incrementally closer to or further away from full verification as the problem evolves, becomes better understood, or new techniques emerge. Full verification for most programs is still too difficult, but we should be able verify what's feasible and use standard testing techniques for the rest. It will still be a huge leap towards real software engineering.
- pron 9y ago
  > Indeed, which is why I think something like Idris will probably be the future. I very much doubt it. I think other code-level specification languages (like JML for Java or ACSL for C), are much better suited to the configurable level of verification that you're looking for. The reason their tooling[1] is better than Idris's is not just because they're more mature, but for deeper reasons, too. While working in different formalisms (dependent types or direct logic) doesn't make much of a difference, when you specify in types, the lowest level of confidence you allow is formal proof, which, as you note, is beyond reach for anything but small and simple code. It doesn't make much of a difference whether you need to prove a JML specification or an Idris type, but a JML specification allows you to optionally use weaker but much cheaper forms of verification like concolic testing, regular test generation etc. OTOH, Idris already has test-generation libraries that require yet another form of specification, just because types won't work with anything less than proof. I heard you could achieve the same with types, but that requires enclosing the weakly-verified types in monads, so type T and type `Weak T` is not the same. Idris is one of many (I've lost count) of experiments in code-level formal verification. So far I don't see any indication it is closer to being "the future" than any of the multitude of other experiments. I don't think it's necessarily worse, either (while suffering from the problem I mentioned above, I assume it has advantages, too), but right now if you hear a lot about Idris it mostly means you hang around Haskellers, who have taken a liking to the language because of its similarity to Haskell in both spirit and style. [1]: See here for an example of some automated JML tools http://www.openjml.org/ http://www.openjml.org/, and here for semi-automated tools (using proof assistants) http://krakatoa.lri.fr/ http://krakatoa.lri.fr/
palmskog 9y ago
If you're looking for programs verified down to the machine code level, using C and the Verified Software Toolchain (VST) is one option. C programs are proven in the Hoare style (pre/postconditions) inside Coq, and then compiled using the verified CompCert compiler. Properties proven in Coq are guaranteed to hold about the compiled code. There is nothing fundamental to prevent using VST to prove Verdi handler code correct, but the current runtime is not set up for that workflow. http://vst.cs.princeton.edu http://vst.cs.princeton.edu
fmap 9y ago
Regarding extraction in Coq, there's certicoq: http://www.cs.princeton.edu/~appel/certicoq/ http://www.cs.princeton.edu/~appel/certicoq/ Granted, there's a lot of engineering work left to do, but it's moving in the right direction.

nickpsecurity 9y ago

Try TLA+ (learntla.com) for concurrency, Alloy Analyzer for structure, and SPARK or Frama-C for code-level stuff. See if you can feed TLA+ or Alloy properties into stuff like SPARK. E-SPARK did that with Event-B. These are the low-hanging fruit for verification vs full build out in Coq or Isabelle. Then, you write checkers for it to apply testing like KLEE, property-based, or fuzz testing. These will get you close to full verification with less work. Each of the three languages has been used in a lots of CompSci and industrial work. Note that SPIN is similar to TLA+ and you can Google its industrial use for ideas of TLA+ power in concurrency analysis.

pron 9y ago
Java also has code-level specification language called JML, with a rich set of verification tools[1] (in fact, Frama-C's specification language, ACSL, was heavily inspired by JML). Also, if you know TLA+, there's little reason to learn Alloy as well, as TLA+ is a superset of its features (as well as of Event-B, and you can compile TLA+ to Event-B to use its tools[2]) SPIN is not so similar to TLA+, as its language, Promella, is relatively low-level, while TLA+ allows an arbitrary level of detail, and so is well suited to specify very large, very complex applications, rather than small, well-contained ones. Also, if you absolutely must write proofs and have the considerable resources, I believe that Promella requires proving in Isabelle (which takes a long time to learn), while TLA+ has its own user-friendly proof language that hides Isabelle under the covers. [1]: E.g. http://www.openjml.org/ http://www.openjml.org/ and there are others. [2]: https://www3.hhu.de/stups/prob/index.php/The_ProB_Animator_and_Model_Checker https://www3.hhu.de/stups/prob/index.php/The_ProB_Animator_a...
- nickpsecurity 9y ago
  Re Alloy Most people that use these tools told me TLA+ and Alloy do different things with their automated tooling. They usually say TLA+ looks at ordering of things with Alloy looking at structuring. I only found a few people comparing them directly, though. Do you have a resource showing TLA+ does same thing as Alloy or as easily? Re SPIN Im saying they were used similarly. You wrote in one artocle like set theory, model-checking for temporal errors, and so on are new. That was the default in high-assurance decades ago using things like Z specs with SPIN for concurrency. Then, they tried to go for verifying high-level code, then rough code, code then assembly, and so on with refinement proofs. However, it started with algorithmic verification with specs in set theory, first-order logic, and ASM's. Writeups like yours tell me Lamport's concept was to similarly use those easier formalisms leaving off anything but the algorithm. Then add more automation to get more bang for buck for more developers. A good idea since the subset of that which Z and SPIN offered had already prevented serious, sometimes deep, errors in prior systems. Now, far as SPIN, it was used to chech the properties of concurrency models, hardware specs, caching, protocols, standards, and distributed systems. Industry found bugs in all these things using it with relatively little training vs other methods that required rare specialists. Sound familiar? TLA+ now shows up as tool of choice for quite a few of those areas with SPIN still used a lot due to maturity & being well-known. That's why I said they're similar: people are specifying and model checking similar things with them similarly with much less effort than provers. The easier proving on TLA+ and high-level nature are real benefits ovee SPIN. It's why I recommend TLA+. ;)
  - hwayne 9y ago
    The only in-depth study I know about is "Alloy meets TLA+".[1] Their conclusion was that Alloy is much more flexible and easier to use _unless_ your system is dynamic, because you have to manually model time in Alloy. [1] https://arxiv.org/pdf/1603.03599.pdf https://arxiv.org/pdf/1603.03599.pdf
  - pron 9y ago
    > Do you have a resource showing TLA+ does same thing as Alloy or as easily? See, Why Amazon Chose TLA+[1]. They found Alloy pleasant enough but a bit weirder than TLA+, and TLA+ is richer in terms of expressivity and features. I learned Alloy and played with it after knowing TLA+ well, and while I think it is an extremely nice and useful tool (although its syntax is indeed weird), it is absolutely trivial to express anything you can in Alloy in TLA+, and that's without even TLA (i.e., just the +). Their tooling is a bit different, so I guess there may be cases where Alloy would be more convenient even if you already know TLA+. > Im saying they were used similarly. ... Yeah. Deep formal methods are, in general, much more similar to one another than they are different. [1]: https://link.springer.com/chapter/10.1007/978-3-662-43652-3_3 https://link.springer.com/chapter/10.1007/978-3-662-43652-3_...
palmskog 9y ago
Design verification using TLA+ and Alloy is a completely different game than verification at the level of code as in Verdi. While there are plenty of studies saying design verification is good in general, I'm not aware of any studies saying that (or quantifying to what degree) it gets you close to implementation verification. On the flip side, the classic paper on the implementation of Paxos hints at just at how wide the gap is between design and running systems: https://research.google.com/archive/paxos_made_live.html https://research.google.com/archive/paxos_made_live.html While Frama-C style verification works well out-of-the-box for proving single-threaded, isolated programs correct, one has to make a major effort to capture assumption-heavy distributed systems behavior using ghost code and other tricks. The only effort I'm aware of in this direction is the following, which uses the VCC tool: http://madhu.cs.illinois.edu/evcons.pdf http://madhu.cs.illinois.edu/evcons.pdf

sanxiyn 9y ago

I don't think having to trust the extractor matters much in practice, since you need to trust the compiler for extracted program anyway. Compared to OCaml compiler, Coq-to-OCaml extractor is simple and small.

naasking 9y ago

> Writing a complex program in a very abstract language further away from an engineer's typical problem domain, being fairly limited in types of languages supported for extraction, and/or still having to have an awful lot of faith in the extractor (which itself is unverified as near as I can tell) are all things that are currently keeping me out of Coq for immediate use cases. Indeed, which is why I think something like Idris will probably be the future. We need to combine programming and theorem proving, and allow us to move the line incrementally closer to or further away from full verification as the problem evolves, becomes better understood, or new techniques emerge. Full verification for most programs is still too difficult, but we should be able verify what's feasible and use standard testing techniques for the rest. It will still be a huge leap towards real software engineering.

pron 9y ago
> Indeed, which is why I think something like Idris will probably be the future. I very much doubt it. I think other code-level specification languages (like JML for Java or ACSL for C), are much better suited to the configurable level of verification that you're looking for. The reason their tooling[1] is better than Idris's is not just because they're more mature, but for deeper reasons, too. While working in different formalisms (dependent types or direct logic) doesn't make much of a difference, when you specify in types, the lowest level of confidence you allow is formal proof, which, as you note, is beyond reach for anything but small and simple code. It doesn't make much of a difference whether you need to prove a JML specification or an Idris type, but a JML specification allows you to optionally use weaker but much cheaper forms of verification like concolic testing, regular test generation etc. OTOH, Idris already has test-generation libraries that require yet another form of specification, just because types won't work with anything less than proof. I heard you could achieve the same with types, but that requires enclosing the weakly-verified types in monads, so type T and type `Weak T` is not the same. Idris is one of many (I've lost count) of experiments in code-level formal verification. So far I don't see any indication it is closer to being "the future" than any of the multitude of other experiments. I don't think it's necessarily worse, either (while suffering from the problem I mentioned above, I assume it has advantages, too), but right now if you hear a lot about Idris it mostly means you hang around Haskellers, who have taken a liking to the language because of its similarity to Haskell in both spirit and style. [1]: See here for an example of some automated JML tools http://www.openjml.org/ http://www.openjml.org/, and here for semi-automated tools (using proof assistants) http://krakatoa.lri.fr/ http://krakatoa.lri.fr/

palmskog 9y ago

If you're looking for programs verified down to the machine code level, using C and the Verified Software Toolchain (VST) is one option. C programs are proven in the Hoare style (pre/postconditions) inside Coq, and then compiled using the verified CompCert compiler. Properties proven in Coq are guaranteed to hold about the compiled code. There is nothing fundamental to prevent using VST to prove Verdi handler code correct, but the current runtime is not set up for that workflow. http://vst.cs.princeton.edu http://vst.cs.princeton.edu

fmap 9y ago

Regarding extraction in Coq, there's certicoq: http://www.cs.princeton.edu/~appel/certicoq/ http://www.cs.princeton.edu/~appel/certicoq/ Granted, there's a lot of engineering work left to do, but it's moving in the right direction.