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

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

• 批准号: 1816812
• 负责人: Qirun Zhang
• 金额: $ 50万
• 依托单位: University of California-Davis
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-10-01 至 2019-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1816812&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的法定任务，并且使用基金会的知识分子优点和更广泛的影响评估标准，被认为值得通过评估来获得支持。