FMitF: Track I: Verifying System Software on an Arm Multiprocessor Hardware Model

软件缺陷和漏洞对软件系统构成重大安全风险，这些软件系统是当今计算基础设施的基础，例如操作系统内核和系统管理程序。这些风险因在现代硬件上运行的软件的日益复杂而增加，因为在复杂硬件上执行的复杂软件中的漏洞更容易被忽视。形式验证通过证明系统软件被正确实现，为这个问题提供了一个潜在的解决方案。不幸的是，现有的经过验证的软件系统基于过于简化的硬件模型，这意味着经过验证的属性可能无法反映软件在实际硬件上的行为。为了解决这个问题，这个项目正在设计、实现和评估VARM，这是一个验证框架，用于在现实的ARM多处理器硬件模型上验证复杂系统软件。该项目的新奇之处在于：(1)一个新的硬件模型，它忠实地捕捉了多处理器ARM硬件的行为；(2)一个高度抽象的机器模型，用于推理同步良好的多处理器程序；(3)一个结合了这些模型的多层框架。这种组合既准确又易于使用，因此真正的系统软件可以首次在ARM多处理器硬件上进行验证。VArm引入了一种新颖的分层方法，将详细的底层机器模型RealArm逐步提炼成更简单的抽象模型AbsArm。RealArm是一个真实而正确地反映ARM多处理器硬件行为的硬件模型。此行为包括宽松的内存一致性、标记的转换后备缓冲区(TLB)、共享页表和高速缓存一致性。AbsArm是一个高度抽象的机器模型，它隐藏或简化了低级硬件功能。然而，AbsArm允许对同步良好的程序进行验证，就好像它们几乎是连续的一样，同时仍然确保ARM多处理器硬件的证明成立。该项目将展示RealArm为同步良好的程序改进AbsArm，从而对AbsArm的验证保证也适用于RealArm。为了证明其有效性，研究人员计划使用VARM重新验证各种系统，如基于内核的虚拟机(KVM)，以便他们的证明将适用于ARM多处理器硬件。该项目将取消以前的限制性假设，如顺序一致性和不共享页表。这将是第一批经验证符合实际多处理器硬件模型的系统软件正确性证明。该奖项反映了NSF的法定使命，并已通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Software bugs and vulnerabilities pose major security risks for software systems that provide the foundation for today’s computing infrastructure, such as Operating System kernels and hypervisors. These risks are increased by the growing complexity of software running on modern hardware, as vulnerabilities are much more easily overlooked in complex software executing on sophisticated hardware. Formal verification offers a potential solution to this problem by proving that the system software is implemented correctly. Unfortunately, existing verified software systems are based on over-simplified hardware models, meaning proven properties may not reflect the software’s behavior on real hardware. To address this problem, this project is designing, implementing, and evaluating VArm, a verification framework for verifying complex systems software over a realistic ARM multiprocessor hardware model. This project’s novelties are (1) a novel hardware model that faithfully captures the behavior of multiprocessor ARM hardware, (2) a highly abstract machine model for reasoning about well-synchronized multiprocessor programs, and (3) a multi-layered framework that combines these models. The combination is accurate yet easy to use such that real system software can, for the first time, be verified over ARM multiprocessor hardware. The project's impacts are to improve the state-of-the-art of formal-verification methods and reduce security risks for real-world software systems.VArm introduces a novel layered approach, gradually refining a detailed low-level machine model, RealArm, to a simpler abstract model, AbsArm. RealArm is a hardware model that faithfully and correctly reflects ARM multiprocessor hardware behavior. This behavior includes relaxed memory consistency, tagged Translation Look-aside Buffers (TLBs), shared page tables, and cache coherence. AbsArm is a highly abstract machine model that hides or simplifies low-level hardware features. Nevertheless, AbsArm allows well-synchronized programs to be verified as if they were almost sequential while still ensuring the proofs hold for ARM multiprocessor hardware. The project will show that RealArm refines AbsArm for well-synchronized programs, such that verified guarantees on AbsArm also hold on RealArm. To demonstrate its effectiveness, the researchers plan to use VArm to re-verify various systems such as Kernel-based Virtual Machine (KVM) such that their proofs will hold on ARM multiprocessor hardware. The project will remove previously limiting assumptions such as sequential consistency and no sharing of page tables. These will be the first correctness proofs of system software that are verified to hold on a realistic multiprocessor hardware model.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.