Provably correct microkernel (seL4)

[yo at secappdev.org (Johan Peeters)]

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



-- 
Johan Peeters
http://johanpeeters.com