[ACM Press the 10th workshop - Saint-Emilion, France (2002.07.01-2002.07.01)] Proceedings of the 10th workshop on ACM SIGOPS European workshop: beyond the PC - EW10 - Applying source-code verification to a microkernel

✍ Scribed by Hohmuth, Michael; Tews, Hendrik; Stephens, Shane G.

• Book ID: 121006127
• Publisher: ACM Press
• Year: 2002
• Weight: 118 KB
• Category: Article
• DOI: 10.1145/1133373.1133405

✦ Synopsis

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++.