Collaborative Research: SHF: Small: A General Framework for Responsive Static Analysis

合作研究：SHF：小型：响应式静态分析的通用框架

• 批准号: 2223825
• 负责人: Bor-Yuh Evan Chang
• 金额: $ 30万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2223825&HistoricalAwards=false
• 关键词: Collaborative; Research; SHF; Small; General

Society increasingly relies on the reliability and security of software. Abstract interpretation is a well-established methodology for proving that software is free of certain classes of bugs. However, for industrial-scale software, standard abstract interpretation techniques may take hours to complete, making them difficult to integrate into modern software development practices. This project develops a framework for responsive static analysis, which retains the power of abstract interpretation while running much more quickly for common use cases. The project's novelties are new algorithms for running abstract interpretation responsively, corresponding mathematical proofs that these algorithms produce the desired, correct results, and working implementations of the algorithms. The project's impacts are greater performance and applicability of powerful abstract interpretation techniques for verifying software correctness, which in turn will yield more reliable and secure software.The project builds on a recently-developed framework for demanded abstract interpretation, a demand-driven and incremental analysis approach based on reifying analysis computations and dependencies in a graph structure. Via generalizations of this approach, this project will extend the framework to handle compositional analysis, essential for efficient analysis of procedure calls, and refinement-based analysis, to enable combining analyses with varying levels of precision and scalability. This generalized framework will facilitate provable guarantees of from-scratch consistency, a crucial property for responsive analysis. The project will also implement the generalized framework and instantiate it with challenging analysis problems, addressing research challenges in making the framework practical.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.

社会越来越依赖软件的可靠性和安全性。 抽象解释是一种完善的方法，用于证明软件没有某些类别的错误。 但是，对于工业规模的软件，标准的抽象解释技术可能需要数小时才能完成，从而使它们难以集成到现代软件开发实践中。 该项目为响应式静态分析开发了一个框架，该框架保留了抽象解释的力量，同时在常见用例中更快地运行。 项目的新颖性是用于响应地运行抽象解释的新算法，这些算法可以产生所需的，正确的结果和算法的工作实现。 该项目的影响是强大的抽象解释技术用于验证软件正确性的更大性能和适用性，这又将产生更可靠和安全的软件。该项目基于最近开发的框架，用于要求的抽象解释，需求驱动和逐步分析方法，一种基于对图结构中的重新分析计算和依赖性的基于需求驱动的分析方法。通过这种方法的概括，该项目将扩展框架以处理组合分析，对于程序调用有效分析以及基于改进的分析至关重要，以使分析与精度和可扩展性的不同水平相结合。这个广义框架将有助于可证明的从施加一致性的保证，这是响应式分析的关键属性。该项目还将实施广泛的框架，并通过具有挑战性的分析问题实例化，解决了使框架实用的研究挑战。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子和更广泛影响的评估评估标准的评估值得支持的。