Provably correct microkernel (seL4)

[ddefigue at adobe.com (Dimitri DeFigueiredo)]

There is a proof for a whole kernel I can use today. How's that not practically useful? Is it not practically useful 
because there are caveats on the proof? I don't we can just dismiss this one without further reasoning or because we 
don't know how to apply it to our own problems.

Dimitri

-----Original Message-----
From: sc-l-bounces at securecoding.org [mailto:sc-l-bounces at securecoding.org] On Behalf Of Jeremy Epstein
Sent: Friday, October 02, 2009 6:38 AM
To: Wall, Kevin
Cc: Secure Code Mailing List
Subject: Re: [SC-L] Provably correct microkernel (seL4)

This was discussed a few months ago on several other lists I read.
The consensus is that it's interesting, and is further than anyone
else has gone in recent years to do proofs, but not practically
useful.  Additionally, there are a lot of caveats on the proof (which
I don't recall, but are well documented on their web site) that make
it clear it's not really as useful as it might sound.

--Jeremy

On Thu, Oct 1, 2009 at 5:33 PM, Wall, Kevin <Kevin.Wall at qwest.com> wrote:
> Thought there might be several on this list who might appreciate
> this, at least from a theoretical perspective but had not seen
> it. (Especially Larry Kilgallen, although he's probably already seen it. :)
>
> In http://www.unsw.edu.au/news/pad/articles/2009/sep/microkernel_breakthrough.html,
>
> ? ?"Professor Gernot Heiser, the John Lions Chair in Computer Science in
> ? ?the School of Computer Science and Engineering and a senior principal
> ? ?researcher with NICTA, said for the first time a team had been able to
> ? ?prove with mathematical rigour that an operating-system kernel -- the
> ? ?code at the heart of any computer or microprocessor -- was 100 per cent
> ? ?bug-free and therefore immune to crashes and failures."
>
> In a new item at NICTA
> <http://nicta.com.au/news/current/world-first_research_breakthrough_promises_safety-critical_software_of_unprecedented_reliability>
>
> it mentions this proof was the effort of 6 people over 5 years (not quite
> sure if it was full-time) and that "They have successfully verified 7,500
> lines of C code [there's the problem! -kww] and proved over 10,000
> intermediate theorems in over 200,000 lines of formal proof". The proof is
> "machine-checked using the interactive theorem-proving program Isabelle".
>
> Also the same site mentions:
> ? ?The scientific paper describing this research will appear in the 22nd
> ? ?ACM Symposium on Operating Systems Principles (SOSP)
> ? ? ? ?http://www.sigops.org/sosp/sosp09/.
> ? ?Further details about NICTA's L4.verified research project can be found
> ? ?at http://ertos.nicta.com.au/research/l4.verified/.
>
> My $.02... I don't think this approach is going to catch on anytime soon.
> Spending 30 or so staff years verifying a 7500 line C program is not going
> to be seen as cost effective by most real-world managers. But interesting
> research nonetheless.
>
> -kevin
> ---
> Kevin W. Wall ? ? ? ? ? Qwest Information Technology, Inc.
> Kevin.Wall at qwest.com ? ?Phone: 614.215.4788
> "It is practically impossible to teach good programming to students
> ?that have had a prior exposure to BASIC: as potential programmers
> ?they are mentally mutilated beyond hope of regeneration"
> ? ?- Edsger Dijkstra, How do we tell truths that matter?
> ? ? ?http://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD498.html
>
> _______________________________________________
> Secure Coding mailing list (SC-L) SC-L at securecoding.org
> List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
> List charter available at - http://www.securecoding.org/list/charter.php
> SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
> as a free, non-commercial service to the software security community.
> _______________________________________________

_______________________________________________
Secure Coding mailing list (SC-L) SC-L at securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
_______________________________________________