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. ___
[SC-L] OWASP Summit / Elections
The next global summit for OWASP Foundation Inc (www.owasp.org) will be held on November 11th 2009 (Veterans Day in the USA) in Washington, DC., USA As is customary at our summits we will govern by rough consensus and collaborate face to face town hall style for our professional associations direction. http://www.owasp.org/index.php/Summit_2009 Just one of the many shaping activities that will take place will be, the first democratic ELECTION of a OWASP Board Member by the membership. Eligible individuals have already volunteered time, served as a project leader and or chapter leader and have have demonstrated global leadership acumen as a current and active member of a Global Committee. You will hear from each of these candidates during the town hall session of why they are the best person for the role. If you have never attended a OWASP Summit (such as Portugal 2008 http://www.owasp.org/index.php/OWASP_EU_Summit_2008 ) you will not want to miss this event - when you get passion filled OWASP people together we come together as a community to set the direction for the next 6,12,24 months and we need you to get involved to continue our mission. Semper Fi, Tom Brennan OWASP Foundation 973.506.9303 About OWASP - http://www.owasp.org/index.php/About_OWASP - 2009 OWASP Summit http://www.owasp.org/index.php/Summit_2009 ___ 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. ___
