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. _______________________________________________
