Experience Report: SeL4 Formally Verifying a High-Performance Microkernel

The authors report on their experience using the functional programming language Haskell in the formal verification of the seL4 microkernel (Elphinstone et al. 2007). The seL4 kernel is an evolution of the high-performance L4 microkernel family (Liedtke 1995) for secure, embedded devices. It provides essential operating system services such as threads, inter-process communication, virtual memory, interrupts, and authorisation via capabilities. In earlier work (Derrin et al. 2006), they reported on their experience with Haskell as a specification language for seL4. In this paper, they concentrate on the effect the choice of Haskell had on the formal verification of the kernel, from abstract operational specification down to high-performance C code.