The FLINT Project








Compositional Verification of a Baby Virtual Memory Manager

Last modified: Mon Dec 10 05:25:16 2012 GMT.


Alexander Vaynberg
Zhong Shao


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)

Copyright © 1996-2023 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page