Secure Coding mailing list archives
Provably correct microkernel (seL4)
From: jeremy.j.epstein at gmail.com (Jeremy Epstein)
Date: Fri, 2 Oct 2009 13:01:28 -0400
Caveats on the proofs, as I recall. I'll try to dig up the details. It's been pretty extensively discussed elsewhere... On Fri, Oct 2, 2009 at 12:54 PM, Dimitri DeFigueiredo <ddefigue at adobe.com> wrote:
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. _______________________________________________
Current thread:
- Provably correct microkernel (seL4) Wall, Kevin (Oct 01)
- Provably correct microkernel (seL4) Jeremy Epstein (Oct 02)
- Provably correct microkernel (seL4) Dimitri DeFigueiredo (Oct 02)
- Provably correct microkernel (seL4) Jeremy Epstein (Oct 02)
- Provably correct microkernel (seL4) Dimitri DeFigueiredo (Oct 02)
- Provably correct microkernel (seL4) ljknews (Oct 02)
- Provably correct microkernel (seL4) Cassidy, Colin (GE Infra, Energy) (Oct 02)
- Provably correct microkernel (seL4) Gunnar Peterson (Oct 02)
- Provably correct microkernel (seL4) Chris Wysopal (Oct 02)
- Provably correct microkernel (seL4) Gunnar Peterson (Oct 02)
- Provably correct microkernel (seL4) Johan Peeters (Oct 02)
- Provably correct microkernel (seL4) Steven M. Christey (Oct 02)
- Provably correct microkernel (seL4) Wall, Kevin (Oct 02)
- Provably correct microkernel (seL4) Johan Peeters (Oct 03)
- Provably correct microkernel (seL4) Wall, Kevin (Oct 02)
- <Possible follow-ups>
- Provably correct microkernel (seL4) Bobby Miller (Oct 02)
- Provably correct microkernel (seL4) Jeremy Epstein (Oct 02)