FRAMEWORK SYNTHESIS FOR SYMBOLIC EXECUTION OF EVENT-DRIVEN FRAMEWORKS

Simple item page
dc.contributor.advisorFoster, Jeffrey Sen_US
dc.contributor.authorJeon, Jinseongen_US
dc.contributor.departmentComputer Scienceen_US
dc.contributor.publisherDigital Repository at the University of Marylanden_US
dc.contributor.publisherUniversity of Maryland (College Park, Md.)en_US
dc.date.accessioned2016-06-22T05:45:57Z
dc.date.available2016-06-22T05:45:57Z
dc.date.issued2016en_US
dc.description.abstractSymbolic execution is a powerful program analysis technique, but it is very challenging to apply to programs built using event-driven frameworks, such as Android. The main reason is that the framework code itself is too complex to symbolically execute. The standard solution is to manually create a framework model that is simpler and more amenable to symbolic execution. However, developing and maintaining such a model by hand is difficult and error-prone. We claim that we can leverage program synthesis to introduce a high-degree of automation to the process of framework modeling. To support this thesis, we present three pieces of work. First, we introduced SymDroid, a symbolic executor for Android. While Android apps are written in Java, they are compiled to Dalvik bytecode format. Instead of analyzing an app’s Java source, which may not be available, or decompiling from Dalvik back to Java, which requires significant engineering effort and introduces yet another source of potential bugs in an analysis, SymDroid works directly on Dalvik bytecode. Second, we introduced Pasket, a new system that takes a first step toward automatically generating Java framework models to support symbolic execution. Pasket takes as input the framework API and tutorial programs that exercise the framework. From these artifacts and Pasket's internal knowledge of design patterns, Pasket synthesizes an executable framework model by instantiating design patterns, such that the behavior of a synthesized model on the tutorial programs matches that of the original framework. Lastly, in order to scale program synthesis to framework models, we devised adaptive concretization, a novel program synthesis algorithm that combines the best of the two major synthesis strategies: symbolic search, i.e., using SAT or SMT solvers, and explicit search, e.g., stochastic enumeration of possible solutions. Adaptive concretization parallelizes multiple sub-synthesis problems by partially concretizing highly influential unknowns in the original synthesis problem. Thanks to adaptive concretization, Pasket can generate a large-scale model, e.g., thousands lines of code. In addition, we have used an Android model synthesized by Pasket and found that the model is sufficient to allow SymDroid to execute a range of apps.en_US
dc.identifierhttps://doi.org/10.13016/M25X9X
dc.identifier.urihttp://hdl.handle.net/1903/18205
dc.language.isoenen_US
dc.subject.pqcontrolledComputer scienceen_US
dc.subject.pquncontrolledAndroiden_US
dc.subject.pquncontrolledEvent-driven Frameworken_US
dc.subject.pquncontrolledFramework Modelen_US
dc.subject.pquncontrolledProgram Synthesisen_US
dc.subject.pquncontrolledSymbolic Executionen_US
dc.titleFRAMEWORK SYNTHESIS FOR SYMBOLIC EXECUTION OF EVENT-DRIVEN FRAMEWORKSen_US
dc.typeDissertationen_US

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Jeon_umd_0117E_16937.pdf
Size:
1.06 MB
Format:
Adobe Portable Document Format
Download

Collections

UMD Theses and Dissertations
Computer Science Theses and Dissertations