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

91–100 of 113 posts

Re: The Case for Formal Verification (2013)

#91

Post by anon4 »

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…

I think you're not thinking far enough. Why not have a compiler that can take your specification and just write your program for you? You'll probably need to write some code yourself, which will then interface with the written-from-formal-proof code a-la quark.

My intuition is that a specification that can be checked and is good enough to guarantee that your program is 100% correct should be enough to compile a full program from, possibly with some hand-written lower-level code for guidance so it doesn't fall in pathological cases like "the empty program satisfies these constraints and is easiest to generate, so here".

Re: The Case for Formal Verification (2013)

#92

Post by Shish2k »

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…

I'd love to use proofs that my software is good; but after reading the 43 page "coq in a hurry" document, I still have no idea how to prove that "print 2 + 2" prints out "4", let alone how to apply it to any of my real world apps :(

Mostly it seems formal proof stuff looks a lot like my memories of the functional programming world -- lots of one-letter variable names and unicode symbols, no code comments, any word that isn't an abbreviation is in Latin; all emphasis on the abstract, no mention of how to make this wonderful formula interact with the real world... Is there some fundamental reason that a proof language can't be as readable and practical as Python?

Re: The Case for Formal Verification (2013)

#93

Post by EzraVinh »

solomatov wrote: post #64
EzraVinh wrote: post #63

Earlier quoted context omitted.

But Haskell is also based on some type system, and yet Learn You a Haskell teaches Haskell without formally teaching this type system. I've been learning Idris and reading the HoTT book at the same time. I'm not sure what it would have been like learning Idris without any formal type theory, but I believe it would be possible.

The difference here is that type system in case of agda and coq is the core of the language, it's very similar to what operational semantics does with usual programming languages. The type systems is a logic via Curry-Howard correspondence, with which program correctness is proved. In case of Haskell it's just a software engineering tool which helps you find errors in your program in a semi-automatic way.

I would say its a sliding scale, I don't think there is a sharp qualitative difference between Idris and Haskell. Haskell programs can also be thought of as proofs, namely proofs that the variables/functions you define have the types you claim they have.

You mention Agda and Coq. Maybe one difference in our viewpoint is that Idris really is designed for general purpose programming. E.g. you can write a program with almost identical structure to a Haskell program.

Re: The Case for Formal Verification (2013)

#94

Post by chriswarbo »

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…

Why are imperfect programs and test suites useful, yet imperfect specifications are worthless?

It's not all black-and-white. Specifications, like test suites, contain many properties. The problems of specifying slightly-wrong behaviour on edge-cases might be more than offset by the security guarantees that are gained.

Also, note that many properties are built on each other and specifications will grow and change along with the software. Incorrect properties are often incompatible, but unlike tests which may never hit the incompatible cases, a verification tool will refuse to accept such incompatibilities.

Re: The Case for Formal Verification (2013)

#95

Post by vertex-four »

jeffreyrogers wrote: post #90
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 imp…

> I think someone forgot to put brackets around an if statement that contained two expressions

That was Apple's goto fail. Heartbleed was caused by out of bounds memory access.

Re: The Case for Formal Verification (2013)

#96

Post by chriswarbo »

anon4 wrote: post #91
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…

I think you're not thinking far enough. Why not have a compiler that can take your specification and just write your program for you? You'll probably need to write some code yourself, which will then interface with the written-from-formal-proof code a-la quark. My intuition is that a specification that can be checked and is good enough to guarantee that your program is 100% correct should be enough to compile a full…

> Why not have a compiler that can take your specification and just write your program for you?

One difficulty with this is that programs (by definition) are 'computationally relevant' whereas proofs are not. In other words, as long as we have a proof of X it doesn't make a difference which proof we happen to have. On the other hand, different functions of type X can have a big impact on a program.

For starters, there are properties which are difficult to express using types. For example, we only have rudimentary ways to encode space and time usage (eg. 'cost semantics'). Without this, when we ask for a sorting algorithm we may get back bubblesort, since it's a perfectly acceptable implementation of a sorting algorithm.

Also, our types will have to become incredibly precise. Rather than just encoding the properties we care about (eg. security guarantees), we need to include lots of uninteresting properties to guide the computer to what we want (compare this to guiding a genetic algorithm via a fitness function, or getting a genie to grant you a wish in exactly the way you want). At this point, you're basically writing your program in a very indirect way; you may be better off just writing one or two lines 'manually' instead of trying to steer the automated process.

Re: The Case for Formal Verification (2013)

#98

Post by jderick »

jeffreyrogers wrote: post #90
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 imp…

It is also possible to apply model checking or theorem proving directly to the implementation. Doing so would be able to catch any sort of error that a static analysis tool would. Of course, static analysis typically scales better and would be a good place to start for catching this type of error.

Re: The Case for Formal Verification (2013)

#99

Post by solomatov »

EzraVinh wrote: post #93
solomatov wrote: post #64

Earlier quoted context omitted.

The difference here is that type system in case of agda and coq is the core of the language, it's very similar to what operational semantics does with usual programming languages. The type systems is a logic via Curry-Howard correspondence, with which program correctness is proved. In case of Haskell it's just a software engineering tool which helps you find errors in your program in a semi-automatic way.

I would say its a sliding scale, I don't think there is a sharp qualitative difference between Idris and Haskell. Haskell programs can also be thought of as proofs, namely proofs that the variables/functions you define have the types you claim they have. You mention Agda and Coq. Maybe one difference in our viewpoint is that Idris really is designed for general purpose programming. E.g. you can write a program with a…

>I don't think there is a sharp qualitative difference between Idris and Haskell.

Yes, there's no such a difference. However, in order to use Idris to its full potential, you need to use dependent types. It's just like writing procedural programs in object-oriented or functional language. It's possible, however, it's not a very bright idea.

Re: The Case for Formal Verification (2013)

#100

Post by CHY872 »

munin wrote: post #88
CHY872 wrote: post #72

Earlier quoted context omitted.

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.

My first opportunity to whip this one out :) https://cakeml.org/popl14.pdf
Post reply on HN