One of the challenges in verifying systems level code is the low-level, untyped view of the machine state that operating systems have. We describe a way to faithfully formalise this view while at the same time providing an easy-to-use, abstract and typed view of memory where possible. We have used this formal memory model to verify parts of the virtual memory subsystem of the L4 high-performance microkernel. All formalisations and proofs have been carried out in the theorem prover Isabelle and the verified code has been integrated into the current implementation of L4.

@inproceedings{TuchK-05,
  author =       {Harvey Tuch and Gerwin Klein},
  title =        {A Unified Memory Model for Pointers},
  booktitle =    {12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-12)},
  year =      {2005},
  editor =    {Geoff Sutcliffe and Andrei Voronkov},
  address =   {Jamaica},
  month =     Dec,
  pages =     {474--488},
  series =    {Lecture Notes in Computer Science},
  volume =    {3835},
}