"Devin" == Devin Harper randomfractals@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)