SHF: CSR: Small: Collaborative Research: Automated Model Synthesis of Library and System Functions for Program-Environment Co-Analysis

SHF：CSR：小型：协作研究：用于程序-环境协同分析的库和系统功能的自动模型合成

• 批准号: 1218358
• 负责人: Feng Qin
• 金额: $ 9万
• 依托单位: Ohio State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-09-01 至 2013-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1218358&HistoricalAwards=false
• 关键词: SHF; CSR; Small; Collaborative; Research

Program analysis provides solid foundations for a broad range of applications, such as detecting security vulnerabilities, localizing program faults, proving program correctness, and optimizing performance. A pervasive and critical challenge in program analysis is to handle library functions and system calls, which provide an essential execution environment for a program and would be ideal to be co-analyzed with the program itself. Despite its importance, achieving program-environment co-analysis in practice is challenging. First, the difficulty to acquire the source code of some environmental functions precludes source code based analysis. Moreover, even if source code is available, the code base is often prohibitively large and complex, making analysis difficult. Existing solutions are to provide program analysis with either manually-constructed models, which do not scale, or imprecise models, which are overly conservative.In this project, the goal is to apply program synthesis technique to construct models for environmental functions from their binary implementation and a set of initial inputs. The models are essentially programs that provide the same functionality of the functions being modeled, yet substantially simplified. Such programs can be included as part of the application, enabling program-environment co-analysis. The proposed technique will lead to an automated solution that will offload the onus of manually crafting models from program analysis developers' shoulders. Moreover, it will demonstrate the feasibility of precise program-environment co-analysis through applications.

程序分析为广泛的应用程序提供了坚实的基础，例如检测安全漏洞，本地化程序故障，证明程序正确性和优化性能。程序分析中的普遍和关键挑战是处理库功能和系统调用，这为程序提供了必不可少的执行环境，并且非常适合与程序本身共同分析。尽管它很重要，但在实践中实现计划环境共同分析是具有挑战性的。首先，获取某些环境功能的源代码的困难排除了基于源代码的分析。此外，即使有源代码可用，代码库通常在大而复杂，使分析变得困难。现有的解决方案是通过手动构造的模型提供程序分析，这些模型不会扩展或不精确的模型，这些模型过于保守。在该项目中，目标是将程序合成技术应用于其二进制实施和一组初始输入的环境功能的模型。这些模型本质上是提供与正在建模的功能相同功能的程序，但基本简化了。这些程序可以作为申请的一部分包括在内，从而实现了环境的共同分析。提出的技术将导致一种自动解决方案，该解决方案将从程序分析开发人员的肩膀上卸载手动制作模型的责任。此外，这将证明通过应用程序进行精确的程序 - 环境共同分析的可行性。