Running the Manual: An Approach to High-Assurance Microkernel Development
Presenter: Michael
Preview
This week I’ll be presenting the paper “Running the Manual: An Approach to High-Assurance Microkernel Development”, by Philip Derrin et al. This is a paper from 2006 during the earlier stages of seL4’s development, dealing with their use of Haskell in creating an executable prototype of their microkernel. They describe modelling the kernel’s behavior/state in a functional language, the use of HOL for verification, and future work (since completed) of creating an abstract specification and a C implementation that refines said abstract spec as well as this executable spec.
See you there! Michael
Paper Summary
This paper begins by explaining that, “unfortunately, systems programming languages and rigorous formal methods are far apart, leading to slow development and and to compromises in performance and safety.” They propose rethinking the traditional kernel development model by focusing on the implementation of an executable kernel API specification (specifically, a microkernel called seL4), in Haskell. By creating a high-level runnable prototype, they can iterate quickly, avoid low-level HW details, and extract a formal specification into HOL, which is then is proven to refine a more abstract specification. In addition, in (now completed) further work they created a separate high-performance C implementation which refines this executable Haskell specification.
They model the kernel as a state transformer which is a function on system events; essentially, the kernel is a monad. They model storing objects in the physical address space and define the set of faults, errors, and failures that can occur, isolating the portion of the kernel that can trigger said failures via the ErrorT monad transformer.
To test their API/implementation, they used simulators of actual hardware architectures to generate a wide range of events in various system states. They prove refinement and low-level system properties (system call termination, kernel-user memory separation, kernel’s sole use of privileged code) by translating (“for the most part,” “purely syntactical[ly]”) Haskell to Isabelle/HOL. They rely on using a constrained subset of Haskell to make sure that Haskell functions always terminate, and rely on using concrete monads in Isabelle to overcome Isabelle’s lack of certain other features.
To finish, they describe their experience qualitatively. They argue that their approach is nice because they can test the kernel design incrementally, without having to imeplement everything. Early formalization efforts helped them uncover implementation bugs early, and they also argue that they literally are “running the manual” because they write in and generate documentation from Literate Haskell files.
Lab Discussion
The main questions we had concerned the extent of how much hardware they model in the Haskell specification and the form of their refinement proofs, and we learned a little Isabelle. We went through the paper (sorry, no slides today), jumping to another two papers intermittently to answer doubts we had in the process. Specifically, we referred to Elphinstone and Heiser’s “From L3 to seL4: What Have we Learnt in 20 Years of L4 Microkernels” and Klein et al.’s “Comprehensive Formal Verification of an OS Microkernel” (both linked below) to answer questions about the C implementation and refinement proof process. Additionally, we briefly went through seL4 Haskell spec code form their l4v repository and the accompanying Isabelle refinement code.