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

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.