Formal verification of demand paging

Abstract

This thesis presents the formal pervasive verification of demand paging. Memory virtualization by means of demand paging is a crucial component of every modern operating system. The formal verification is challenging because the reasoning about the page-fault handler (i) has to cover two concurrent computational sources: the processor and the hard disk, and (ii) involves different kinds of semantics for high- and low-level programming languages. In order to tackle the challenge we applied a stack of semantics [Sch06, AHL+ 09] for a high-level C-dialect [Lei07] and low-level assembly code. It can handle mixed-language implementations and concurrently operating devices, and permits the transferral of properties to the target architecture while obeying its resource restrictions. We use a formally verified microprocessor VAMP [BJK+ 06] with devices [Alk09] as a target architecture to run the demand paging implementation. The main result of this work is a mechanically checked formal proof that the page-fault handler maintains memory virtualization of user processes running on top of an operating-system microkernel: each user process is provided with the notion of an own, large and isolated memory. This work is a part of the Verisoft project, a large scale effort bringing together industrial and academic partners to push the state-of-the-art in formal verification for realistic computer systems comprising hard- and software.