SHF: Small: Toward Fully Automated Formal Software Verification

软件是我们社会的关键部分，但不幸的是，部署的软件中的缺陷是典型的，故障的成本非常高。提高软件质量的一种很有前途的方法是形式验证，它使开发人员能够从数学上证明他们代码的属性，从而保证软件的某些方面的正确性。但手动编写这样的证明是极其困难的，即使使用证明助手也是如此，证明助手旨在帮助开发人员编写高级证明脚本，然后自动执行一些证明过程。虽然这类工具在行业中取得了一些成功(例如，Firefox、Chrome和Android使用验证助手验证的密码库进行通信)，但正式验证的高得令人望而却步的成本确保了今天，几乎所有发布的软件公司都是未经验证的。这个项目的中心目标是开发从现有证明脚本中学习的技术，以自动合成新的证明脚本，完全自动化形式验证。该项目背后的关键思想是(1)从现有证明脚本语料库中学习预测语言模型。这个预测模型，给出了一个部分编写的证明脚本，预测了可能的下一个证明步骤。然后(2)在预测模型的指导下，使用元启发式搜索从零开始合成潜在的证明，并使用证明辅助来约束搜索。该项目围绕三个方面展开。第一个推力是开发一种方法，通过对证明脚本和证明状态一起建模，使用CoQ证明助手来完全自动化软件属性的正式验证。第二个推力利用学习语言模型固有的多样性，通过有效地结合多个模型的能力来增加自动形式验证方法的证明能力。第三个推力开发了一种基于语言模型的方法，用于修复作为软件演化的一部分而中断的证明脚本。该项目改进了自动化形式验证的技术水平，以提高软件质量，降低软件调试和维护的成本，并有助于通过公开可访问的基准和开放源码验证系统改进正式验证的科学努力。该项目还通过将正式验证纳入相关课程，为本科生和研究生教育做出贡献。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.