Applying source-code verification to a microkernel

Abstract

We present the VFiasco project, in which we apply source-code verification to a complete operating-system kernel written in C++. The aim of the VFiasco project is to establish security-relevant properties of the Fiasco microkernel.Source-code verification works by reasoning about the semantics of the full source code of a program. Traditionally it is limited to small programs written in an academic programming language. The project's main challenges are to enable high-level reasoning about typed data starting from only low-level knowledge about the hardware, and to develop a clean semantics for the subset of C++ used by the kernel. In this extended abstract we present our ideas for tackling these challenges. We focus on a type-safe object store that is based on a hardware model that closely resembles the IA32 virtual-memory architecture and on guarantees provided by the kernel itself. We also briefly touch on the semantics for C++.Please find the full version of this paper at http://www.vfiasco.org/objstore.pdf.