CAREER: Modal Abstractions of Systems Concepts for OS Kernel Verification

Drexel University, Philadelphia PA

Investigators

Abstract

Operating systems (OSes) are software systems that coordinate sharing of hardware between other applications (such as sharing memory without conflict), provide a high-level abstraction of hardware, and include reusable functionality for common program tasks (such as storing and retrieving files from disk). Because they have control over other programs and mediate use of hardware resources, defects in operating system code can compromise the reliability or security of any software running on the OS. Most computers run one of just a few general-purpose operating systems, so a bug in any one of those systems will likely affect very many computers, making their correctness critical to countless computer-based systems used daily around the world. This project explores new ways to mathematically prove correctness properties of operating systems, and thereby to establish conclusively the impossibility of bugs in them. The project's novelties are a focus on verifying realistic OS designs similar to those used in industry, treating significant subtleties of OS control over hardware, and new approaches to specifying correctness for common design patterns in low-level code. The project's impacts are the introduction of new verification techniques for low-level code that are expected to apply more broadly than to operating systems, and integration with education. The project develops new ways of teaching undergraduate automata and computability courses, integrating modern applications from security and software verification to better demonstrate the material's value and improve student engagement. The project brings a range of techniques from modal logic to bear on OS verification, and attempts to show that these techniques support three kinds of reasoning that occur in operating system kernels and systems code in general: location virtualization (as in virtual-memory management and copy-on-write filesystems), caching (including hardware store buffers, translation lookaside buffers, and OS-level caches), and abstraction of a single protocol to be used in multiple different ways but in a compatible manner (as relevant to device driver frameworks). The project constructs a detailed model of the multicore x86-64 architecture, including details of interactions between interrupt handling, virtual memory management, and weak memory models. The project uses the model to implement a small OS following standard OS designs (in particular, using the same standard abstractions for address spaces, device drivers, the virtual filesystem layer, and filesystem caching), and verifies the OS in a Hoare logic extended with new reasoning principles. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.