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 <ddefi...@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-boun...@securecoding.org [mailto:sc-l-boun...@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.w...@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.w...@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@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@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@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. _______________________________________________
