1. INTRODUCTION

The security and reliability of a computer system can only be as good as that of the underlying operating system (OS) kernel. The kernel, defined as the part of the system executing in the most privileged mode of the processor, has unlimited hardware access. Therefore, any fault in the kernel’s implementation has the potential to undermine the correct operation of the rest of the system.

General wisdom has it that bugs in any sizeable code base are inevitable. As a consequence, when security or reliability is paramount, the usual approach is to reduce the amount of privileged code, in order to minimise the exposure to bugs. This is a primary motivation behind security kernels and separation kernels [38, 54], the MILS approach [4], microkernels [1, 12, 35, 45, 57, 71] and isolation kernels [69], the use of small hypervisors as a minimal trust base [16,26,56,59], as well as systems that require the use of type-safe languages for all code except some“dirty”core [7,23].

Similarly, the Common Criteria [66] at the strictest evaluation level requires the system under evaluation to have a “simple” design.

With truly small kernels it becomes possible to take security and robustness further, to the point where it is possible to guarantee the absence of bugs [22, 36, 56, 64]. This can be achieved by formal, machine-checked verification, providing mathematical proof that the kernel implementation is consistent with its specification and free from programmer-induced implementation defects.

We present seL4, a member of the L4 [46] microkernel family, designed to provide this ultimate degree of assurance of functional correctness by machine-assisted and machinechecked formal proof. We have shown the correctness of a very detailed, low-level design of seL4 and we have formally verified its C implementation. We assume the correctness of the compiler, assembly code, boot code, management of caches, and the hardware; we prove everything else.

Specifically, seL4 achieves the following:

• it is suitable for real-life use, and able to achieve performance that is comparable with the best-performing microkernels;
• its behaviour is precisely formally specified at an abstract level;
• its formal design is used to prove desirable properties, including termination and execution safety;
• its implementation is formally proven to satisfy the specification; and
• its access control mechanism is formally proven to provide strong security guarantees.