CAREER: Computing Program Invariants using Abstract Domains Search

职业：使用抽象域搜索计算程序不变量

• 批准号: 1942044
• 负责人: Elena Sherman
• 金额: $ 47.35万
• 依托单位: Boise State University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-06-01 至 2025-05-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1942044&HistoricalAwards=false
• 关键词: CAREER; Computing; Program; Invariants; using

Computer software has become embedded in the very fabric of how society works and plays. However, as software continues to increase in size and complexity, program analysts and software engineers find it increasingly challenging to keep computer software secure, reliable, and safe. To do so, they use what is called software verification. Program invariants are an essential part of software verification; they are summaries of possible program behaviors. Unfortunately, current methods for computing program invariants are not keeping pace with software complexity, resulting in approaches that do not scale well, or which compute imprecise, i.e., weak program invariants. In addition, while better strategies for developing program invariants are available, they are too difficult for most engineers to apply without highly specialized training. This project will produce novel techniques to overcome these limitations to compute strong program invariants, and to do so far more easily. Since program invariants touch on so many parts of software engineering such as generating, debugging, verifying, and optimizing computer code, improved accuracy and efficiency can transform software development. In addition, the investigator at Boise State University in Boise, Idaho will work closely with regional industry professionals both to enhance their verification training, as well as to collaborate in co-developing a graduate-level class on applied program analysis.The project will use an approach for computing program invariants called abstract interpretation. Key to effective abstract interpretation is choosing an appropriate abstraction level for static code analysis. On the one hand, if the abstraction is too fine, it will not scale well. On the other hand, if the abstraction is too coarse, it will compute weak invariants. This project will result in a novel approach for finding suitable abstractions that allows for a scalable, precise, and far more accessible method of computing program invariants. The resulting Search-based Static Analysis (SBSA) framework will significantly improve upon current static analysis methods and use search techniques to automatically optimize abstract interpreter configurations. It will also facilitate new research directions that require strong program invariants. There are three project objectives, to: (1) investigate search techniques to find the best abstract domain, (2) explore mechanisms for guiding the abstract domain search based on software concrete semantics, and (3) improve precision by strategically partitioning software into components and then analyzing them separately to enable better search.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.

计算机软件已经嵌入到社会运作和娱乐的结构中。然而，随着软件的规模和复杂性不断增加，程序分析师和软件工程师发现保持计算机软件安全、可靠和安全越来越具有挑战性。为此，他们使用所谓的软件验证。程序不变量是软件验证的重要组成部分；它们是可能的程序行为的摘要。不幸的是，当前计算程序不变量的方法没有跟上软件复杂性的步伐，导致方法不能很好地扩展，或者计算不精确，即程序不变量较弱。此外，虽然可以使用更好的策略来开发程序不变量，但对于大多数工程师来说，如果没有高度专业化的培训就很难应用它们。该项目将产生新颖的技术来克服这些限制，以计算强大的程序不变量，并且更容易做到这一点。由于程序不变量涉及软件工程的许多部分，例如生成、调试、验证和优化计算机代码，因此提高准确性和效率可以改变软件开发。此外，位于爱达荷州博伊西的博伊西州立大学的研究人员将与地区行业专业人士密切合作，加强他们的验证培训，并合作共同开发应用程序分析的研究生课程。该项目将使用一种计算程序不变量的方法，称为抽象解释。有效抽象解释的关键是为静态代码分析选择适当的抽象级别。一方面，如果抽象太精细，就无法很好地扩展。另一方面，如果抽象太粗糙，它将计算弱不变量。该项目将产生一种新的方法来寻找合适的抽象，从而实现可扩展、精确且更易于访问的计算程序不变量的方法。由此产生的基于搜索的静态分析（SBSA）框架将显着改进当前的静态分析方法，并使用搜索技术自动优化抽象解释器配置。它还将促进需要强大的程序不变量的新研究方向。项目有三个目标：(1) 研究搜索技术以找到最佳抽象域，(2) 探索基于软件具体语义指导抽象域搜索的机制，以及 (3) 通过策略性地将软件划分为组件来提高精度该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Incremental Transitive Closure for Zonal Abstract Domain

区域抽象域的增量传递闭包

• DOI: 10.1007/978-3-031-06773-0_43
• 发表时间: 2022
• 期刊: NASA Formal Methods
• 作者: Ballou, Kenny;Sherman, Elena
• 通讯作者: Sherman, Elena