CAREER: Computing Program Invariants using Abstract Domains Search

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

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.