A virtual memory manager (VMM) is a part of an operating system that
provides the rest of the kernel with an abstract model of
memory. Although small in size, it involves complicated and
interdependent invariants that make monolithic verification of the VMM
and the kernel running on top of it difficult. In this paper, we make
the observation that a VMM is constructed in layers: physical page
allocation, page table drivers, address space API, etc., each layer
providing an abstraction that the next layer utilizes. We use this
layering to simplify the verification of individual modules of VMM and
then to link them together by composing a series of small
refinements. The compositional verification also supports function
calls from less abstract layers into more abstract ones, allowing us
to simplify the verification of initialization functions as well. To
facilitate such compositional verification, we develop a framework
that assists in creation of verification systems for each layer and
refinements between the layers. Using this framework, we have
produced a certification of BabyVMM, a small VMM designed for
simplified hardware. The same proof also shows that a certified kernel
using BabyVMM's virtual memory abstraction can be refined following a
similar sequence of refinements, and can then be safely linked with
BabyVMM. Both the verification framework and the entire certification
of BabyVMM have been mechanized in the Coq Proof Assistant.
- Proc. 2nd International Conference on Certified Programs
and Proofs (CPP'12), Kyoto, Japan, December 2012.
Lecture Notes in Computer Science Vol. 7679, pages 143-159.
Conference Paper (PDF).
- Extended TR (PDF)
- Implementation (zip)