Formal Memory Models for the Verification of Low-Level Operating-System Code

Hendrik Tews, Marcus Völp, and Tjark Weber. Journal of Automated Reasoning: Special Issue on Operating Systems Verification, 42(2-4):189-227, April 2009.

Abstract

This article contributes to the field of operating-systems verification. It presents a formalization of virtual memory that extends to memory-mapped devices. Our formalization consists of a stack of three detailed formal memory models: physical memory (i.e., RAM), physically-addressable memory-mapped devices (including their respective side effects, access and alignment requirements), and page-table based virtual memory. Each model is formally shown to satisfy the plain-memory specification, a memory abstraction that enables efficient reasoning for type-correct programs.
This stack of memory models was developed in an attempt to verify Nova, the Robin micro-hypervisor. It is a key component of our verification environment for operating-system kernels based on the interactive theorem prover PVS.

Download

© Springer-Verlag

BibTeX

@article{tews09formal,
  author    = {Hendrik Tews and Marcus V{\"o}lp and Tjark Weber},
  title     = {Formal Memory Models for the Verification of Low-Level Operating-System Code},
  journal   = {Journal of Automated Reasoning: Special Issue on Operating Systems Verification},
  volume    = {42},
  number    = {2--4},
  pages     = {189--227},
  month     = apr,
  year      = {2009},
  url       = {http://dx.doi.org/10.1007/s10817-009-9122-0}
}

Last modified: 2009-06-15