Secure Coding mailing list archives
Provably correct microkernel (seL4)
From: colin.cassidy at ge.com (Cassidy, Colin (GE Infra, Energy))
Date: Fri, 2 Oct 2009 15:47:53 +0200
I have a few concerns with formal proofs particularly applying them in a non-academic environment (some of which may be my own na?ve lack of understanding and my feeble memory of my university years studying formal methods). Firstly whilst the code provably does what you said that it would do, that does not mean that what you said the code should do is necessarily correct. As Gary McGraw has pointed out 50% of security issues are bugs, 50% are design flaws. So we have only removed 50% of the problem. Secondly, as you pointed out, that is an awful lot of effort in terms of man years for what is essentially a small program and I don?t think it will scale well Thirdly, I suspect this is one of those processes that is easier to apply to greenfield development, I don?t think many developers will have that luxury. In conclusion, it seems an awful effort to fix half the problem, I'd expect, though cant prove, that a combination of other secure development processes working together will get better results with less overall effort. CJC
-----Original Message----- From: sc-l-bounces at securecoding.org [mailto:sc-l-bounces at securecoding.org] On Behalf Of Wall, Kevin Sent: 01 October 2009 22:34 To: Secure Code Mailing List Subject: [SC-L] Provably correct microkernel (seL4) 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_breakth
rough_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. _______________________________________________
-------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/x-pkcs7-signature Size: 4427 bytes Desc: not available URL: <http://krvw.com/pipermail/sc-l/attachments/20091002/368f798c/attachment.bin>
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)