Xiongnan (Newman) Wu – 3rd Year
Advisor: Zhong Shao
Title: Verification of a practical hypervisor operating system kernel
Abstract: Operating System (OS) kernels form the backbone of all system software. We have developed a new compositional approach for building certified OS kernels. Because the very purpose of an OS kernel is to build layers of abstraction over hardware resources, we insist on uncovering and specifying these layers formally, and then verifying each kernel module at its proper abstraction level. To demonstrate the effectiveness of our new approach, we have successfully implemented and verified a practical OS kernel in the Coq proof assistant. Our certified hypervisor OS kernel is written in 5500 lines of C and x86 assembly, and can successfully boot a version of Linux as a guest. The entire specification and proof effort took less than 1.5 person years.
For each kernel function, we prove a strong contextual refinement property, which states that the implementation of each such function behaves like its specification under any kernel/user (or host/guest) context. In this talk, we present the methodology we use on the verification of the C programs, which is one of the major components of the contextual refinement proof. For each C function in the kernel, we prove that its semantics, under the big-step semantics provided by CompCert, refines its specification. Verification of C programs is challenging. C programming language is known to support very limited forms of abstraction, which makes the verification task extremely complicated, especially when the programs manipulate low level pointer data structures stored in the memory. Hence, full automatic verification of C programs is impractical. On the other hand, we have developed various proof automation tools to semi-automate the process of verifying C source code of the operating system. The goal is to reduce manual proof as much as possible and seek for human interaction only when it is necessary. With the help of these libraries, we show how we handle sequential statements, conditionals, and (nested) loops present in the program. These tools have greatly reduced the amount of work needed in the verification of the OS kernel.