Modal abstractions for operating system kernels

Ismail Kuru

doi:10.17918/00010934

Operating-System kernels are important pieces of the software world. They interact with the hardware and their reliability is essential, as the rest of the software world depends on it. There are certain aspects that make verifying kernels challenging, and this thesis captures principles dealing with three of these aspects. The first challenge stems from the sharing of a resource among different kernel abstractions (and their particular instances) through an indirection mechanism employed between address (alias) and the data (virtualization). As the first contribution of this thesis, we introduce reasoning principles for understanding location virtualization in kernels. Location virtualization appears in multiple components of the kernel, including memory and file resource virtualization. In this thesis, we take virtual memory management (VMM) as our experimental setting to apply our reasoning principles. VMM code is a critical piece of general-purpose OS kernels, but verification of this functionality is challenging due to the complexity of the hardware interface (the page tables are updated via writes to those memory locations, using addresses that are themselves virtualized). Prior work on verification of VMM code 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 thesis, we introduce a modal abstraction to describe the truth of assertions relative to a specific virtual address space: [r]P indicating that P holds in the virtual address space rooted at r. Such modal assertions allow different address spaces to refer to each other, enabling complete verification of instruction sequences and manipulating multiple address spaces. Using them effectively requires working with other assertions, such as points-to assertions in our separation logic, relative to a given address space. We therefore define virtual points-to relations, which mimic hardware address translation, relative to a page table root. The second challenge appears when we extend the kernel functionality. It is common for any software to expect certain API usage to follow a protocol, and it is particularly common in OS kernels, where the protocols are essentially the contracts for extension points. Any kernel, in one way or another, realizes mechanisms that allow us to plug in different implementations of the same functionality. For example, Virtual File System (VFS) enables different filesystem implementations to coexist, or device drivers require extensions with respect to the changing device capabilities. In doing so, these mechanisms impose certain protocols which may internally have simpler or more complex usage protocols that are *compatible* with the official interface. This constitutes the second challenge, as any change in the protocol brings into question whether the validity (or reliability) of the client code is still valid or not (evolution). As the second contribution of this thesis, we want to let proofs capture and exploit the compatibility of the client proofs against the evolution of the specifications. To do so, we introduce a single-form logical abstraction for specifying protocols that are abstracted as state transition systems (STS)es. STSes are an increasingly popular means of specifying and verifying fine-grained concurrent programs. Unlike more traditional rely-guarantee-based approaches, they allow interference to be conveniently treated as a resource, transferred between threads, or even stored in other resources. However, existing STS systems leave the traditional Hoare-style rule of consequence weaker than before. Code involving STSes is verified against one particular STS, making it unusable with other similar transition systems, even when one is contained in the other. We extend the notion of entailment for STS-based logics to incorporate a form of bisimulation (as on Kripke structures) between STS systems into an extended rule of consequence. We show that a specification of a file write operation preserves its validity against a file resource usage protocol changed to handle distributed write requests. The third challenge this thesis is concerned with is ergonomics of assertions that may be useful for the correct usage of the constructs that are exposed as a kernel API. One of the common constructs appearing in kernel APIs are concurrency constructs (e.g., reader-writer locks). As low-level systems, kernels are expected to be more efficient. Thus, in them, more highly optimized sharing mechanisms and data structures are implemented using these sharing mechanisms. As a critical piece, memory management in lock-free data structures is promising but is a major challenge in concurrent programming. Design techniques, including read-copy-update (RCU) and hazard pointers, provide workable solutions and are widely used to great effect. These techniques rely on the concept of a grace period: nodes that should be freed are placed on a deferred free list, and all threads obey a protocol to ensure that the deallocating thread can detect when all possible readers have completed their use of the object. This provides an approach to safe deallocation, but only when these subtle protocols are implemented correctly. In other words, the reasoning principles for this kind of semantics must refer to the representation of the contingent-truth referring to the consistency of the program state with respect to a certain grace period. We present a static type system to ensure correct use of RCU memory management: that nodes removed from a data structure are always scheduled for subsequent deallocation, and that nodes are scheduled for deallocation at most once. As part of our soundness proof, we give an abstract semantics for RCU memory management primitives that captures the fundamental properties of RCU. Our type system allows us to give the first proofs of memory safety for RCU linked list and binary search tree implementations without requiring full verification. In conclusion, we explain a general verification approach shaped around the concept of resource context that helps to design new modalities to verify the system code. We justify our perspective by identifying existing systems that have used modalities for systems verification successfully, arguing that they fit into the verification design pattern we articulate, and explaining how this approach might apply to other systems verification challenges.

Modal abstractions for operating system kernels

Files and links (1)

Abstract

Metrics

Details

Modal abstractions for operating system kernels

Files and links (1)

Abstract

Metrics

Details

Drexel University Social media