Questions and Answers
This page answers some of the burning questions on the seL4 (secure, embedded L4) microkernel and its formal verification.
Where can I download seL4?
seL4, its proofs, as well as userspace libraries and tools are open-source software and can be accessed from http://seL4.systems
Yes, yes, it's verified. But does it run Linux?
We're pleased to say that it does. Presently, we have a para-virtualized version of Linux running on top of the (unverified) x86 port of seL4. There are plans to port Linux to the verified ARM version of seL4 as well.
Does seL4 run Windows, Windows CE, Darwin, iPhone OS, Android, Symbian, ..?
Currently not, but there is no reason why it couldn't, given appropriate agreements and funding.
What platforms does seL4 run on?
Currently, ARM11 and x86.
Does seL4 support multi-core?
There is currently only experimental and unverified multi-core support for seL4. Meaningful support of multi-core chips together with formal verification still is a research challenge.
Does seL4 have zero bugs?
Our proof states that, if the proof assumptions are true, the seL4 kernel has no deviations from its specification. There may still be unexpected features in the specification and one or more of the assumptions may not apply. In particular, the remaining implementation details below the level of the C programming language may still contain as many or few defects as other well-engineered software. The proof and assumption page has the longer version.
Is seL4 proven secure?
No, it is not. The proof states and shows functional correctness, not security. Functional correctness implies the absence of many security common problems, provided the proof assumptions hold (see also the longer version), but it does not mean that the kernel or system as a whole is "secure". Such a statement would first require a precise mathematical definition of what secure means. We are working on proving precisely defined, high-level security properties of seL4 in the future. These proofs will provide stronger assurance than what is possible of current systems, but they will still be up to assumptions and classes of attack vectors.
If I run seL4, is my system secure?
Not automatically, no. Security is a question that spans the whole system, including its human parts. An OS kernel, verified or not, does not automatically make a system secure. It can, however, provide the system architect and user with strong mechanisms to implement security policies.
What does seL4 provide?
Microkernels like seL4 are very small operating system kernels. The kernel by definition is the part of the software that runs in the most privileged access mode of the hardware. The idea of a microkernel is to minimise this all-powerful code base. Microkernels typically do not provide device drivers, file systems or network stacks. All of these run in user mode and can be made to perform as well or better than the same services running in kernel mode in monolithic systems. The seL4 kernel provides the following mechanisms to build such user-level services on top: threads, scheduling, inter-process communication (IPC), virtual memory, interrupts, and access control via capabilities.
Where can seL4 be used?
seL4 is a general-purpose microkernel, so the right answer is: anywhere, really. The main target are embedded systems with security or reliability requirements, but that is not exclusive. Using a microkernel like seL4 makes sense on platforms that provide virtual memory protection and for application areas where you would like to isolate different parts of the software from each other. For many systems, this is just common sense and good software engineering practise. For some systems it is essential. Immediate applications that come to mind are in the financial, medical, automative, aero-space, and defence sectors. There is no reason seL4 could not run on a normal desktop computer.