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

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

• 批准号: 1218993
• 负责人: Xiangyu Zhang
• 金额: $ 4.48万
• 依托单位: Purdue University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-09-01 至 2013-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1218993&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.

程序分析为广泛的应用提供了坚实的基础，例如检测安全漏洞、定位程序故障、证明程序正确性和优化性能。程序分析中普遍存在的关键挑战是处理库函数和系统调用，它们为程序提供了必要的执行环境，并且非常适合与程序本身进行联合分析。尽管它很重要，但在实践中实现程序-环境协同分析仍然具有挑战性。首先，某些环境函数的源代码获取困难，阻碍了基于源代码的分析。此外，即使源代码可用，代码库也往往过于庞大和复杂，使得分析变得困难。现有的解决方案是通过手动构建的模型（无法扩展）或不精确的模型（过于保守）提供程序分析。在该项目中，目标是应用程序综合技术从其二进制实现构建环境函数的模型和一组初始输入。这些模型本质上是提供与正在建模的功能相同的功能的程序，但大大简化了。此类程序可以作为应用程序的一部分包含在内，从而实现程序-环境协同分析。所提出的技术将带来一种自动化解决方案，从而减轻程序分析开发人员手动构建模型的负担。此外，它将通过应用展示精确的程序-环境协同分析的可行性。