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

FMITF：高效、可靠和安全操作系统组件的综合框架

• 批准号: 1836724
• 负责人: Zachary Tatlock
• 金额: $ 98万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1836724&HistoricalAwards=false
• 关键词: FMitF; Framework; Synthesis; Efficient; Reliable

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.

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

项目成果

Noninterference specifications for secure systems

• DOI: 10.1145/3421473.3421478
• 发表时间: 2020-08
• 期刊: ACM SIGOPS Operating Systems Review
• 作者: Luke Nelson;James Bornholt;A. Krishnamurthy;Emina Torlak;Xi Wang

Fixing Code That Explodes Under Symbolic Evaluation

修复在符号求值下爆炸的代码

• 发表时间: 2020
• 期刊: and Abstract Interpretation (VMCAI'20
• 作者: Porncharoenwase, Sorawee;Bornholt, James;Torlak, Emina
• 通讯作者: Torlak, Emina

Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel

现场规范和验证：将形式化方法应用于 Linux 内核中的 BPF 即时编译器

• 发表时间: 2020
• 期刊: 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20
• 作者: Nelson, Luke;Van Geffen, Jacob;Torlak, Emina;Wang, Xi
• 通讯作者: Wang, Xi

A formal foundation for symbolic evaluation with merging

合并符号评估的正式基础

• DOI: 10.1145/3498709
• 发表时间: 2022
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Porncharoenwase, Sorawee;Nelson, Luke;Wang, Xi;Torlak, Emina
• 通讯作者: Torlak, Emina

Synthesizing JIT Compilers for In-Kernel DSLs

• DOI: 10.1007/978-3-030-53291-8_29
• 发表时间: 2020-06-16
• 期刊: Computer Aided Verification
• 作者: Van Geffen J;Nelson L;Dillig I;Wang X;Torlak E
• 通讯作者: Torlak E