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