Formal Memory Models for the Verification of Low-Level Operating-System Code
In this paper, the authors contribute to the field of operating-systems verification. It presents a formalization of virtual memory that extends to memory-mapped devices. Their 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.