Verification of programs in virtual memory using separation logic

Download files
Access & Terms of Use
open access
Copyright: Kolanski, Rafal Michal
Altmetric
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.
Persistent link to this record
Link to Publisher Version
Link to Open Access Version
Additional Link
Author(s)
Kolanski, Rafal Michal
Supervisor(s)
Klein, Gerwin
Elphinstone, Kevin
Creator(s)
Editor(s)
Translator(s)
Curator(s)
Designer(s)
Arranger(s)
Composer(s)
Recordist(s)
Conference Proceedings Editor(s)
Other Contributor(s)
Corporate/Industry Contributor(s)
Publication Year
2011
Resource Type
Thesis
Degree Type
PhD Doctorate
UNSW Faculty
Files
download whole.pdf 1.37 MB Adobe Portable Document Format
Related dataset(s)