We describe aspects of the formalisation and verification of
the L4 micro-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.
@inproceedings{TuchKleinOSV04,
author = {Harvey Tuch and Gerwin Klein},
title = {Verifying the {L4} Virtual Memory Subsystem},
booktitle = {Proc.\ NICTA Formal Methods Workshop on Operating Systems Verification},
pages = {73--97},
year = {2004},
editor = {Gerwin Klein},
organization = {NICTA Technical Report 0401005T-1},
publisher = {National ICT Australia},
}