PhD Proposal: Synthesis-Aided Symbolic Execution for Event-Driven Frameworks

Symbolic execution is a popular and effective technique to discover software bugs and vulnerabilities. However, it is very challenging to symbolically execute apps written using event-driven frameworks, for two reasons. First, such apps are tightly tied to the framework, yet the framework code is too large and complex to symbolically execute. Second, since apps have complex control flow and are interactive, it is difficult to both formulate properties to check and to ensure checking explores sufficiently many paths.
We propose to use program synthesis to semi-automatically generate two artifacts that can make symbolic execution more effective and efficient in this context. First, we propose synthesizing a model of the framework, which abstracts away unimportant details and is simpler and more amenable to symbolic execution. Second, we propose synthesizing drivers that provide end-users with easy-to-understand code that drives symbolic execution to analyze desired properties. To attack both problems, we will use a multi-modal synthesis that incorporates both behavioral and structural constraints. Behavioral constraints come from call-return sequences and environment changes from actual program executions, and structural constraints come from high-level knowledge---typically involving design patterns---of the framework API. We propose to demonstrate the effectiveness of our approach by synthesizing a model of Android; synthesizing drivers that cause Android apps to access to privacy-sensitive user data; and checking privacy policies via a symbolic executor for Android, together with two aforementioned artifacts.
Examining Committee:
Committee Chair: - Dr. Jeffrey S. Foster
Dept. Rep: - Dr. Hal Daume III
Committee Members: - - Dr. Michael Hicks
- Dr. Armando Solar-Lezama