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.
|School Location:||United States -- Connecticut|
|Source:||DAI-B 78/07(E), Dissertation Abstracts International|
|Keywords:||Abstraction Layer, Certain Complier, Certified OS Kernels, Concurrency, Deep Specification, Program Verification|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be