Verification of programs in virtual memory using separation logic

Abstract

Formal reasoning about programs executing in virtual memory is a difficult problem, as it is an environment in which writing to memory can change its layout. At the same time, correctly reasoning about virtual memory is essential to operating system verification, a field we are very much interested in. Current approaches rely on entering special modes or making high-level assertions about the nature of virtual memory which may or may not be correct.

In this thesis, we examine the problems created by virtual memory and develop a unified view of memory, both physical and virtual, based on separation logic. We first develop this model for a simple programming language on a simplified architecture with a one-level page table, taking care to prove it constitutes a separation logic. We then extend the framework to deal with low-level C programs executing in a virtual memory environment of the ARMv6 architecture with a two-level page table. We perform two case studies involving mapping in of a new page into the current address space: first for the simple version of our logic, and finally for our full framework. The case studies demonstrate that separation logic style modular reasoning via the frame rule can be used in a unified model which encompasses virtual memory, even in the presence of page table writes.

To our knowledge, we present the first model offering a unified view of virtual and physical memory, the first separation logic involving an address translation mechanism, as well as the first published model of a functional subset of ARM memory management unit. Our memory models, framework, proofs and all results are formalised in the Isabelle/HOL interactive theorem prover.