Researchers 

• Yepang Liu
• Chang Xu
• S.C. Cheung

This webpage decribes how we implemented GreenDroid as an extension on top of Java PathFinder (JPF). JPF is a general purpose model checking for Java programs. It can systematically execute a Java program in its own virtual machine and perform fault detection. Since Android applications are written in Java, it is possible to use JPF to analyze them. However, there are three technical issues that need to addressed because Android applications are (1) event driven, and (2) rely on a proprietary set of libraries which is unavailable outside emulators and real devices. These technical issues are:

1. User interaction simulation: we need to simulate user actions to drive the execution of an Android application.
   
2. Event handler scheduling: we need to schedule event handlers correctly to handle the generated user actions. There is no explicit control flows or calling relationships between these handlers.
3. API modeling: we need to properly model Android APIs (those interfaces exposed by library classes). Simply ignoring the side effect of these APIs may lead to huge imprecision in an application's analysis.
   

To address the first issue, we propose to analyze the GUI layout configuration files of an Android application before analysis, and exhaustively generate all possible user interaction event sequences at runtime. The detailed discussion of the algorithm can be find in our paper [X]. To address the second issue, we propose to extract the handler scheduling policies from Android documentations and organize these policies as a collection or temporal rules (named application exeuction model) that specify the calling relationships between event handlers. These rules can be translated to code either manually or automatically (with a specially designed parser if the rules are specified in a certain type of domain specific language). To address the third issue, we took a pragmatic approach by modeling a critical set of Android APIs for experimental purposes. We are modeling more and more Android APIs as GreenDroid evolves. The remaining of this webpage lists our temporal rules and modeled Android APIs (the API list will get longer as we model more and more APIs).

1. Android application execution model

The application execution model is a collection of temporal rules of the following form:
[f1], [f2]

2. Modeled Android APIs

The following are some examples of Android APIs that have been modeled in GreenDroid. The list will keep expanding and can be found here.

Activity related APIs (public class android.app.Activity)
-- public void startActivity(Intent intent)
-- public void startActivityForResult(Intent intent, int requestCode)
-- public void finish()
-- public void finishActivity(int requestCode)
-- public final void setResult(int resultCode)
-- public final void setResult(int resultCode, Intent data)
-- public void setContentView(int layoutResID)
-- public View findViewById(int id)
-- public Object getSystemService(String name)

Service related APIs (public class android.app.Service)
-- public ComponentName startService(Intent intent)
-- public boolean bindService(Intent intent, ServiceConnection conn, int flags)
-- public abstract IBinder onBind(Intent intent)
-- public final void stopSelf()
-- public final void stopSelf(int startId)
-- public final void stopSelfResult(int startId)
-- public boolean stopService(Intent name)
-- public void unbindService(ServiceConnection conn)

BroadcastReceiver related APIs (base class: public abstract class android.content.Context)
-- public Intent registerReceiver(BroadcastReceiver rcv, IntentFilter filter)
-- public Intent registerReceiver(BroadcastReceiver rcv, IntentFilter filter, String permission, Handler scheduler)
-- public void unRegisterReceiver(BroadcastReceiver rcv)
-- public void sendBroadcast(Intent msg)
-- public void sendBroadcast(Intent msg, String permission)
-- public void sendOrderedBroadcast(Intent msg, String permission)
-- pubilic void sendOrderedBroadcast(Intent intent, String receiverPermission, BroadcastReceiver resultReceiver, Handler scheduler, int initial code, String initialData, Bundle initialExtras)
-- public void sendStickyBroadcast(Intent intent)
-- public void sendStickyBroadcast(Intent intent, String receiverPermission, BroadcastReceiver resultReceiver, Handler scheduler, int initial code, String initialData, Bundle initialExtras)

GUI widgets related APIs (base class: public class android.view.View)
-- public void setOnClickListener(View.onClickListener listener)
-- public void setOnLongClickListener(View.onLongClickListener listener)
-- public void setOnTouchListener(View.onTouchListener listener)
-- public void setOnCreateContextMenuListener(View.OnCreateContextMenuListener l)
-- public void setOnDragListener(View.OnDragListener l)
-- public void setOnHoverListenert(View.OnHoverListener l)
-- public void setOnTouchListener(View.OnTouchListener l)
-- public void setOnKeyListener(View.OnKeyListener l)

Location sensing related APIs (class: public class android.location.LocationManager)
-- public void requestLocationUpdate(String provider, long minTime, float minDistance, LocationListener listener)
-- public void removeUpdates(LocationListener listener)
-- public boolean enableMyLocation() (Google maps API in MyLocationOverlay class)
-- public void disableMyLocation() (Google maps API in MyLocationOverlay class)
-- public List<String> getProviders(boolean enabledOnly)
-- public List<String> getProviders(Criteria criteria, boolean enabledOnly)
-- public LocationProvider getProvider(String name)
-- public List<String> getAllProviders()
-- public String getBestProvider(Criteria criteria, boolean enabledOnly)
-- public boolean isProviderEnabled(String providerName)
-- public Location getLastKnownLocation(String provider)

Wake lock related APIs (class: public class android.os.PowerManager and WakeLock)
-- public WakeLock newWakeLock(int levalAndFlags, String tag)
-- public void acquire()
-- public void release()
-- public void setKeepScreenOn(boolean keepScreenOn)

Asynchronous task and timer task related APIs (class: public class android.os.AsyncTask, java.util.TimerTask)
-- public final AsyncTask<Params, Progress, Result> execute (Params... params)
-- public void schedule(TimerTask task, long period)
-- public void schedule(TimerTask task, long delay, long period)
-- public void schedule(TimerTask task, Date when)
-- public void schedule(TimerTask task, long delay)

CSE Department | HKUST | Template design by E-CRM | Page Last Update on Oct. 14, 2013