Files and links (1)
Preprint (Author's original)arXiv.org - Non-exclusive license to distribute, Open
Preprint
Modal Abstractions for Virtualizing Memory Addresses
arXiv.org
13 Aug 2023
Abstract
Operating system kernels employ virtual memory management (VMM) subsystems to
virtualize the addresses of memory regions in order to to isolate untrusted
processes, ensure process isolation and implement demand-paging and
copy-on-write behaviors for performance and resource controls. Bugs in these
systems can lead to kernel crashes. VMM code is a critical piece of
general-purpose OS kernels, but their verification is challenging due to the
hardware interface (mappings are updated via writes to memory locations, using
addresses which are themselves virtualized). Prior work on VMM verification has
either only handled a single address space, trusted significant pieces of
assembly code, or resorted to direct reasoning over machine semantics rather
than exposing a clean logical interface.
In this paper, we introduce a modal abstraction to describe the truth of
assertions relative to a specific virtual address space, allowing different
address spaces to refer to each other, and enabling verification of instruction
sequences manipulating multiple address spaces. Using them effectively requires
working with other assertions, such as points-to assertions in our separation
logic, as relative to a given address space. We therefore define virtual
points-to assertions, which mimic hardware address translation, relative to a
page table root. We demonstrate our approach with challenging fragments of VMM
code showing that our approach handles examples beyond what prior work can
address, including reasoning about a sequence of instructions as it changes
address spaces. All definitions and theorems mentioned in this paper including
the operational model of a RISC-like fragment of supervisor-mode x86-64, and a
logic as an instantiation of the Iris framework, are mechanized inside Coq.
Metrics
9 Record Views
Details
- Title
- Modal Abstractions for Virtualizing Memory Addresses
- Creators
- Ismail KuruColin S Gordon
- Publication Details
- arXiv.org
- Resource Type
- Preprint
- Language
- English
- Academic Unit
- Computer Science (Computing)
- Other Identifier
- 991021868727004721