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

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

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.