On Tue, May 31, 2011 at 06:02:39PM +0200, Paul de Weerd wrote:
> On Tue, May 31, 2011 at 05:36:17PM +0200, Erik wrote:
> | Op 31-5-2011 17:51, Kevin Chadwick schreef:
> |
> >http://www.techrepublic.com/blog/security/working-towards-bug-free-secure-software/5560?tag=nl.e036
> | >
> | Actually they go full steps further. They have produced a formally
> | verified OS kernel, was in the news august 13, 2009:
> http://tech.slashdot.org/story/09/08/13/0827231/Worlds-First-Formally-Proven-OS-Kernel
>
> "Beware of bugs in the above code; I have only proved it correct, not
> tried it."
Besides that, they use formal proof tools, which are probably much
more complex than the code thay are trying to verify and thus have
bugs of their own.
While formal proofs have their utility (by some accident I studied
with Peter van Emde Boas. The above famous quote comes from a letter
by Don Knuth to Peter) I don't think formal proofs have a lot of
significance when trying to verify a whole OS.
-Otto
