FMitF: Track I: A Secure and Verifiable Commodity Hypervisor

云计算提供商广泛部署虚拟机管理程序来支持虚拟机（VM），但其日益增长的复杂性带来了安全风险，因为大型代码库包含许多漏洞。一个受损的虚拟机管理程序会危及其所有虚拟机的数据和隐私--这对云提供商和用户来说都是不可取的结果。在当今数据驱动的世界中，数据的机密性和完整性至关重要。该项目将设计、实施、验证和评估一种全新的虚拟机管理程序设计方法，为商用虚拟机管理程序提供一个小型的、经过验证的可信计算基础（TCB），以保护在云中运行的虚拟机的机密性和完整性。 该项目的创新之处在于新的hypervisor架构和形式验证框架。该项目的影响是为系统软件验证方面的未来创新奠定基础，特别是云计算基础设施，并验证Linux中的开源虚拟化技术，以推动研究创新，使其能够在商业系统中采用。该项目设计了一种新颖的虚拟机管理程序架构，该架构将虚拟机管理程序划分为执行基本虚拟化的可信核心和执行其他虚拟机管理程序功能并可与主机操作系统集成的不可信主机。调查人员研究了传统虚拟机管理程序的功能，并确定核心只需要安全的靴子和基本的CPU和内存虚拟化，从而产生了一个明显更简单和可验证的虚拟机管理程序核心。该项目采用了一种新的形式验证框架命名为认证抽象层（CAL）的原因的正确性（即，实现符合其规范）和安全性（即，规范保证虚拟机的机密性和完整性）的hypervisor核心与不可信的主机。该项目改造和验证了Linux内核虚拟机（KVM）虚拟机管理程序，展示了这些验证技术在实际中与商品虚拟机管理程序软件一起工作的能力。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Hypervisors are widely deployed by cloud- computing providers to support virtual machines (VMs), but their growing complexity poses a security risk as large codebases contain many vulnerabilities. A compromised hypervisor risks the data and privacy of all its VMs -- an undesirable outcome for both cloud providers and users. In today's data-driven world, data confidentiality and integrity are of crucial importance. This project will design, implement, verify, and evaluate a fundamentally new approach to hypervisor design that provides a small, verified trusted computing base (TCB) for commodity hypervisors to protect the confidentiality and integrity of VMs running in the cloud. The project's novelties are a new hypervisor architecture and formal-verification framework. The project's impacts are providing a foundation for future innovations in the verification of systems software, especially for cloud-computing infrastructure, and verifying open-source virtualization technologies in Linux to drive research innovation in a way that can be adopted in commercial systems. This project designs a novel hypervisor architecture that partitions the hypervisor into a trusted core that performs basic virtualization, and an untrusted host that performs other hypervisor functionality and can be integrated with a host operating system. The investigators examine features of traditional hypervisors and identify only secure boot and basic CPU and memory virtualization as necessary for the core, resulting in a significantly simpler and verifiable hypervisor core. This project adopts a novel formal-verification framework named certified abstraction layers (CAL) to reason about the correctness (that is, the implementation meets its specification) and security (that is, the specification guarantees VM confidentiality and integrity) of the hypervisor core with an untrusted host. This project retrofits and verifies the Linux Kernel Virtual Machine (KVM) hypervisor, demonstrating the ability of these verification techniques to work in practice with commodity hypervisor software.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.