Operating System (OS) kernels form the backbone of all system software. They have a significant impact on the resilience, extensibility, and security of today's computing hosts. However, modern OS kernels are complex and may consist of a multitude of sequential or concurrent abstraction layers; unfortunately, abstraction layers have almost never been formally specified or verified. This makes it difficult to establish strong correctness properties, and to scale program verification across multiple abstraction layers.;Recent efforts have demonstrated the feasibility of building large scale formal proofs of functional correctness for simple general-purpose kernels, but the cost of such verification is still prohibitive, and it is unclear how to use their verified kernels to reason about user-level programs and other kernel extensions. Furthermore, they have ignored the issues of concurrency, which include not just user- and I/O concurrency on a single core, but also multicore parallelism with fine-grained locking.;This thesis presents CertiKOS, an extensible architecture for building certified sequential and concurrent OS kernels. CertiKOS proposes a new compositional framework showing how to formally specify, program, verify, and compose concurrent abstraction layers. We present a novel language-based account of abstraction layers and show that they correspond to a strong form of abstraction over a particularly rich class of specifications that we call deep specifications . We show how to instantiate the formal layer-based framework in realistic programming languages such as C and assembly, and how to adapt the CompCert verified compiler to compile certified C layers such that they can be linked with assembly layers. We can then build and compose certified abstraction layers to construct various certified OS kernels, each of which guarantees a strong contextual refinement property for every kernel function, i.e., the implementation of each such function will behave like its specification under any kernel/user context with any valid interleaving.;To demonstrate the effectiveness of our new framework, we have successfully implemented and verified multiple practical sequential and concurrent OS kernels. The most realistic sequential hypervisor kernel is written in 6000 lines of C and x86 assembly, and can boot a version of Linux as a guest. The general-purpose concurrent OS kernel with fine-grained locking can boot on a quad-core machine. For all the certified kernels, their abstraction layers and (contextual) functional correctness properties are specified and verified in the Coq proof assistant.
展开▼
