Verifying the L4 virtual memory subsystem
Harvey Tuch, Gerwin Klein · 2004
Abstract. We describe aspects of the formalisation and verification of the L4 µ-kernel. Starting from an abstract model of the virtual memory subsystem in L4, we prove safety properties about this model, and then refine the page table abstraction, one part of the model, towards C source code. All formalisations and proofs have been carried out in the theorem prover Isabelle. 1