The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels

Abstract

The key software component of a computer system is the operating-system kernel. It always needs to be trusted because it runs in the CPU’s privileged mode and therefore has access to all system components. Consequently, kernel correctness is crucial for secure, safe and reliable computer systems. Correctness can be improved by careful design, development and testing. However, this is not enough for kernels of high-assurance computer systems used in defence, aviation and the like. Much stronger correctness guarantees can be obtained by formal verification of a kernel’s implementation. In order to keep verification complexity at a manageable level, prior kernel verification research only targeted uniprocessor kernels. In other words, the current state of research restricts computer systems that require a verified kernel to running on one CPU/core. This is a problem because manufacturers are increasing computing power of their systems by adding more CPUs and cores. In this thesis, we demonstrate that it is possible to extend a verified uniprocessor kernel to utilise multiple CPUs/cores and leverage the existing proofs to obtain a verified multiprocessor version of that kernel (under certain assumptions). To this end, we introduce the clustered multikernel, a point in the design space of multiprocessor kernels. The main feature of this design is that it reduces concurrent data access to a minimum while offering a configurable trade-off between scalability and flexibility. Furthermore, we present a conversion scheme to convert a uniprocessor kernel into a clustered multikernel. Based on this design, we contribute a refinement lifting framework, which lifts the converted kernel’s functional-correctness proof such that it applies to the clusteredmultikernel version. The support for handling the introduced concurrency is added to the existing verification framework in a non-intrusive way and accounts for total-store-order weak memory ordering. We demonstrate the practicability of our approach by successfully applying it to seL4, a formally verified general-purpose microkernel. We show that this requires relatively low effort, compared to the kernel’s initial verification. All formal specifications and proofs are machine-checked in the theorem prover Isabelle/ HOL.