Verifying the L4 Virtual Memory Subsystem

Harvey Tuch and Gerwin Klein


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.

Online Copy

Available as [PDF]

Bibtex entry

  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},
Gerwin Klein
2005-01-30 14:04:10