Provably correct microkernel (seL4)

[Kevin.Wall at qwest.com (Wall, Kevin)]

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