SHF: Small: Toward Fully Automated Formal Software Verification

点击翻译按钮获取中文摘要

Software is a critical part of our society, but, unfortunately, defects in deployed software are typical, and the cost of failures is extremely high. One promising method for improving software quality is formal verification, which enables developers to mathematically prove properties of their code, guaranteeing some aspects of software correctness. But writing such proofs manually is incredibly difficult, even using proof assistants, which are designed to help developers write high-level proof scripts and then automate some of the proof processes. While such tools have seen some success in industry (e.g., Firefox, Chrome, and Android use proof-assistant-verified cryptography libraries for communication), the prohibitively high cost of formal verification has ensured that, today, nearly all the software companies ship is unverified. The central goal of this project is to develop techniques that learn from existing proof scripts to automatically synthesize new ones, fully automating formal verification.The key idea behind this project is (1) to learn a predictive language model from a corpus of existing proof scripts. This predictive model, given a partially written proof script, predicts the likely next proof steps. And then (2) to use metaheuristic search to synthesize potential proofs from scratch, guided by the predictive model and using the proof assistant to constrain the search. The project is organized around three thrusts. The first thrust develops a method for fully automating formal verification of software properties using the Coq proof assistant by modeling the proof script and proof state together. The second thrust uses the inherent diversity of learned language models to increase the proving power of the automated formal verification approach by efficiently combining the power of multiple models. The third thrust develops a language-model-based method for repairing proof scripts that break as part of software evolution. The project improves the state of the art of automated formal verification toward improving software quality and reducing the cost of software debugging and maintenance and contributes to the scientific efforts to improve formal verification with publicly accessible benchmarks and open-source verification systems. The project also contributes to undergraduate and graduate education by incorporating formal verification into relevant courses.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.