Applying source-code verification to a microkernel — the VFiasco project

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 mi-crokernel. Source-code verification works by reasoning about the semantics of the full source code of a program. Tradition-ally 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 resem-bles the IA32 virtual-memory architecture and on guaran-tees provided by the kernel itself. We also briefly touch on the semantics for C++. Please find the full version of this paper a