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