JPF-ANDROID

JPF-Android logo

Extending JPF-Android

Executing Android Applications on Java PathFinder

Android applications are designed to run on the Android software stack. Due to this design Android applications's implementation is heavily dependent on the Android application framework and system services.

The Android application framework, the system services and Android applications are implemented in the Java programming language. The Java source code is compiled to Java byte-code and eventually converted into dex byte-code that can be executed on the DVM.

The first step in executing Android applications on the JPF JVM is to acquire the Java byte-code of the application framework, the system services and the application. This is necessary as JPF only executes Java byte code.

The Java byte-code of the application is generated by compiling its source code against the Jar archive shipped with the Android SDK (android.jar). This archive contains compiled class stubs of the Android application framework for all classes visible from Android applications. The compiled application class files are only converted to dex byte-code when the application is packaged into a APK file that can be installed on a device.

Although the Android application classes are compiled using the android.jar archive, they cannot be used to run the application on JPF since these classes are only stubs and do not contain any logic or implementation of the Android framework.

The Android application framework is compiled to Java byte-code and converted to dex byte-code during the creation of a new Android system image. After this process is complete, the Java byte-code of the compiled Android application framework classes can be retrieved. It is important to note that, although it is possible to retrieve the compiled Java byte-code of the Android application framework, these classes cannot directly be executed on the JVM. They are dependent on native methods which, in turn, are dependent on specific hardware drivers and kernel features only available on the Android platform.

For these class files to run on JPF's JVM, a closed system of the Android framework needs to be created by modeling the underlying functionality that is not available. The closed system must run on JPF and must be independent of the underlying architecture of the system. The figure below displays the different levels at which the system can be closed.

The levels at which the Android software stack can be modeled

The highest level at which the system can be closed is at level one. In this case none of the Android application framework or system services classes are included in the model. JPA creates a new model of the Android application framework including only the basic classes that an application requires to run. A driver can then be written to execute the application components life-cycle methods and fire the listeners of View components.

This way of modeling the Android software stack works well for component testing and is used in Robolectric. It is not sufficient for verifying complex interaction between components and concurrent behavior of applications.

At the lowest level, the system can be closed at level three. At this level all the Android framework classes and system services will be executed on the JPF JVM. Only the native method calls of the framework and their interaction with the C libraries and hardware drivers will be modeled.

The Android framework and system services contain a large number of classes and one of the main challenges of JPA is to decide which parts of the system to include in the JPF Android model environment. The more of the Android framework classes included in the environment, the more realistic the environment becomes and the more errors can be found. However, if too many of the framework classes are included, the scheduling possibilities increase exponentially which results in a search space too large to verify.

JPA closes the Android framework at level two. Modeling the framework at this level has the advantage of including the base framework used to execute an Android application, but reduces the state space by creating simple models of the Android system services.

