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

FMITF：第一轨：在 Arm 多处理器硬件模型上验证系统软件

• 批准号: 2124080
• 负责人: Jason Nieh
• 金额: $ 75万
• 依托单位: Columbia University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2124080&HistoricalAwards=false
• 关键词: FMitF; Track; Verifying; System; Software

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.

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

项目成果

UPGRADVISOR: Early Adopting Dependency Updates Using Hybrid Program Analysis and Hardware Tracing

UPGRADVISOR：使用混合程序分析和硬件跟踪尽早采用依赖项更新

• 发表时间: 2022
• 期刊: Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2022
• 作者: David, Yaniv;Sun, Xudong;Sofaer, Raphael J.;Senthilnathan, Aditya;Yang, Junfeng;Zuo, Zhiqiang;Xu, Guoqing Harry;Nieh, Jason;Gu, Ronghui
• 通讯作者: Gu, Ronghui

Design and Verification of the Arm Confidential Compute Architecture

• 发表时间: 2022
• 作者: Xupeng Li;Xuheng Li;Christoffer Dall;Ronghui Gu;Jason Nieh;Yousuf Sait;Gareth Stockwell

Effective Performance Issue Diagnosis with Value-Assisted Cost Profiling

通过价值辅助成本分析进行有效的性能问题诊断

• DOI: 10.1145/3552326.3587444
• 发表时间: 2023
• 期刊: Proceedings of the 18th European Conference on Computer Systems
• 作者: Weng, Lingmei;Hu, Yigong;Huang, Peng;Nieh, Jason;Yang, Junfeng
• 通讯作者: Yang, Junfeng

BlackBox: A Container Security Monitor for Protecting Containers on Untrusted Operating Systems

• 发表时间: 2022
• 作者: Alexander Van't Hof;Jason Nieh

DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols

DuoAI：用于验证分布式协议的归纳不变量的快速自动推理

• 发表时间: 2022
• 期刊: Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2022
• 作者: Yao, Jianan;Tao, Runzhou;Gu, Ronghui;Nieh, Jason
• 通讯作者: Nieh, Jason