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

程序分析为广泛的应用提供了坚实的基础，例如检测安全漏洞，定位程序错误，证明程序正确性和优化性能。程序分析中一个普遍而关键的挑战是处理库函数和系统调用，它们为程序提供了一个基本的执行环境，并且非常适合与程序本身进行共同分析。尽管重要，但在实践中实现方案-环境共分析是一项挑战。首先，获取某些环境函数的源代码的困难排除了基于源代码的分析。此外，即使源代码可用，代码库也往往过于庞大和复杂，使得分析变得困难。现有的解决方案是提供程序分析与手工构造的模型，不缩放，或不精确的模型，这是过于conservative.In本项目中，目标是应用程序合成技术，从他们的二进制实现和一组初始输入构建模型的环境功能。模型本质上是提供与被建模的功能相同的功能的程序，但实质上是简化的。这样的程序可以作为应用程序的一部分，从而实现程序-环境协同分析。所提出的技术将导致一个自动化的解决方案，将卸载的负担，手动制作模型从程序分析开发人员的肩膀。此外，它将通过应用程序证明精确的程序环境协同分析的可行性。

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.