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

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

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.