CAREER: A Framework for Automated Verification of Hypervisors

职业：虚拟机管理程序自动验证框架

• 批准号: 1844807
• 负责人: Xi Wang
• 金额: $ 56.96万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-06-01 至 2024-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1844807&HistoricalAwards=false
• 关键词: CAREER; Framework; Automated; Verification; Hypervisors

Hypervisors are an essential component of modern computing devices, from personal laptops to cloud servers. They create the illusion of having multiple physical machines and provide vital support for resource management. Software bugs have proliferated due to the increasing complexity of modern hypervisors; such bugs can cause issues ranging from performance degradation to security vulnerabilities that allow malicious virtual machines to compromise the entire system. This project, IsoV, is to build highly reliable and secure hypervisors through the use of automated verification techniques that effectively eliminate entire classes of software bugs.IsoV will provide novel programming support for developing hypervisors and for formally verifying their correctness and isolation guarantees. The novelty in the project lies in the ideas behind the push-button approach to hypervisor design. The main idea of push-button verification is to design the interfaces of these systems to be finite and amenable to automated verification. The research goal of IsoV is to develop new designs and techniques for automated verification of hypervisors. This project focuses on two common classes of hypervisors: those that provide isolated execution environments to shield applications from untrusted or buggy operating systems; and those that safely partition resources among mutually distrustful virtual machines. The practical and educational goals of this project are to apply IsoV in building real systems; to release the tools and systems as open-source software; and to disseminate results widely.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.

虚拟机管理程序是现代计算设备（从个人笔记本电脑到云服务器）的重要组成部分。它们营造出拥有多台物理机器的错觉，并为资源管理提供重要支持。由于现代管理程序的复杂性不断增加，软件错误激增；此类错误可能会导致各种问题，从性能下降到允许恶意虚拟机危害整个系统的安全漏洞。这个名为 IsoV 的项目旨在通过使用自动验证技术来构建高度可靠和安全的虚拟机管理程序，从而有效地消除整个类别的软件错误。IsoV 将为开发虚拟机管理程序以及正式验证其正确性和隔离保证提供新颖的编程支持。该项目的新颖之处在于管理程序设计的按钮方法背后的想法。按钮验证的主要思想是将这些系统的接口设计得有限且适合自动验证。 IsoV 的研究目标是开发用于虚拟机管理程序自动验证的新设计和技术。该项目重点关注两类常见的虚拟机管理程序：提供隔离执行环境以保护应用程序免受不受信任或有缺陷的操作系统影响的虚拟机管理程序；以及提供隔离执行环境的虚拟机管理程序。以及在相互不信任的虚拟机之间安全地划分资源的技术。该项目的实践和教育目标是应用 IsoV 构建真实系统；将工具和系统作为开源软件发布；该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

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

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

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