SHF:Small:Scalable and Precise Program Analyses via Linear Conjunctive Language Reachability

静态程序分析提供了基础和实用的技术来帮助构建可靠和安全的软件。上下文无关语言（CFL）可达性已被广泛用于指定程序分析问题。然而，在推进 CFL 可达性框架本身方面几乎没有取得任何基础性进展。为了支持精确和可扩展的程序分析，需要一类富有表现力、易于理解的形式语言可达性来连接基础形式语言研究和基于实用分析的工具开发。该项目的新颖性是双重的：用于指定程序分析的新的强大形式主义，以及用于实现基于该形式主义的实用框架的算法和技术。该项目的影响是加深了对构建精确和可扩展的静态分析以及提高软件可靠性和安全性的实用分析的了解和提高的能力。该项目将探索线性连接语言（LCL）可达性作为一种新的静态分析形式。 与 CFL 相比，LCL 在所有集合论运算下都是封闭的，并且还可以在二次时间内有效地识别。 大量高级程序分析需要同时匹配多个 CFL 描述的属性。 LCL 可以精确地表达许多此类属性，而 CFL 则不能，因为它们在交集下不闭合。因此，拼箱可达性为指定和实现程序分析提供了一个新颖的视角。研究人员在 LCL 可达性方面的初步工作显示出相当大的前景，导致更精确和数量级更大的可扩展别名和污点分析，这两种广泛使用的分析。 该项目旨在通过开发统一的解决方案来指定 LCL 中的程序分析问题并实现支持高效 LCL 可达性算法的新颖数据结构，从而充分发挥 LCL 可达性的潜力。它侧重于 (1) LCL 可达性公式的理论发展，(2) 计算 LCL 可达性的有效算法，以及 (3) 推广到实际程序分析。如果成功，该项目将显着推进软件分析和验证领域的最先进水平。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

Static program analysis provides foundational and practical techniques to help build reliable and secure software. Context-free language (CFL) reachability has been widely adopted for specifying program analysis problems. However, little foundational progress exists on advancing the CFL-reachability framework itself. To support precise and scalable program analyses, an expressive, accessible class of formal language reachability is needed to bridge fundamental formal language research and practical analysis-based tool development. The project's novelties are twofold: a new powerful formalism for specifying program analyses, and algorithms and techniques for realizing a practical framework based on this formalism. The project's impacts are deepened knowledge on and improved capabilities for building precise and scalable static analyses, as well as practical analyses for improving software reliability and security.This project will explore linear conjunctive language (LCL) reachability as a new static analysis formalism. In contrast to CFLs, LCLs are closed under all set-theoretic operations and can also be efficiently recognized in quadratic time. A significant number of advanced program analyses need to match properties described by multiple CFLs simultaneously. LCLs can precisely express many such properties, while CFLs cannot because they are not closed under intersection. Thus, LCL reachability offers a novel perspective in specifying and realizing program analyses. The investigators' initial work on LCL-reachability has shown considerable promise, leading to both more precise and orders of magnitude more scalable alias and taint analysis, two widely-used analyses. This project aims to fully exploit LCL-reachability's potentials by developing a unified solution for specifying program analysis problems in LCL and implementing novel data structures that support efficient LCL-reachability algorithms. It focuses on (1) theoretical development of the LCL-reachability formulation, (2) efficient algorithms for computing LCL-reachability, and (3) generalizing to practical program analyses. If successful, this project will significantly advance the state-of-the-art in software analysis and verification.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.