In the Android software stack, the system server managing the system services runs in its own process and each service runs in its own thread. To reduce the state space of the environment and to create a more realistic model of the system, the Android system services are modeled in the \ac{MJI environment provided by \ac{JPF . For the same reasons the entire system service is not modeled but only its necessary components that drive the execution of the application or present an interface to the application framework.

The implementation of the Android system services is complex, extremely large and undocumented. To simplify the model of the Android services and to ensure that the model is realistic, the tool is limited to the verification of a single Android application. This can later be extended to verify multiple Android applications.

A remaining question is whether this model environment will allow accurate detection of errors in Android applications which are developed to be executed on the Android software stack and the DVM. Android applications are developed in Java and can contain the same language related errors as Java applications and these errors will automatically be detected by JPF.

In addition, another advantage of keeping the implementation of the Android application framework and only modeling the interaction between the systems service and the framework is that the application executes in the same way as it would on the Android application framework on the Android platform.

Java PathFinder

JPF is an automated, open source, analysis engine for Java applications~\citep{modelchecking . It is implemented as an explicit state model checker designed to model-check Java applications at byte code level. It includes its own custom JVM implementation which include callbacks to notify subscribed listeners of certain JVM and JPF events. The application is executed on the JPF JVM while being verified against property specifications implemented as JPF listeners.

There are two requirements for applications to run on JPF:

Firstly, the applications need to run on the JVM (since JPF uses a custom Java VM). In other words, they must consist of valid Java code/byte code.

Secondly, the applications require drivers to drive the applications' execution.

By default JPF can detect errors such as deadlocks, race conditions, infinite loops, track object allocations and can inject exceptions into the application.

JPF also includes a MJI that allows Java classes to be modeled at two levels. Firstly, the environment can replace any Java class in the application, its libraries and even classes in the Java class library with a new class with the same name, but which models the functionality of the original class. This class lookup can be configured in the JPF properties file. The MJI also allows native method calls to be intercepted and custom native methods written in Java to be executed to model the functionality of the actual native code .

JPF itself includes several models for classes in the Java class library. Models of entire Java classes run on the JPF JVM and are verified similar to the normal Java application classes. Native method models however, are executed outside of the JPF JVM on the actual JVM which it not verified by the JPF model checking engine.

Programs are model checked under a closed state space including all states that was reached during the program's execution. JPF introduces ChoiceGenerators as a mechanism to reach as many of the program's states as possible. ChoicesGenerators are used to branch transitions in the state-transition graph of the Java application. A path in the state space is branched due to multiple non-deterministic choices (transitions) being available. JPF, for example, makes use of ChoiceGenerators internally to store and \mbox{schedule different thread interleavings. ChoiceGenerators can also be used to non-deterministically schedule different data input choices. When a non-\linebreak deterministic choice is reached during a transition, a ChoiceGenerator is pushed on a stack kept by the JPF model checking engine. As soon as this happens, JPF breaks the current transition, creates and stores a new system state object and then traverses each of the choices of the ChoiceGenerator non-deterministically.

Modeling the Android Environment

JPA closes the Android system just below the Android application framework. Closing the system at this level is complex since the Android application framework itself is very large and has many depedencies on the system server classes. The Android application framework also contains code that does not influence the verification of an Android application. This includes process management, inter process communication, UI drawing and resource parsing code. This code bloats the JPA model environment and increases the search space during verification. For this reason JPA's environment contains models for some of the framework classes to simplify their implementation.

Furthermore, JPA must model all IO from and to the applications. This includes file management, network IO, database storage and communication with other applications.

In this section the different parts of the Android application framework that have to be modeled to close the system is described. The two main parts of the system that needs to modeled are the interaction and functionality of the system services and the native application framework functionality.

JPA aims to keep the functionality of the Android application framework similar to its original implementation. This is done to ensure that its behavior is consistent with the original framework. But, due to the many references and dependencies on the system services and currently unsupported functionality of the application framework, JPA is required to provide temporary model classes for several application framework classes. These models remove the currently unsupported features rather than stubbing many other classes to support this functionality.

Android System Services

The Android system services are part of the Android system server, the main application of the Android software stack. The system server, like all other Android applications, runs in its own process. For Android applications to communicate with system services they need to make use of the Binder IPC service. Each of the system services provides an AIDL interface allowing multiple clients (application components) to invoke RPC methods on the service concurrently. When a client calls a RPC method, it waits until the method returns before continuing to execute. In other words RPC methods are called synchronously in Android. Each process is assigned a thread pool of Binder threads in the native Binder driver to process the concurrent requests from the clients. As the code of the services can be executed concurrently, code changing the state of the service is put into synchronized blocks to avoid data races.

JPA is designed to verify only a single Android application in a single process. As a result of this restriction, the Android system services was first designed to be implemented in the JPF MJI environment. This allowed the services to be executed outside of the application process, in the native environment where their execution will not influence the verification of the application.

One of the problems with this design is that the MJI environment is not automatically backtracked together with the application state. \ac{JPF does allow objects in the MJI environment to attach an object representing the state of the service to the \ac{JPF system state. This state is then stored and restored as necessary. This process becomes tedious and memory intensive as the new state is not stored as efficient as the JPF state and has to be deep cloned for each new system state to ensure that the all states are independent of each other.

JPA overcomes this problem by storing the state of each service in the manager class of the service which is part of the application framework. Examples of these manager classes include the WindowManager, ActivityManager, InputManager and PackageManager. The manager classes originally masked the complex Binder IPC between the application and the system services. Now, instead of performing IPC to remotely invoke method calls, they store the state of the service and provide methods to interact with the state directly. The system state is now backtracked as part of the application state.

The logic of the system services is now running in the application process where it was previously run in system process. This increases the size of the application's state and the amount of non-determinism in the application process.

JPA reduces the complexity and scheduling possibilities of the application by not creating a new Binder thread to process each RPC method call from the application. As these method calls are made synchronously, it instead executes the methods directly as the system service methods are now also run in the application process.

Several of the services also include a messenger thread to synchronously process outgoing requests from the system service to the application. These requests include the delivery of Broadcast Intents and updates to the state of the application.

In JPA the system service makes outgoing requests directly. It does not schedule them in a messenger thread to be processed synchronously. Since JPA only verifies a single Android application, most of the time, only a single thread will be interacting with a system service (the main thread of the application). But, since Android does support multi-threading and to ensure that JPA does not have data races, JPA defines all methods that changes the state of the service and send outgoing requests as synchronized.

JPA's model of the system services has the advantage of reducing scheduling possibilities by reducing the number of concurrent threads. The disadvantage of this design is that JPA may miss errors related to strange scheduling of messages in the system services. There is also no way to verify that the system executes exactly as it is executes in Android. Lastly JPA system services must clone all objects sent to the service and returned from the service to ensure that the service/application does not change the objects since these objects are usually sent between processes.

The ServiceManager class is part of the Android application framework and is used to retrieve Binder connections to the system services. JPA has created a model of the ServiceManager class. Instead of using this class to retrieve these connections, JPA uses this class to startup and store references to the system services. The application components can retrieve the service managers by requesting them by name from the Context . The ContextImpl implementation of the Context subsequently request the manager of the service from the ServiceManager class. The Context class acts as the link between the component and the system services. It is responsible for retrieving references to the Android system service managers. For this reason, the Context object's model is an important part of the application framework model.

JPA creates a model for the Context class to control how the application retrieves system service managers.

Managing the Application components

Android applications consist of four base component types. These components are represented by the Activity , Service , BroadcastReceiver and ContentProvider classes. These classes are overwritten by application developers to create many component implementations.

It is important to retain the public interface as well as the inner workings of each of these components as they are exposed to application developers. JPA models the functionality of these components with great care. The Activity model, for example, contains the same public methods as the original class and follows the same life-cycle. By creating a model of the class, the functionality that is currently not supported by the model environment can be removed. All the unsupported classes could have been modeled, but several class stubs would have had to be created since the Activity class is so large and dependent on several other classes.

The main components of an Android application are created and their life-cycle controlled by the ActivityThread class. The ActivityThread manages the states of the application. It stores the resources and the configuration of the application. It also contains the main entry point of the application and starts the main thread of the application responsible for handling all application events.

The ActivityThread class contains a handler, ApplicationThread , which can schedule messages on the message queue of the main thread of the application. These messages include changes in the state of the application, for example, an Activity starting, a Service stopping or an Intent broadcast to the application. These messages are processed by the main thread of the application by calling the ApplicationThread handler to handle them. The ActivityThread responds to these messages by guiding the relevant component through the correct life-cycle stages for the specific event.

All application components of all applications are managed by the \linebreak ActivityManagerService . When an application is started, the \linebreak ActivityManagerService is passed a Binder connection to the \linebreak ApplicationThread handler of the application. The \linebreak ActivityManagerService makes use of this handler to schedule messages on the application's message queue. The ApplicationThread provides methods to schedule application messages on the message queue of the application to be processed by its main thread.

JPA creates a model class for the ActivityThread to remove some of its unused functionality, but the core implementation of the class remains the same. The model class provides the same interface to the ActivityManagerService and processes the requests and manages the state of its components using the same methods as the original class.

The ActivityThread is controlled by the Activity\+Manager\+Service . The main challenge of managing the application components is to model the ActivityManagerService . Each Android application component has different requirements when it comes to the ActivityManagerService . These requirements are discussed in more detail below.

Activity

The Activity component requires the ActivityManagerService to keep track of the order in which Activities were started. Additionally the ActivtyManager needs to keep track of the Tasks within the stack of Activities. JPA stores only one stack of Activities and currently only supports one Task. In other words, in JPA the Activity stack stores the Activities within a single task.

When an Activity is started by another Activity, a new ActivityRecord is pushed on the stack. The ActivityRecord stores information related to the Activity. This includes the Intent that started the Activity and whether the Activity expects a result from the next Activity. It also tracks the state of the Activity. When an Activity is destroyed, the ActivityRecord is popped from the Activity stack. The Activity stack can contain multiple instances of the same Activity type. Each time an Activity starts another Activity, a new instance is created in JPA.

When an Activity is destroyed, the ActivityManager resumes and delivers the result to the previous Activity on the stack.

Service

The JPA ActivityManager stores a list of all started services. This list is used to determine if a service must be started or if the service is already running in which case only an Intent is delivered to the service. There can only exist one instance of a started service at a time. Therefore, when the startService() method is called, the service must not be started again.

When a component binds to a Service, it passes the ActivityManager a ServiceConnection object. The ServiceConnection object is used by the ActivityManager to return the service connection to the component since binding to a service is an asynchronous request. JPA's ActivityManager stores a mapping of ServiceConnection objects to bounded services. If the service is unexpectedly terminated, the onServiceDisconnected() method of all the ServiceConnection objects mapped to this service is called to notify the client that the connection is lost. When a component unbinds from a service, the ServiceConnection mapping is removed from the ActivityManager. If all service connection mappings have been removed, the ActivityManager destroys the service.

AIDL services are used in two location in Android applications. Firstly for communication between the system and the applications and for communication between an application component and a service of a different application. The communication between the application and system is simple to model since these classes are not directly exposed to the developer.

In the case of an external service it is harder to control the communication. Applications containing AIDL services are pre-processed with the aidl tool in the Android SDK. This tool generates the correct interfaces required for an Android application to compile on the normal Java compiler. The IPC of AIDL services is usually handled by the Binder driver in the Android kernel. GINA~\footnote{Available at: \url{https://gitorious.org/jpf-android-services , a fork of the aidl tool, can be used to generate alternative interfaces that allow applications to directly call the methods on the AIDL service instead of using \ac{IPC .

Broadcast Receivers

The JPA ActivityManager stores a list of all Broadcast Receivers that are dynamically registered from within the application code. When an Intent is sent to the ActivityManager to be broadcast to system, the ActivityManager Service resolves the Intent to all registered BroadcastReceivers. It also makes use of the PackageManager to resolve the Intent to all BroadcastReceivers that are statically registered in the Android Manifest file.

Once the Broadcast has been resolved to the relevant BroadcastReceivers, the ActivityManager schedules the delivery of the Intent to the components on the main thread of the application.

In the case of an ordered broadcast, the Intent is delivered sequentially to each of the BroadcastReceiers according to their priory.

When a sticky Intent is broadcast, the ActivityManager keeps a reference to the Intent. When a BroadcasyReceiver is registered from the application code, the ActivityManager checks if one of the sticky Intents matches the BroadcastReceiver. The first matching sticky Intent is return to the component.

Modeling the Graphical User Interface

Many of the Android testing tools focus on verifying the \ac{GUI of the application. One way to verify the \ac{GUI is to take screen shots of the application at certain states of its execution and compare these screen shots with test oracles~\citep{MonkeyRunner . This technique is easily influenced by changes in the resolution and orientation of the screen. Other tools internally inspect the view hierarchy of the Windows using test cases.~\citep{AJUnit,robotium,robolectric .

JPA does not focus on testing the actual rendering of the \ac{GUI , it focuses on detecting errors in the logic of the application which results in unexpected and unwanted behavior of the system. Instead of trying to create an exact model of the windowing system to accurately calculate the coordinates and sizes of all the View objects, JPA models the state of each View object.

JPA View objects continue to store the id of the element, its state (enabled / visible / focused), and its listeners, but returns default values for attributes such as its coordinates, size, background and theme. JPA stores the state of a View to avoid triggering script actions on disabled or invisible objects. Custom View objects such as CheckBoxes, TextBoxes and ListBoxes each models their own unique attributes and listeners. The CheckBox, for example, has an additional checked attribute and an OnCheckedChangeListener . The ListBox has an adapter to store the list of values to display. The TextBox stores a String value representing the text inside of the box. As Android contains many View components, each with many attributes, these models are continually upgraded and extended. The View hierarchy is kept in tact to support cascading attributes such as visibility.

JPA stores the View hierarchy in the Window of an Activity. When the Activity is made visible, it sets this Window as the current visible Window in the WindowManager.

Network Connections

JPA models network connections by modeling the java.net.URL class. When a connection is opened to this URL, the java.net.URL class returns an InputStream object containing the data stored in a file, instead of actually streaming the data over the network.

JPA allows the user to internally associate an URL with a filename by sending a system event from the input script. Listing shows an example where the URL http://www.sun.ac.za/index.html is associated with the file src/index.html in the project directory.\\

Creating and sending a @urlInputStreamIntent from the script

@urlInputStreamIntent.setAction("android.net.conn.URL_INPUT_STREAM");
@urlInputStreamIntent.putString("url","http://www.sun.ac.za/index.html")
@urlInputStreamIntent.putString("file","src/index.html")

sendBroadcast(@urlInputStreamIntent)

In this code, the @urlInputStreamIntent object is created and its Action is set to android.net.conn.URL_INPUT_STREAM . This Action is used by the system to identify the purpose of the Intent. Two extra properties are set on the Intent that maps the URL to the name of the file containing the data. Lastly, the sendBroadcast() system event is then used to send this Intent to the ActivityManager to be processed.

The ActivityManager processes the @urlInputStreamIntent and forwards it to the native URL class, JPF_java_net_URL . This class stores a map containing all the URL to filename mappings.

When a connection is opened to this URL, JPA reads its input from the input file associated with this URL. The Java code to retrieve data over the network is given in Listing \ref{fig:urlcreate .

Example of opening a connection to an URL

 try {
        URL url = new URL("http://www.sun.ac.za/index.html");
        InputStream is = url.openStream();
        InputStreamReader reader = new InputStreamReader(is);
        char[] contents = new char[15];
        int num = reader.read(contents);
        
        String s =  new String(contents);
        System.out.println(s);
        
  } catch (MalformedURLException e) {
    System.out.println(e.toString());

  }  catch (IOException e) {
    System.out.println(e.toString());
  }

When a new URL object is constructed in Java, it is passed a web address. This address is verified in the constructor of URL class to ensure it is a valid URL. JPA intercepts the constructor of the modeled URL class and natively creates a Java java.net.URL object to ensure that the address passed to the modeled URL object is valid. The code of the native constructor is given in Listing \ref{fig:urlconst . If the URL is not valid, the constructor throws a MalformedURLException in JPF's model environment on line 7.\\

A Malformed URL Exception is thrown if the URL is invalid

@MJI
public void $init__Ljava_lang_String_2(MJIEnv env, int objref, int urlRef) {
  try {
    urlString = env.getStringObject(urlRef);
    URL url = new URL(urlString);
  } catch (MalformedURLException e) {
      env.throwException("java.net.MalformedURLException", e.getMessage());
  }
}

JPA also makes use of the \ac{JPF Verify API to non-deterministically schedule both the case where the network connection could be opened successful and where the connection crashed and an IOException is thrown. The code of the openStream() method is given in Listing \ref{fig:urlconst2 . On line 1 the Verify.getBoolean() method will non-deterministically be scheduled as both true and false simulating both these cases.

Code that non-deterministically throws an IO Exception 

public InputStream openStream() throws IOException {
    boolean error = Verify.getBoolean();

    if (error) {
      throw new IOException("Could not open Url");
    } else {
      return new ByteArrayInputStream(getURLInput());
    }
}

Database Modeling

Model Checking an application with a database is not a simple task. Unfortunately, databases are commonly used in Android applications therefore there is a need to create a simple model.

At the highest level, the database methods can be mocked to return default values. Although this will allow the application to continue running, many of the methods processing data from the database will never be executed.

JPF-Android creates a model of a database at a slightly lower level. It parses the SQL from the application using the JSQL Parser\footnote{Available at: http://jsqlparser.sourceforge.net . It then stores a list of column names and a list of values for each table in a map.

The advantage of modeling the database is this way is that its state (the data it contains) is backtracked together with the application state. The disadvantage of this approach is that the database's entries are all kept in memory, in other words this approach will not scale well for large data sets.

Parsing XML

All code that is executed on the JPF JVM, is model-checked. To avoid unnecessary model-checking of the entire SAX parser, the SAX Parser is implemented as a thin client with native method callbacks run in the MJI on the JVM. The native parser parses the input file using a Document Object Model (DOM) Parser and stores a map of its nodes. As the SAX parser traverses the file it actually traverses the DOM model of the document in the native peer of the SAX parser.