11-10

Correctness of an Operating System Microkernel

We outline the paper and pencil correctness proof for an operating system microkernel written in C. The key ingredients of the proof are 1) a simulation of virtual machines by physical processors with swap memory. Here physical memory serves as a cache for virtual memory. In the correctness proof one argues simultaneously about hardware (memory management units) and low level software (page fault handlers). 2) semantics and provably correct compiler for an appropriate subset of C. One needs small steps semantics resp. structured operational semantics, because the computations of the kernel needs to be interleaved with computations of the users. One needs also to consider in line assembler code, because the variables of an abstract C machine do not show the user processes. The correctness proof for the compiler is nontrivial, because the recursion of small steps semantics does not match the recursion for the code generation very well. 3) the definition of an abstract machine model for an operating system kernel providing multiprocessing and virtual memory. In this model interrupt handling and function calls can be treated in a very uniform way. The simulation of this model by a physical machine combines the techniques from the first two parts. This is joint work with M. Gargano, M. Hillebrand and D. Leinenbach. It is part of a large project funded by the German national government, which aims at the formal verification of entire computersystems consisting of hardware, system software, communication system and applications.