Verification of Android Applications

This study investigates an alternative approach to analyze Android applications using model checking. We develop an extension to Java Path Finder (JPF) called JPF-Android to verify Android applications outside of the Android platform. JPF is a powerful Java model checker and analysis engine that is very effective at detecting corner-case and hard-to-find errors using its fine-grained analysis capabilities. JPF-Android provides a simplified model of the Android application framework on which an Android application can run and it can generate input events or parse an input script containing sequences of input events to drive the execution of the application. JPF-Android traverses all execution paths of the application by simulating these input events and can detect common property violations such as deadlocks and runtime exceptions in Android applications. It also introduces user defined execution specifications called Checklists to verify the flow of application execution.