Comparison

Criteria

The comparison uses the following criteria:

• Correctness proof:
  Is there a proof that the kernel behaves according to a formal specification?
• Security proof:
  Is there proof that a specification of the kernel has specific security properties?
• Fast IPC:
  Does it provide fast IPC mechanisms that make protection domains cheap to use?
• Deployed:
  Is there deployment and use in industry?
• Fine-grained access control:
  Is fine-grained mandatory access control available to user-level?
• MMU support:
  Does the kernel support virtual memory and memory protection?
• Virtualisation:
  Does the kernel provide type-1 hypervisor support?
• General purpose:
  Is the kernel limited to specific application scenarios and domains or can it be used as a general-purpose OS kernel?
• Open source:
  Is it available under under an OSI-approved open source license?

Results

Traditional kernels for safety-critical applications like QNX, Wind River's VxWorks, or Greenhills INTEGRITY are widely deployed and generally support memory protection and virtualisation like seL4. They are not cheap, and certainly not available as open source. It is hard to get official performance numbers for any of these, and evaluation licenses do not allow reporting such numbers. If you have a license, you can compare yourself: public, up-to-date numbers for seL4 are available from the performance page. From what we have seen reported, these kernels are multiple architecture generations older than seL4 and cannot provide the same order of magnitude of IPC performance. The older design also means they do not support fine-grained mandatory access control like seL4 does. In terms of assurance, these kernels do all achieve high levels of traditional safety and security mechanisms, but not to the level that the formal verification of seL4 can provide. Only INTEGRITY underwent a security proof from formal code model to security property, but the proof is neither available for multiple current hardware architectures and OS versions, nor is it public. It also does not connect formally to the source code of the kernel. Without that connection, keeping code and proof in sync is a manual process with all the human error potential that is inherent to manual processes. INTEGRITY does not come with a functional correctness proof.

There is one other formally verified OS kernel in the literature that provides a proof of functional correctness and security comparable to the level seL4 provides: CertiKOS. However, CertikOS is not a general-purpose OS kernel and only provides a very limited API that makes it an academic case study rather than a base for practically usable systems. To the best of our knowledge it is not deployed in any real-world system. Its own performance evaluation puts it at several multiples slower than seL4. A public review copy is available for non-commercial use, under a non-open source license. Development on it seems to have run out.

FreeRTOS is a widely used real-time OS kernel for microcontrollers, comparable to other projects in this class like Zephyr. In contrast to seL4, they specifically target micro-processors without a virtual memory management unit, and do not provide features such as fine-grained access control, virtualisation, or fast IPC. They are not general-purpose kernels, but built specifically for real-time applications. While FreeRTOS is the subject of multiple partial academic formal verification efforts, there is no functional correctness proof or security proof available that covers the entire kernel. Hardware memory protection mechanisms are essential for such proofs to make sense on their own — without memory protection, broken or malicious user-level code can modify kernel data structures and break the kernel. With seL4, this is not the case. If the proof assumptions are satisfied, the seL4 proofs hold for all user behaviours.

The table leaves out monolithic kernels like Linux and solutions built on it such as Ubuntu Core. Modern monolithic kernels are so large that they cannot reliably provide safety and security in high-assurance scenarios and must generally be treated as untrusted code with a large attack surface in a high-assurance security analysis. Even a solution like SELinux, which adds mandatory access control to the kernel, does not change the fact that an exploitable defect anywhere in a monolithic kernel runs in privileged hardware mode and can undermined the entire system. Such solutions can be used to improve application security, but they fundamentally cannot reach high assurance levels.

The table also does not mention mainstream virtualisation solutions like Xen or KVM, which are not OS kernels. In some scenarios they can be used to increase security of a system, but compared to high-assurance solutions their code size and attack surface is still very large. seL4 solves this problem by design and puts most of virtual machine management code at user level where it is subject to mandatory access control and isolation.