FMitF: A Framework for Synthesis of Efficient, Reliable, and Secure Operating System Components

University Of Washington, Seattle WA

Investigators

Abstract

The operating system is a critical part of every computing device, from mobile phones to cloud servers. It consists of core software components, such as the kernel and the file system, that mediate the interaction between user applications and the underlying hardware. Bugs in these components have wide-ranging impact on systems in use every day, from causing crashes and slowdowns to allowing attackers to take over the entire system. This project develops Synix, a transformative new approach to building operating system components that eliminates entire classes of such bugs. Synix is based on automated program synthesis, and it is the first effort to synthesize a broad range of key operating system components, providing formal guarantees of efficiency, reliability, and security. By extending the scalability and reach of program synthesis to the domain of operating systems, Synix advances the state-of-the-art in formal methods and in the design of software components that underpin our computing infrastructure. Synix takes the form of a novel framework for synthesis-aided development of efficient, reliable, and secure operating system components. The PIs prior work on push-button verification of kernels and file systems has demonstrated that it is feasible to verify the safety and security of these components fully automatically and with low specification burden. The enabling idea behind push-button verification is to design component interfaces to be finite so that the semantics of each interface procedure is expressible as a set of traces of bounded length. The main insight behind Synix is that finite interfaces are also an ideal target for syntax-guided synthesis. The research goal of this project is thus to develop new techniques for synthesizing efficient implementations of three classes of core operating system components with finite interfaces: (1) a just-in-time compiler for a given in-kernel interpreter, (2) a crash-safe file system for a given storage interface, and (3) a security monitor for a given application-level isolation policy. The driving idea underpinning the proposed solutions is to use self hosting, write-before relations, and narrow finite interfaces to decompose the target synthesis problems into more tractable synthesis tasks. The practical and educational goals of this project are to apply Synix to synthesize real operating system configurations, thus facilitating adoption; release the resulting tools as open-source software; actively support the tools users; and disseminate key results through papers, lectures, and tutorials. 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.