The L4 microkernel (which you can see in L4Linux) is a better design, but still not briliant. There's still a 14% slow-down for some functions.

About the most extreme design is MIT's Exokernel. This takes everything that a microkernel leaves in, and places it in user space. For security, the Exokernel design looks extremely promising, although MIT seems to have abandoned it.

Another kernel design that looks interesting is EROS, which is designed to be secure from the outset.

IMHO, though, seperation is not the answer. Secure boundaries would be much better, as modules have considerable power. If the scope of a module is confined and pre-determined, you should be able to mathematically prove the security.

To be honest, I think that it's about time that somebody DID audit the entire of the Linux core. Not just run some pre-compiler, such as the Stanford Validator, but formally prove each of the core functions correct.

I'm limiting this to the core, as the boundaries of Linux are expanding just too fast to make it viable to start auditing it.

(The FOLK project, that I maintain, is now almost the same size as the Linux kernel it's supposed to patch! And it doesn't even begin to scratch the surface of what patches exist for Linux.)

Further, if you prove the core (including the module-handling code), then you've proved everything you need to. Any rougue module CANNOT impact any other part of the kernel, simply because that would violate the pre/post conditions of the module-handler.

--
You have received this message because you are subscribed to the selinux list.
If you no longer wish to subscribe, send mail to majordomo@tycho.nsa.gov with
the words "unsubscribe selinux" without quotes as the message.