Formal Verification of a Microkernel Used in Dependable Software Systems
Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer
In recent years, deductive program verification has improved to a degree that
makes it feasible for real-world programs. Following this observation, the
main goal of the Verisoft XT project is (a) the creation of methods and tools
which allow for the pervasive formal verification of integrated computer
systems, and (b) the prototypical realization of four concrete, industrial
application tasks.
In this paper, we report on the Verisoft XT subproject Avionics, where formal
verification is applied to a commercial embedded operating system. The goal is
to use deductive techniques to verify functional correctness of the PikeOS
system, which is a microkernel-based partitioning hypervisor.
We present our approach to verifying the microkernel's system calls, using a
system call for changing the priority of threads as an example. In
particular, (a) we give an overview of the tool chain and the verification
methodology, (b) we explain the hardware model and how assembly semantics is
specified so that functions whose implementation contain assembly can be
verified, and (c) we describe the verification of the system call itself.
We also explain why this effort matters in regulatory dependability frameworks
such as DO-178B and IEC61508 for safety resp. Common Criteria for security.