Android is the primary software platform for mobile, networked devices such as tablets and smartphones. These devices are increasingly used for safety-critical functions that require verification of correct and robust behavior of applications. Such software written for the Android operating system is hard to test because applications are inherently concurrent, applications are usually being driven by asynchronous user input and network events, the application model is not amenable to unit testing, and the availability of sources for many commercial applications is missing. Safety-critical applications require verification by means of systematic exploration of all possible software behaviors. Conventional testing does not guarantee sufficient coverage, especially for concurrent applications.
The preferred verification method for binary programs with the above characteristics is software model checking, which automatically varies all parameters such as input data and scheduling sequences in order to systematically check the program for absence of errors along all execution paths. The open-source Java Pathfinder (JPF) system is a software model-checking framework developed at NASA Ames that supports execution of Java bytecode, and provides many well defined extension points to adapt to different application models and implement new verification properties by means of runtime-configured plugins without the need to modify JPF itself. JPF is based on Java bytecode and the Java Virtual Machine (JVM) specification. JVMs are stack machines. While Android applications are written in the Java programming language, the Android platform uses its own virtual machine (Dalvik VM), which is a register machine. Dalvik bytecode is very different compared to JVM bytecode, and binary distribution formats differ significantly. Consequently, JPF cannot be used off-the-shelf to verify binary Android applications that are only available as Dalvik bytecode.
PathDroid is an extension of the JPF verification framework that supports checking binary Android applications for the absence of software defects such as unhandled exceptions and deadlocks. PathDroid lets users run such applications on development platforms without the need for hardware-in-the-loop or availability of sources.
Components of PathDroid include Dalvik-specific replacements for JVM constructs such as StackFrames and class loading, and implementation of the Dalvik instruction set (with about 300 bytecode instructions). PathDroid is used as a runtime-configured JPF extension that allows executing binary Android applications through the normal JPF user interfaces. As a regular JPF extension, PathDroid can be used alone from the command line, from within integrated development environments such as Eclipse, and embedded from specialized JPF driver applications.
This work was done by Peter Mehlitz of Ames Research Center. This software is available for use. To request a copy, please visit here.