Secure Microkernels, State Monads and Scalable Refinement

The authors present a scalable, practical Hoare Logic and refinement calculus for the nondeterministic state monad with exceptions and failure in Isabelle/HOL. The emphasis of this formalisation is on large-scale verification of imperative-style functional programs, rather than expressing monad calculi in full generality. They achieve scalability in two dimensions. The method scales to multiple team members working productively and largely independently on a single proof and also to large programs with large and complex properties. They report on the experience in applying the techniques in an extensive (100,000 lines of proof) case study - the formal verification of an executable model of the seL4 operating system microkernel.