[seL4] Memory protections within userspace and hardware/driver support

Peter.Chubb at data61.csiro.au Peter.Chubb at data61.csiro.au
Wed May 3 17:55:52 AEST 2017

>>>>> "Devin" == Devin Harper <randomfractals at gmail.com> writes:

Devin> Hi, I read the whole FAQ. Does the "bug-free"
Devin> protections for privacy apply to within each app of the same
Devin> Linux virtual machine (overcoming memory bugs built in apps),

No, the privacy protections are between different security domains
running on seL4.  Linux in a virtual machine is in a single security
domain; there is no added protection for programs running on top of
the virtualised linux kernel.

Devin> Furthermore, do I understand correctly that sel4 will only work
Devin> on a few pieces of computer hardware, or will it work on
Devin> everything the Linux kernel supports (has drivers for)? If sel4
Devin> will work on everything the Linux kernel supports (has drivers
Devin> for), then do the same bug-free promises hold true on those
Devin> hardwares in addition to the hardwares sel4 has already been
Devin> tested on?

seL4 is a microkernel. It contains no drivers at all.
The released verified version is only for one ARM platform; the
verification doesn't cover startup or drivers.  

However, there is some added assurance when running on the platforms
for which seL4 has not been verified (all the platform independent
parts are verified, for instance).  

Peter C

Dr Peter Chubb         Tel: +61 2 9490 5852      http://ts.data61.csiro.au/
Trustworthy Systems Group                           Data61 (formerly NICTA)

More information about the Devel mailing list