Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Case for Formal Verification (2013)

permalink.gmane.org

Post reply on HN
Print view View original

81–90 of 113 posts

Re: The Case for Formal Verification (2013)

#81

Post by mateja »

solomatov wrote: post #58
gsnedders wrote: post #57

Earlier quoted context omitted.

There's Learn You An Agda at " rel="nofollow">https://github.com/liamoc/learn-you-an-agda> , though it never got that far. (I've done comparatively little with theorem provers (v. model checkers), so I can't point you anywhere that useful!)

All these tutorials won't teach you how to use coq or agda. The main problem is that in order to use coq or agda, you need to learn Martin-Lof type theory (or calculus of inductive constructions, which is a similar formalism to MLTT) first, and learn to write code later. Otherwise everything will seem like a magic. There are however, good books on the topic: * Type Theory and Functional Programming ( http://www.cs.ke…

There's a really wonderful tutorial on Coq [1] that holds your hand through all the theory you need to learn. I took a class that used this tutorial and I found it to be very understandable and practical, with hardly any background on formal methods myself. Yes, it's a steep learning curve, but at least with this tutorial, you know the curve you need to follow.

[1] Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/

Hint: Check out the overview [2] to see the chapter dependencies and decide which chapters you may want to skip.

[2] http://www.cis.upenn.edu/~bcpierce/sf/deps.html

Re: The Case for Formal Verification (2013)

#82

Post by mateja »

ma2rten wrote: post #66
sanxiyn wrote: post #60

Earlier quoted context omitted.

I'd think the security of Facebook privacy settings will be improved by, for example, lightweight modelling using Alloy. Alloy would catch bugs like this one: http://mashable.com/2011/12/06/facebook-bug-zuckerberg-photo... When I read about that bug in the past, I thought "this would be a great example to use for Alloy".

Could you elaborate on that? I looked at the article and look at a description of Alloy, it doesn't seem to me like a good example to use for Alloy.

From Daniel Jackson's book on Alloy [1], here are a few of the major examples they provide:

* Leader election in a ring

* Hotel room locking (this one is really cool)

* Media asset library management

* Memory abstractions

[1] http://books.google.com/books?id=DDv8Ie_jBUQC&lpg=PP1&dq=sof...

Re: The Case for Formal Verification (2013)

#83

Post by chriswarbo »

lmm wrote: post #68
wsxcde wrote: post #61

Earlier quoted context omitted.

Model checking deals with two kinds of properties - safety and liveness. Safety properties effectively say nothing bad ever happens while liveness properties say that something good will eventually happen. For example, "my program will never crash due to a null point dereference" is a safety property. "My arbiter module will output a grant for every input request" is a liveness property. It is true that model checker…

> you are inherently limited in terms of what you can prove to whatever it is that the type system can express Does that actually limit you? E.g. I can imagine using a monad-like structure in Haskell to construct things like "procedure guaranteed to terminate in <k primitive steps".

Well, considering that the article talks about Coq, which is completely built around a type system (plus a termination checker), it's not that limiting.

Re: The Case for Formal Verification (2013)

#84

Post by wsxcde »

lmm wrote: post #68
wsxcde wrote: post #61

Earlier quoted context omitted.

Model checking deals with two kinds of properties - safety and liveness. Safety properties effectively say nothing bad ever happens while liveness properties say that something good will eventually happen. For example, "my program will never crash due to a null point dereference" is a safety property. "My arbiter module will output a grant for every input request" is a liveness property. It is true that model checker…

> you are inherently limited in terms of what you can prove to whatever it is that the type system can express Does that actually limit you? E.g. I can imagine using a monad-like structure in Haskell to construct things like "procedure guaranteed to terminate in <k primitive steps".

It's not just about whether it is possible in theory though. I'm sure it is, but if it's too complicated, it won't see adoption. The point I was making is that expressibility isn't just important in your programming language, it's important for your verification scheme as well.

Re: The Case for Formal Verification (2013)

#85

Post by randomdata »

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…

