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

21–30 of 113 posts

Re: The Case for Formal Verification (2013)

#21

Post by ryanobjc »

daleharvey wrote: post #15
Pacabel wrote: post #11

Earlier quoted context omitted.

Your description of TDD is a pretty blatant misrepresentation of the actual philosophy and techniques. Furthermore, I think that you're ignoring that TDD tries to be a practical solution to certain real-world problems. This means that trade-offs are made in the name of creating software that works sufficiently well, while keeping expenses in check. Sure, extensive formal verification of all software would probably br…

Really confused at why this comment is being so harshly downvoted, it seems fairly accurate, possibly downplaying how useful formal verification may be in the future, but the parent is most definitely misrepresenting the practicality and usefulness of TDD

I also agree, have some upboats.

The reality is that programming is an engineering endeavor, and in the face of limited resources, we have to choose the tools that can offer realistic benefits now.

Formal verification is not that tool for most projects right now. Would instagram or even facebook be better off? Most people would, correctly, say no.

And ultimately in the end, nearly all software (including quite a bit of open source software!) is written in pursuit of business reasons, and has to answer to that.

Re: The Case for Formal Verification (2013)

#22

Post by betterunix »

sliverstorm wrote: post #16
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…

Perhaps because formal verification is hard & very expensive? For starters, where does an open source project come up with an entire compute farm...

You can do formal verification with tools like Coq using a laptop. The real issue is that writing a formal specification is hard even for small problems; writing a formal spec for something like TLS would be harder than actually implementing TLS.

Re: The Case for Formal Verification (2013)

#23

Post by comex »

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 case with corresponding difficulty of modification and low optimization level. The compiler would still have to be modified to do the propagation, and a machine code model and verifier constructed, but theoretically this would be easier than proving the whole thing works correctly.

I guess Typed Assembly Language works along these lines:

http://www.cs.cornell.edu/talc/

but I haven't read up on the papers, and it seems outdated.

My imaginary end goal (not that I'd be able to do anything remotely as ambitious myself, but I still like to think about it) is an operating system where all code is run in kernel mode after being checked for safety - like Singularity OS but without trusting a compiler.

Perhaps that trust doesn't actually matter very much, since the compiler is unlikely to contain too many exploitable bugs (AFAIK most Java vulnerabilities are not related to the JIT, for instance), and there are plenty of other places in such an operating system bugs could hide anyway. But it's inelegant to require all code to go through a single compiler. For example, it would be cooler if the assembly verifier were not baked into the system, but simply a program proven to correctly check whether some code is safe in the machine code model; if you (any user) could prove a JIT never generates unsafe code, you could submit the JIT in place of the verifier, and run wild with it without going through any slow compilation or verification processes.

Re: The Case for Formal Verification (2013)

#24

Post by wsxcde »

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 hardware world, there's been a lot of progress in automated verification thanks to modern model checkers [1,2] (which incidentally build on modern SAT, and in some cases SMT, solvers [3-6]). The nice thing about model checkers is that you just specify the property you want proven and let the verifier crunch away and it will (hopefully) come up with a proof or a counterexample. This has been successful enough that there are companies like JASPER and OneSpin which make money by selling hardware companies formal verification tools.

I worked with JASPER's tools in the recent-ish past and one of the big things they seem to have done is make the tool much more usable. With the JASPER tool, it was much less of a pain to configure the model checker, abstract away parts of the design, keep track of the properties specified and proven, examine counter example traces and so forth than I was expecting. A lot of this sort of thing doesn't get done in academic tools like ABC because it doesn't count as research. But such improvements are extremely important if you want to push adoption of formal tools in an industrial setting. And from what I can see the emphasis on usability seems to paying off for JASPER.

Model checking in software has been less successful because the state explosion problem is much more pronounced but there have been notable success stories like Microsoft Research's SLAM project [7]. And I definitely think there is an opportunity here to build upon the algorithmic progress in automated verification in order to build tools that are much usable in a software setting.

[1] http://ecee.colorado.edu/~bradleya/ic3/

[2] http://www.eecs.berkeley.edu/~alanmi/abc/abc.htm

[3] https://www.princeton.edu/~chaff/zchaff.html

[4] http://minisat.se/

[5] http://fmv.jku.at/picosat/

[6] http://z3.codeplex.com/

[7] http://research.microsoft.com/en-us/projects/slam/

Re: The Case for Formal Verification (2013)

#25

Post by sliverstorm »

betterunix wrote: post #22
sliverstorm wrote: post #16

Earlier quoted context omitted.

Perhaps because formal verification is hard & very expensive? For starters, where does an open source project come up with an entire compute farm...

You can do formal verification with tools like Coq using a laptop. The real issue is that writing a formal specification is hard even for small problems; writing a formal spec for something like TLS would be harder than actually implementing TLS.

Cool! I do hardware, I guess software is probably easier to compute.

Re: The Case for Formal Verification (2013)

#26

Post by nullc »

ahomescu1 wrote: post #6
Igglyboo wrote: post #4

Can someone explain why CompCert is not more popular? A formally verified compiler seems to be much more useful than something that can produce bugs.

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.

Re: The Case for Formal Verification (2013)

#27

Post by betterunix »

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…

On the topic of trusting compilers:

http://www.dwheeler.com/trusting-trust/

Re: The Case for Formal Verification (2013)

#28

Post by dkarapetyan »

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.

Re: The Case for Formal Verification (2013)

#29

Post by rossjudson »

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 get what you're saying about the state explosion problem, but the article specifically calls out the idea of proving a lack of negative behaviors. It seems to me it might be quite useful to be able to prove, for example, that a program never reads memory at random, or that it never exceeds the bounds of any allocated buffer.

That's a different problem scale than "prove the whole thing works as specified".

Re: The Case for Formal Verification (2013)

#30

Post by betterunix »

sliverstorm wrote: post #25
betterunix wrote: post #22

Earlier quoted context omitted.

You can do formal verification with tools like Coq using a laptop. The real issue is that writing a formal specification is hard even for small problems; writing a formal spec for something like TLS would be harder than actually implementing TLS.

Cool! I do hardware, I guess software is probably easier to compute.

Ah, you might have been thinking of techniques basic on SAT and ATPG solving. What makes software different is this:

https://en.wikipedia.org/wiki/Curry-Howard_Correspondence

Basically, checking a proof of correctness for software is equivalent to type checking (for a very fancy type system).

Post reply on HN