Commodity hypervisors are widely deployed to support virtual machines on multiprocessor server hardware. Modern hypervisors are complex and often integrated with an operating system kernel, posing a significant security risk as writing large, multiprocessor systems software is error-prone. Attackers that successfully exploit hypervisor vulnerabilities may gain unfettered access to virtual machine data and compromise the confidentiality and integrity of virtual machine data. Theoretically, formal verification offers a solution to this problem, by proving that the hypervisor implementation contains no vulnerabilities and protects virtual machine data under all circumstances. However, it remains unknown how one might feasibly verify the entire codebase of a complex, multiprocessor commodity system. My thesis is that modest changes to a commodity system can reduce the required proof effort such that it becomes possible to verify the security properties of the entire system. This dissertation introduces microverification, a new approach for formally verifying the security properties of commodity systems. Microverification reduces the proof effort for a commodity system by retrofitting the system into a small core and a set of untrusted services, thus making it possible to reason about properties of the entire system by verifying the core alone. To verify the multiprocessor hypervisor core, we introduce security-preserving layers to modularize the proof without hiding information leakage so we can prove each layer of the implementation refines its specification, and the top layer specification is refined by all layers of the core implementation. To verify commodity hypervisor features that require dynamically changing information flow, we incorporate data oracles to mask intentional information flow. We can then prove noninterference at the top layer specification and guarantee the resulting security properties hold for the entire hypervisor implementation. Using microverification, we retrofitted the Linux KVM hypervisor with only modest modifications to its codebase. Using Coq, we proved that the hypervisor protects the confidentiality and integrity of VM data, including correctly managing tagged TLBs, shared multi-level page tables, and caches. Our work is the first machine-checked security proof for a commodity multiprocessor hypervisor. Experimental results with real application workloads demonstrate that verified KVM retains KVM’s functionality and performance.

For software to take advantage of modern multicore processors, it must be safely concurrent and it must scale. Many techniques that allow safe concurrency do so at the expense of scalability. Coarse grain locking allows multiple threads to access common data safely, but not at the same time. Non-Blocking Synchronization and Transactional Memory techniques optimistically allow concurrency, but only for disjoint accesses and only at a high performance cost. Relativistic programming is a technique that allows low overhead readers and joint access parallelism between readers and writers. Most of the work on relativistic programming has assumed a single writer at a time (or, in partitionable data structures, a single writer per partition), and single writer solutions cannot scale on the write side. This dissertation extends prior work on relativistic programming in the following ways: 1) It analyses the ordering requirements of lock-based and relativistic programs in order to clarify the differences in their correctness and performance characteristics, and to define precisely the behavior required of the relativistic programming primitives. 2) It shows how relativistic programming can be used to construct efficient, scalable algorithms for complex data structures whose update operations involve multiple writes to multiple nodes. 3) It shows how disjoint access parallelism can be supported for relativistic writers, using Software Transactional Memory, while still allowing low-overhead, linearly-scalable, relativistic reads.