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

SHF:Small：通过线性联合语言可达性进行可扩展且精确的程序分析

• 批准号: 1917924
• 负责人: Qirun Zhang
• 金额: $ 48.19万
• 依托单位: Georgia Tech Research Corporation
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-12-01 至 2023-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1917924&HistoricalAwards=false
• 关键词: SHF; Small; Scalable; Precise; Program

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.

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

项目成果

Program debloating via stochastic optimization

通过随机优化进行程序膨胀

• DOI: 10.1145/3377816.3381739
• 发表时间: 2020
• 期刊: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: New Ideas and Emerging Results
• 作者: Xin, Qi;Kim, Myeongsoo;Zhang, Qirun;Orso, Alessandro
• 通讯作者: Orso, Alessandro

Studying and Understanding the Tradeoffs Between Generality and Reduction in Software Debloating

• DOI: 10.1145/3551349.3556970
• 发表时间: 2022-10
• 期刊: Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering
• 作者: Qi Xin;Qirun Zhang;A. Orso

On the complexity of bidirected interleaved Dyck-reachability

双向交错Dyck可达性的复杂性

• DOI: 10.1145/3434340
• 发表时间: 2021
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Li, Yuanbo;Zhang, Qirun;Reps, Thomas
• 通讯作者: Reps, Thomas

Efficient algorithms for dynamic bidirected Dyck-reachability

• DOI: 10.1145/3498724
• 发表时间: 2022-01
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Yuanbo Li;K. Satya;Qirun Zhang

Witnessability of Undecidable Problems

不可判定问题的可见证性

• DOI: 10.1145/3571227
• 发表时间: 2023
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Ding, Shuo;Zhang, Qirun
• 通讯作者: Zhang, Qirun