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

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.