Paper Info
Title
Compositional verification of a baby virtual memory manager
Abstract
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.
Year
DOI
Venue
2012
10.1007/978-3-642-35308-6_13
CPP
Keywords
Field
DocType
next layer utilizes,abstract model,verification system,compositional verification,certified kernel,monolithic verification,abstract layer,small vmm,baby virtual memory manager,verification framework,small refinement
Address space,Separation logic,Functional verification,Programming language,Virtual memory,Computer science,Page table,Memory model,High-level verification,Operating system,Proof assistant
Conference
Citations 
PageRank 
References 
7
0.50
16
Authors
2
Name
Order
Citations
PageRank
Alexander Vaynberg1683.04
Zhong Shao289768.80