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

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

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