The rapid advance of program analysis greatly benefits many applications, including security vulnerability detection, software fault localization, performance optimization, to name a few. However, handling library functions and system calls (also referred to as environmental functions) presents a pervasive and critical challenge in program analysis. Even though these environmental functions are not written by developers, they are an intrinsic part of program semantics and consequently it would be ideal for a program analysis to co-analyze the program and its execution environment. 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.
In this project, the goal is to develop a highly automated technique that can construct models for environmental functions from their binary implementations 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 a highly automated solution that will largely offload the onus of manually crafting models from program analysis developers' shoulders. Moreover, it will make program environment co-analysis feasible and more precise, enabling detection of security vulnerability and software defects that are otherwise undetectable. Additionally, the PIs expect the proposed research to foster learnings in both program analysis and operating systems, as well as providing many opportunities to incorporate findings to relevant courses in computer science.
