Zhong Shao, Yale Univeresity

Advanced Development of Certified OS Kernels

Abstract

Operating System (OS) kernels form the backbone of all system software. They can have a significant impact on the resilience, extensibility, and security of today's computing hosts. In this talk, we present a new compositional approach for building certifiably secure and reliable 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 support reasoning about user-level programs and linking with other certified kernel extensions, we prove a strong contextual refinement property for every kernel function, which states that the implementation of each such function will behave like its specification under any kernel/user (or host/guest) context. To demonstrate the effectiveness of our new approach, we have successfully implemented and specified a practical OS kernel and verified its (contextual) functional correctness property in the Coq proof assistant. We show how to extend our base kernel with new features such as virtualization, interrupts and device drivers, and end-to-end information flow security, and how to quickly adapt existing verified layers to build new certified kernels for different domains.