CAREER: Automated Verification of Loops in Systems Code

职业：系统代码中循环的自动验证

• 批准号: 2239484
• 负责人: Ronghui Gu
• 金额: $ 52.5万
• 依托单位: Columbia University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-02-01 至 2028-01-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2239484&HistoricalAwards=false
• 关键词: CAREER; Automated; Verification; Loops; Systems

System software such as operating systems and hypervisors forms the software foundations of our computing infrastructure. Formally verifying the correctness and security of system software is highly demanding but comes at a considerable cost especially when there are many loops. Complex system software typically requires months of verification effort into loops alone. This project is designing, implementing, and evaluating Ashera, a data-driven framework for automatically verifying loops in systems code. The project’s novelties are the introduction of a new learning architecture, Recursive Continuous Logic Networks (R-CLNs), for learning loop invariants using system execution traces. This project, for the first time, enables automated verification for complex loops in real-world systems code and will be a crucial step to scale formal verification techniques for building modern resilient system software so that everyone can have access to trustworthy computing environments.Ashera verifies loops by inferring and validating loop invariants, which capture the effect of the loop on the program state irrespective of the actual number of loop iterations. These invariants for systems code usually contain quantifiers and recursive functions over iterative data structures, which are difficult and time-consuming to manually infer and prove, even for verification experts. To tackle these challenges, Ashera introduces R-CLN, a neural architecture specialized for learning quantified and recursive loop invariants using novel training data collected from execution traces of the target program, such as sliding windows and randomized history windows. Ashera incorporates a Dafny-based validation scheme and translators for C, Go, and Coq proof assistant, such that a system designer only needs to provide pre- and post-conditions of the loop in order for the learning framework to sample, infer, and validate an invariant. This project will use Ashera to conduct end-to-end, automated verification for loops in all major verified systems and several real systems, including KVM, the Linux Buddy system, and the Linux page fault handler, which was previously considered intractable, demonstrating that Ashera is capable of scaling verification for system 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.

操作系统和虚拟机管理程序等系统软件构成了计算基础设施的软件基础。形式上验证系统软件的正确性和安全性要求很高，但成本相当高，特别是当有许多循环时。复杂的系统软件通常需要几个月的验证工作才能进入循环。该项目正在设计，实现和评估Ashera，这是一个数据驱动的框架，用于自动验证系统代码中的循环。该项目的新颖之处是引入了一种新的学习架构，递归连续逻辑网络（R-CLN），用于使用系统执行跟踪学习循环不变量。该项目首次实现了对真实世界系统代码中复杂循环的自动验证，并将成为扩展形式验证技术以构建现代弹性系统软件的关键一步，以便每个人都可以访问可信的计算环境。Ashera通过推断和验证循环不变量来验证循环，其捕获循环对程序状态的影响，而不管循环迭代的实际次数。这些系统代码的不变量通常包含迭代数据结构上的量词和递归函数，即使对于验证专家来说，手动推断和证明也是困难和耗时的。为了应对这些挑战，Ashera引入了R-CLN，这是一种神经架构，专门用于使用从目标程序的执行轨迹（如滑动窗口和随机历史窗口）收集的新训练数据来学习量化和递归循环不变量。Ashera集成了基于Dafny的验证方案和用于C、Go和Coq证明助手的翻译器，因此系统设计人员只需要提供循环的前置和后置条件，以便学习框架对不变量进行采样、推断和验证。该项目将使用Ashera对所有主要验证系统和几个真实的系统（包括KVM、Linux Buddy系统和Linux页面错误处理程序）中的循环进行端到端的自动验证，这在以前被认为是棘手的，该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的学术价值和更广泛的影响审查标准。

项目成果

Spoq: Scaling Machine-Checkable Systems Verification in Coq

• 发表时间: 2023
• 期刊: ArXiv
• 作者: Xupeng Li;Xuheng Li;Wei Qiang;Ronghui Gu;Jason Nieh

Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions

具有排名功能的分布式协议的活性属性的自动验证

• DOI: 10.1145/3632877
• 发表时间: 2024
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Yao, Jianan;Tao, Runzhou;Gu, Ronghui;Nieh, Jason
• 通讯作者: Nieh, Jason