CAREER: Automated Verification of Loops in Systems Code

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.