Re: [SC-L] Provably correct microkernel (seL4)
I wonder what would happen if somebody offered $1 to the first applied researcher to find a fault or security error. According to http://ertos.nicta.com.au/research/l4.verified/proof.pml, buffer overflows, memory leaks, and other issues are not present. Maybe people would give up if they don't gain some quick results, but it seems like you'd want to sanity-check the claims using alternate techniques. - Steve ___ 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. ___
Re: [SC-L] Provably correct microkernel (seL4)
I might argue that it may fix problems that aren't fixable otherwise. My experience in this area is very old, but I found that the biggest benefit of formal methods was not so much the proof but the flaws discovered and fixed on the way to the proof. 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 ___ 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. ___
Re: [SC-L] Provably correct microkernel (seL4)
Steve Christy wrote... I wonder what would happen if somebody offered $1 to the first applied researcher to find a fault or security error. According to http://ertos.nicta.com.au/research/l4.verified/proof.pml, buffer overflows, memory leaks, and other issues are not present. Maybe people would give up if they don't gain some quick results, but it seems like you'd want to sanity-check the claims using alternate techniques. I was actually wondering how they could make that statement unless they can somehow ensure that other components running in kernel mode (e.g., maybe devices doing DMA or device drivers, etc.) can't overwrite the microkernel's memory address space. It's been 20+ years since I've done any kernel hacking, but back in the day, doing something like that with the MMU I think would have been prohibitively expensive in terms of resources. I've not read through the formal proof (figuring I probably wouldn't understand most of it anyhow; it's been 30+ years since my last math class so those brain cells are a bit crusty ;-) but maybe that was one of the caveats that Colin Cassidy referred to. In the real world though, that doesn't seem like a very reasonable assumption. Maybe today's MMUs support this somehow or perhaps the seL4 microkernel runs in kernel mode and the rest of the OS and any DMA devices run in a different address space such as a supervisory mode. Can anyone who has read the nitty-gritty details explain it to someone whose brain cells in these areas have suffered significant bit rot? -kevin -- Kevin W. Wall 614.215.4788Application Security Team / Qwest IT The most likely way for the world to be destroyed, most experts agree, is by accident. That's where we come in; we're computer professionals. We cause accidents.-- Nathaniel Borenstein, co-creator of MIME ___ 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. ___
Re: [SC-L] Provably correct microkernel (seL4)
And presumably before they spent many man years proving implementation correctness they could have spent a fraction of that on design review and subsequent design corrections. -Chris -Original Message- From: sc-l-boun...@securecoding.org [mailto:sc-l-boun...@securecoding.org] On Behalf Of Gunnar Peterson Sent: Friday, October 02, 2009 3:21 PM To: Cassidy, Colin (GE Infra, Energy) Cc: Secure Code Mailing List Subject: Re: [SC-L] Provably correct microkernel (seL4) design flaws. So we have only removed 50% of the problem. for my part there have been many, many days when I would settle for solving 50% of a problem -gunnar ___ 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. ___
Re: [SC-L] Provably correct microkernel (seL4)
It is my understanding that only the micro-kernel runs in kernel mode, but not having read the nitty-gritty either, I'll stand to be corrected. kr, Yo On Fri, Oct 2, 2009 at 11:20 PM, Wall, Kevin kevin.w...@qwest.com wrote: Steve Christy wrote... I wonder what would happen if somebody offered $1 to the first applied researcher to find a fault or security error. According to http://ertos.nicta.com.au/research/l4.verified/proof.pml, buffer overflows, memory leaks, and other issues are not present. Maybe people would give up if they don't gain some quick results, but it seems like you'd want to sanity-check the claims using alternate techniques. I was actually wondering how they could make that statement unless they can somehow ensure that other components running in kernel mode (e.g., maybe devices doing DMA or device drivers, etc.) can't overwrite the microkernel's memory address space. It's been 20+ years since I've done any kernel hacking, but back in the day, doing something like that with the MMU I think would have been prohibitively expensive in terms of resources. I've not read through the formal proof (figuring I probably wouldn't understand most of it anyhow; it's been 30+ years since my last math class so those brain cells are a bit crusty ;-) but maybe that was one of the caveats that Colin Cassidy referred to. In the real world though, that doesn't seem like a very reasonable assumption. Maybe today's MMUs support this somehow or perhaps the seL4 microkernel runs in kernel mode and the rest of the OS and any DMA devices run in a different address space such as a supervisory mode. Can anyone who has read the nitty-gritty details explain it to someone whose brain cells in these areas have suffered significant bit rot? -kevin -- Kevin W. Wall 614.215.4788 Application Security Team / Qwest IT The most likely way for the world to be destroyed, most experts agree, is by accident. That's where we come in; we're computer professionals. We cause accidents. -- Nathaniel Borenstein, co-creator of MIME ___ 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. ___ -- Johan Peeters http://johanpeeters.com ___ 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. ___
Re: [SC-L] Provably correct microkernel (seL4)
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 dont think it will scale well Thirdly, I suspect this is one of those processes that is easier to apply to greenfield development, I dont 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-boun...@securecoding.org [mailto:sc-l-boun...@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.w...@qwest.comPhone: 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. ___ smime.p7s Description: S/MIME cryptographic signature ___ 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. ___
Re: [SC-L] Provably correct microkernel (seL4)
At 4:33 PM -0500 10/1/09, Wall, Kevin wrote: 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. Reading nothing beyond what was posted, the problem I see is to provide a complete specification against which to prove correctness. -- Larry Kilgallen ___ 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. ___
Re: [SC-L] Provably correct microkernel (seL4)
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. maybe not as crazy as it sounds: this is a micro kernel and hence a security chokepoint. The other stuff running on top do not need the same level of assurance. kr, Yo -- Johan Peeters http://johanpeeters.com ___ 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. ___
Re: [SC-L] Provably correct microkernel (seL4)
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. ___
Re: [SC-L] Provably correct microkernel (seL4)
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. ___
Re: [SC-L] Provably correct microkernel (seL4)
design flaws. So we have only removed 50% of the problem. for my part there have been many, many days when I would settle for solving 50% of a problem -gunnar ___ 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. ___
