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.