The Case for Formal Verification (2013) • Hacker News Board

Re: The Case for Formal Verification (2013)

#41

Post by CHY872 » Mon, Apr 21, 2014, 12:57 AM UTC

wsxcde wrote: post #24

Coq is an interactive theorem-prover, which is exactly what it sounds like. You prove your theorems more or less by typing out the proofs and the system mechanically verifies that each step in your proof is sound. I've used Coq and I'll be honest. This is unquestionably a solid way to prove things about your program but it is too much of pain to expect this to have significant adoption in the "real" world. In the har…

The state explosion problem is becoming less of an issue in software nowadays because of the massive improvement in SAT/SMT solvers. The topic of this post is not about model checking, but I believe still interesting.

One big improvement when it came to verification came from symbolic execution [1], in which the verifier looks for assertion violations by representing variables as a set of constraints. At each assertion, the constraints are checked to see if they can be negatively satisfied, giving a counterexample for the error. We run the program in a special interpreter (or using some interesting metaprogramming and a compiler frontend etc) and at each conditional statement a new constraint is added, leading to a tree. By cleverly picking branches etc we hopefully drastically reduce the search space.

This reduced the state explosion problem in many cases, but obviously there's now an explosion on the control flow. A more recent improvement has been to unwind loops a bound number of times, encoding the whole program as a logical statement that is only satisfied by input that will trigger an assertion error. The hypothesis is that the structure of such formulas is well simplified by SAT solvers, and this has been borne out empirically from what I know. We can further improve by natively executing that code which is not constrained, which is a further boon - in principle we could instrument a program to simply return the formula that (if satisfied) produces counterexamples.

This sort of approach is very useful in practice because it's very understandable to software engineers - in the ideal case where a large company produces a product based on it, one might reasonably expect to be able to pass the software their source code and be presented with a series of counterexamples. It's all very interesting.

