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