Applying source-code verification to a microkernel

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 th... View More