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.
The Case for Formal Verification (2013)
71–80 of 113 posts
Re: The Case for Formal Verification (2013)
#72Earlier quoted context omitted.
I'm sorry, but I don't believe this point has any merit with regards to this discussion. Formal verification was seen as the future for large systems for some short time in the latter half of the 20th century, and since then no one has seriously suggested verifying programs of millions lines of code. The point that is made here (quite sensibly) is that in many cases, by verifying small parts of your codebase (a few h…
> 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-notes.pdf [2] http://gallium.inria.fr/~fpottier/publis/fpottier-regis-gian... [3] https://en.wikipedia.org/wiki/Type_safety#Standard_ML
Re: The Case for Formal Verification (2013)
#73Earlier quoted context omitted.
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".
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();
}
Re: The Case for Formal Verification (2013)
#74Earlier quoted context omitted.
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").
Ideally, we should minimize the code in any given path to assurance, but maximize the number of independent paths to assurance (modulo resource constraints).
Re: The Case for Formal Verification (2013)
#75As a q/a by profession, I allways wonder, how to have some better assurances that the software I have does what it is supposed to.
I believe I have even incidentaly reimplemented quick-check on several occasions.
When we were working in Clojure for a little while, I wondered if it might be possible to combine contracts and logic programming, to verify that contracts don't contradict each other on compile ... and then I realized, that for more complex constraints I might need to solve halting problem.
On the other hand, I remember how much productivity I gained, after I wrapped our json library in simple macro, that verified that the data I feed it conforms to schema (that was before prismatics schema existed, or even core.typed).
Re: The Case for Formal Verification (2013)
#76Yes 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…
It's a lot easier to be sure that you are correctly checking that 2 + 2 = 4, than to verify that you're proving the right thing. If you have your proof in hand, and unit tests, you should be more confident than if you have just your proof. Vice versa as well, of course (and probably more so) but that doesn't mean you shouldn't test properties of your code.
Re: The Case for Formal Verification (2013)
#77Earlier quoted context omitted.
I am not mocking documentation.
"just glorified documentation" I think it's pretty well understood that calling something "glorified" is making fun of it. Perhaps I guess you meant to mock TDD but it also seems like you are mocking writing documentation. While it could cut either way I guess, I decided to take a snap judgement (like 99% of your readers) and call you out on it. Sorry.
Don't make the mistake of thinking the pattern "[something perceived as greater than X] is just glorified X" calls into question the value of X. Rather, it's the perception of being greater that is being called into question.
If I say "soda is just glorified water" do you think I'm mocking water and that I don't think water is vital for all life on this planet?
Re: The Case for Formal Verification (2013)
#78Earlier quoted context omitted.
Idris is really worth checking out if you have any interest in this kind of stuff. I used Coq and now am playing with Idris and F*; the latter two feel good and practical. With an FP background they are easy to pick up.
I've also been playing around with these two. I have a little Haskell and some OCaml, but very little understanding of the mathmatics involved in dependent typing, so I'm struggling but still very interested. Wish there were an accessible guide like "Learn you a Haskell" for Idris. By the way, for anyone interested in these two languages with dependent typing, you can try out both Idris and F* online, without install…
Cannot edit for reason, but I thought I would mention, as this is of vital importance to me when i'm learning something new, that both Idris and F* are open source;
https://github.com/nikswamy/FStar (Apache) https://github.com/idris-lang/Idris-dev (do whatever, just retain copyright)
Re: The Case for Formal Verification (2013)
#79Earlier 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…
The QuickCheck model is at least as good as unit tests and is more likely to actually find bugs and corner cases . The resulting code is no more complex either. The only drawback I see is that it requires you to design your code in a very modular way that makes things amenable to automated input generation.
Yes, but unit tests and TDD are not synonymous. TDD is a design technique first and a testing tool second. It's goal is to get you to a good design place, not produce a unit test suite - let alone one with 100% coverage.
I love declarative testing tools like QuickCheck. They're excellent. I still test-drive my code though.
Re: The Case for Formal Verification (2013)
#80This 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.
Verified formally, tested, audited, and whatever else we can throw at it.