CAREER: Automated Verification of Loops in Systems Code

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

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.