Your test is intended to convey to the reader that your function does addition and provide an example of how to access that function. The functional part of the test is to verify that your claim is true, rather than the stories of yore when the documentation often didn't match what the code actually did.

As a nice side effect, when you refactor your function in the future and you mistakenly turn it into multiplication, the test will give you a sanity check that you meant for it to do addition. Perhaps not a big deal in your contrived example, but is huge in the real world where functions are not quite so simple.

Testing is not for verifying a function is mathematically correct.

Re: The Case for Formal Verification (2013)

#86

Post by wsxcde »

CHY872 wrote: post #73
gsnedders wrote: post #55

Earlier quoted context omitted.

Sadly, it's not a different problem scale — the typical model is something similar to "for each state, does the property P hold?". Hence no matter the property (or complexity thereof), one must still enumerate all states.

Of course, one will attempt to also find equivalence classes for the states! The code long x = user_input(); if (x == 0) { violate_model(); } else { do_something(); } you would expect by any reasonable implementation to collapse the system into just two equivalent states that can be tested.

Ah, but finding equivalence classes of states is quite tricky! Obviously the naive approach of enumerating states and assigning them to equivalence classes is dead on arrival. You might be hinting at examining control flow predicates with your example. This technique is called predicate abstraction and underlies a lot of the SLAM effort. It works in certain scenarios - A statement which more or less captures the state of the field itself.

Re: The Case for Formal Verification (2013)

#87

Post by wsxcde »

CHY872 wrote: post #41
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 asserti…

> 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 technical term for this is bounded model checking (BMC).

Re: The Case for Formal Verification (2013)

#88

Post by munin »

CHY872 wrote: post #72
munin wrote: post #62

Earlier quoted context omitted.

> if a program compiles one can know that it will never crash that is not true, you need much stronger guarantees than just typechecking gives you. you also have a large wodge of native code for the runtime that is not written in the strongly typed language.

Ok, so in retrospect I didn't mean that for OCaml. Certainly it is true for Standard ML [1, 2, 3], or rather, the parts of the language that use the underlying native code (IO etc) are generally smaller pieces of code for which the correctness properties are hopefully more easily tested and verified. In any case, I believe my point still stands on the whole :) [1] http://www.cl.cam.ac.uk/teaching/1314/FoundsCS/fcs-no…

friends of mine have still segfaulted mlton-compiled SML programs. as I understand it, you need to have a bisimulation-based proof that shows equivalence in states between ML and x86, and as far as I know that just hasn't been done. until then you have the risk of a bug in some aspect of the compiler, which has happened, emitting code that produces a crash or something else bad.

Re: The Case for Formal Verification (2013)

#89

Post by munin »

sanxiyn wrote: post #70
munin wrote: post #62

Earlier quoted context omitted.

> if a program compiles one can know that it will never crash that is not true, you need much stronger guarantees than just typechecking gives you. you also have a large wodge of native code for the runtime that is not written in the strongly typed language.

Does Safe Haskell guatantee enough, or do we need more?

I don't think so, there have been bugs in ghc before, the problem would be a bug in ghc that emits code that crashes.

Re: The Case for Formal Verification (2013)

#90

Post by jeffreyrogers »

shlomifr wrote: post #71

This is very relevant in the light of Heartbleed. Core security code should be verified formally, there is no other way to guarantee correctness of implementation.

If my understanding of model checking is correct (which I believe is the primary method of formal verification) I don't think this would help much in the case of Heartbleed. The Heartbleed error had to do with an expression being in the wrong scope if I recall correctly. (I think someone forgot to put brackets around an if statement that contained two expressions).

In this case the model would be correct, but the implementation would be wrong. So I don't think formal verification would be of much help. That said, I think there are a number of static analysis tools that would pick up on the error, so a combination of approaches would work.

And of course, it would be great if we could verify that our security critical code was sound in theory, even if we can't necessarily verify that our implementation is free of coding errors, so I agree with your main argument. Of course, whether we're at the point where doing this verification is feasible in practice is another matter unto itself.

Post reply on HN