SHF: Small: Toward Fully Automated Formal Software Verification

SHF：小型：迈向全自动形式软件验证

• 批准号: 2210243
• 负责人: Yuriy Brun
• 金额: $ 59.99万
• 依托单位: University of Massachusetts Amherst
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2210243&HistoricalAwards=false
• 关键词: SHF; Small; Toward; Fully; Automated

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.

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

项目成果

Better Automatic Program Repair by Using Bug Reports and Tests Together

• DOI: 10.1109/icse48619.2023.00109
• 发表时间: 2020-11
• 期刊: 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)
• 作者: Manish Motwani;Yuriy Brun

Baldur: Whole-Proof Generation and Repair with Large Language Models

• DOI: 10.1145/3611643.3616243
• 发表时间: 2023-03
• 期刊: Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering
• 作者: E. First;M. Rabe;T. Ringer;Yuriy Brun

PRoofster: Automated Formal Verification

PROoofster：自动形式验证

• DOI: 10.1109/icse-companion58688.2023.00018
• 发表时间: 2023
• 期刊: Proceedings of the Demonstrations Track at the 45th International Conference on Software Engineering (ICSE
• 作者: Agrawal, Arpan;First, Emily;Kaufman, Zhanna;Reichel, Tom;Zhang, Shizhuo;Zhou, Timothy;Sanchez-Stern, Alex;Ringer, Talia;Brun, Yuriy
• 通讯作者: Brun, Yuriy

Seldonian Toolkit: Building Software with Safe and Fair Machine Learning

• DOI: 10.1109/icse-companion58688.2023.00035
• 发表时间: 2023-05
• 期刊: 2023 IEEE/ACM 45th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion)
• 作者: Austin Hoag;James E. Kostas;B. C. Silva;P. Thomas;Yuriy Brun

My Model is Unfair, Do People Even Care? Visual Design Affects Trust and Perceived Bias in Machine Learning

我的模型不公平，人们关心吗？

• DOI: 10.1109/tvcg.2023.3327192
• 发表时间: 2023
• 期刊: IEEE Transactions on Visualization and Computer Graphics
• 影响因子: 5.2
• 作者: Gaba, Aimen;Kaufman, Zhanna;Cheung, Jason;Shvakel, Marie;Hall, Kyle Wm;Brun, Yuriy;Bearfield, Cindy Xiong
• 通讯作者: Bearfield, Cindy Xiong