(I'm not an expert on this, take what I say with a pinch of salt).

[1] https://klee.github.io/klee/

Re: The Case for Formal Verification (2013)

#42

Post by vilhelm_s » Mon, Apr 21, 2014, 1:06 AM UTC

dkarapetyan wrote: post #28

comex wrote: post #23

Somewhat off topic and very speculative, but I'm curious how feasible it would be to propagate safety proofs through compilation - not just formulaic memory safety rules but hopefully also arbitrary behavioral proofs - all the way down from a source language to machine code, so that essential properties could be formally verified without needing to either trust a compiler or use a provably correct one, in the latter…

What exactly is doing the verification? Another program, no? In which case why would you trust that program any more than the compiler that generated the machine code? At some point you must trust something to be correct. Whether that's the compiler or something else doesn't really change anything.

The idea is to minimize the trusted computing base---a compiler and runtime system for a high level language is a big and complicated system, so it is very hard to get it right, but a proof checker can be small so it is easier to be confident that it is correct. (This idea is also known as the "de Bruijn criterion").

Re: The Case for Formal Verification (2013)

#43

Post by dkarapetyan » Mon, Apr 21, 2014, 1:06 AM UTC

stormbrew wrote: post #40

dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

I find it strange to think that TDD and formal verification are at odds with each other. For it to be backwards to write dynamic tests, you seem to be suggesting that it is actually worse than doing neither. I also don't see how it can be documentation, glorified or otherwise, and not tell you anything about the properties of the software. Really there are perhaps three practical levels of knowledge about what a piec…

Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z? You can sample as many points as you want and you'll still be no wiser as to how + behaves and how it interacts with * or that the implementation of + even respects any of those properties. If you're going to put in the effort to generate unit tests then why not go a bit further and formally verify the correct functionality?

All this is just a roundabout way of saying I don't write unit tests. There is no value in it when I have convinced myself each subcomponent is correct and that composition of those subcomponents preserves correctness. You can write all the unit tests in the world and if you don't verify that the composition of your components preserves the correctness properties those tests are meant to verify then you might as well not have written those tests because now you have created a false sense of security.

If you can verify the kernel pieces of your code and then the composition mechanisms then you're done. You don't need to verify the entire thing as long as the entire thing is built with the kernel pieces and verified composition mechanisms that preserve correctness.

I also suspect we are still talking about separate classes of software. For your run of the mill twitter clone if it makes the corporate overlords happy then write as many unit tests as you want because it doesn't make a difference either way. But if we're talking about actual fundamental software like OS kernels and compilers then I don't think you can have enough formal verification.

Re: The Case for Formal Verification (2013)

#44

Post by [deleted] » Mon, Apr 21, 2014, 1:11 AM UTC

dkarapetyan wrote: post #43

stormbrew wrote: post #40

Earlier quoted context omitted.

I find it strange to think that TDD and formal verification are at odds with each other. For it to be backwards to write dynamic tests, you seem to be suggesting that it is actually worse than doing neither. I also don't see how it can be documentation, glorified or otherwise, and not tell you anything about the properties of the software. Really there are perhaps three practical levels of knowledge about what a piec…

Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z? You can sample as many points as you want and you'll still be no wiser as to how + behaves and how it interacts with * or that the implementation of + even respects any of those properties. If you're going to put in the effo…

[deleted]

Re: The Case for Formal Verification (2013)

#45

Post by stormbrew » Mon, Apr 21, 2014, 1:11 AM UTC

dkarapetyan wrote: post #43

stormbrew wrote: post #40

Earlier quoted context omitted.

I find it strange to think that TDD and formal verification are at odds with each other. For it to be backwards to write dynamic tests, you seem to be suggesting that it is actually worse than doing neither. I also don't see how it can be documentation, glorified or otherwise, and not tell you anything about the properties of the software. Really there are perhaps three practical levels of knowledge about what a piec…

Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z? You can sample as many points as you want and you'll still be no wiser as to how + behaves and how it interacts with * or that the implementation of + even respects any of those properties. If you're going to put in the effo…

> If you're going to put in the effort to generate unit tests then why not go a bit further and formally verify the correct functionality?

At the moment this "a bit further" is a bit like saying if you don't like the price of milk at your corner store, why don't you go to a farm to get a quart? Sure, you might be able to do that, but it's not exactly a comparable effort.

Re: The Case for Formal Verification (2013)

#46

Post by ahomescu1 » Mon, Apr 21, 2014, 1:16 AM UTC

nullc wrote: post #26

ahomescu1 wrote: post #6

Earlier quoted context omitted.

It doesn't support all of C99 [1]. In real-world code, you need that, plus the GNU extensions (the clang developers put in a lot of work into making clang fully compatible with gcc, going as far as accepting the same command-line switches). 1 - http://compcert.inria.fr/compcert-C.html#subset

Considering that the parts of C99 that it doesn't support are also not supported by MSVC I can't imaging that that alone is much of a big deal. The prohibition on commercial use is a much bigger barrier, I expect.

MSVC supports C++ instead (AFAIK, it has most of C++11 implemented), while CompCert doesn't compile C++ at all.

Re: The Case for Formal Verification (2013)

#47

Post by [deleted] » Mon, Apr 21, 2014, 1:17 AM UTC

[deleted] wrote: post #44

dkarapetyan wrote: post #43

Earlier quoted context omitted.

Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z? You can sample as many points as you want and you'll still be no wiser as to how + behaves and how it interacts with * or that the implementation of + even respects any of those properties. If you're going to put in the effo…

[deleted]

[deleted]

Re: The Case for Formal Verification (2013)

#48

Post by Dewie » Mon, Apr 21, 2014, 1:19 AM UTC

betterunix wrote: post #13

dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

The problem with proofs is that you need to know what to prove, and that is hard. Even formalizing something as seemingly simple as sorting is tough for most programmers. If your formalization of whatever you wanted to implement is wrong, then your proof is worthless -- you have only proved that your program does something other than what it was supposed to do. It's not that TDD is perfect, but it is a pragmatic appr…

Writing a specification for sorting sounds a lot easier than actually writing a sorting algorithm. Though admittedly I have never used a programming language where I could try to encode this property in a type.

Re: The Case for Formal Verification (2013)

#49

Post by Dewie » Mon, Apr 21, 2014, 1:25 AM UTC

dkarapetyan wrote: post #43

stormbrew wrote: post #40

Earlier quoted context omitted.

I find it strange to think that TDD and formal verification are at odds with each other. For it to be backwards to write dynamic tests, you seem to be suggesting that it is actually worse than doing neither. I also don't see how it can be documentation, glorified or otherwise, and not tell you anything about the properties of the software. Really there are perhaps three practical levels of knowledge about what a piec…

Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z? You can sample as many points as you want and you'll still be no wiser as to how + behaves and how it interacts with * or that the implementation of + even respects any of those properties. If you're going to put in the effo…

> Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z? You can sample as many points as you want and you'll still be no wiser as to how + behaves and how it interacts with * or that the implementation of + even respects any of those properties. If you're going to put in the effort to generate unit tests then why not go a bit further and formally verify the correct functionality?

One could take the middle road and express commutativity, distributivity etc. through invariants and use a fuzzy testing tool to generate tests for it. Generating 100 tests sounds a lot better than a single handwritten one, though of course it's not as good as actually proving it for all inputs.

Re: The Case for Formal Verification (2013)

#50

Post by jarrett » Mon, Apr 21, 2014, 1:32 AM UTC

Will formal verification ever be possible for systems composed of a bunch of heterogeneous components working together? I'm thinking of a web application, where the software's behavior depends on the interaction of client-side scripts, stylesheets, server-side programs, databases, caching layers, and probably other components, all operating in the request-response cycle that fragments behavior into a bunch of separate runs of the various programs.