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

从移动电话到云服务器，操作系统是每个计算设备的关键部分。它由核心软件组件（如内核和文件系统）组成，它们调解用户应用程序和底层硬件之间的交互。这些组件中的漏洞对每天使用的系统有广泛的影响，从导致崩溃和减速到允许攻击者接管整个系统。该项目开发了Synix，这是一种构建操作系统组件的变革性新方法，可以消除所有此类错误。Synix是基于自动程序合成的，它是合成广泛的关键操作系统组件的第一个努力，提供了效率、可靠性和安全性的正式保证。通过将程序合成的可扩展性和范围扩展到操作系统领域，synnix在形式化方法和支撑计算基础设施的软件组件设计方面取得了最新进展。Synix采用了一种新型框架的形式，用于合成辅助开发高效、可靠和安全的操作系统组件。pi先前在内核和文件系统的按钮验证方面的工作表明，以低规范负担全自动验证这些组件的安全性和安全性是可行的。按钮验证背后的支持思想是将组件接口设计为有限的，以便每个接口过程的语义可以表示为一组有界长度的轨迹。synnix背后的主要见解是，有限接口也是语法引导合成的理想目标。因此，该项目的研究目标是开发新技术，以综合具有有限接口的三类核心操作系统组件的有效实现：(1)针对给定内核内解释器的即时编译器，(2)针对给定存储接口的崩溃安全文件系统，以及(3)针对给定应用程序级隔离策略的安全监视器。支持所建议的解决方案的驱动思想是使用自托管、write-before关系和狭窄的有限接口来将目标合成问题分解为更易于处理的合成任务。本项目的实用和教育目标是应用Synix来综合实际的操作系统配置，从而促进采用；将生成的工具作为开源软件发布；积极支持工具用户；并通过论文、讲座和教程传播关键成果。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.