Dragonfly: Encapsulating Android for Instrumentation
University of Málaga
Ana Rosario Espada
María del Mar Gallardo
Damián Adalid

Index
Introduction
Android Overview
Formalization
Dragonfly Design
Static Monitor
Dynamic Monitor
Conclusions
2
INTRODUCTION
A Runtime Verification Framework for ANDROID Applications
3

Introduction
More than 6 million of
different applications
Different kinds of applications in the market
4

Verification Techniques
Runtime Verification
RV is based on the observation of the traces generated by the execution of a system to detect errors of its behavior.
RV types
Synchronous Asynchronous
Internal External
Offline Online
5
Android Overview
A Runtime Verification Framework for ANDROID Applications
6

Android Architecture
Application
Built-in(phone, contacts, browser), Third-party/Custom
Application Framework
Telephone Manager, Location Manager, Notification Manager, Content providers, Windowing, Resource Manager, etc.
Libraries
Graphics, media, database, WebKit, etc.
Android Runtime
Dalvik Virtual Machine
Linux Kernel
Power, File system, drivers, process, management, etc.
7

Android System
8

Android System
Each application may be composed of different components:
Activity: an independent visual screen for the user
Service: particular task embedded inside a specific application
Content provider: allows to provide data from one application
to another
Broadcast receiver: manages the messages sent by the system or the applications
9
Formalizing Android
A Runtime Verification Framework for ANDROID Applications
10

Formalizing Android
We consider that applications may be in one of the following states:
Inactive: the main thread does not yet exist.
Active: the main thread of the application has been
initialized and some service or activity is active.
Paused: the application is initialized but none of its components is active.
11

Formalizing Android
The configuration of an Android application is given by a tuple:
ID: the application identifier.
State: active, inactive or paused.
Event queue: each of which may be directed to one or several components of a system application.
Components: a list of activities, services, content providers or broadcast receivers.
12

Formalizing Android
Android is basically an event-driven OS. The whole system,
its applications and its components evolve through events.
We formalize those events as transition rules, referred to the
whole system, an application or a component.
Each element extracted from the event queue of an application may release concrete events for any component of the applications.
13

Formalizing Android
Once the event has arrived at the event queue, it is distributed
to the corresponding components.
14
Dragonfly DESIGN
A Runtime Verification Framework for ANDROID Applications
15

Functionality
Events
Monitor throwing events
And listening the traces
Verification with observers
16

Dragonfly Architecture
Monitor
INSTRUMENTATION
Threads
Allocated Objects
Profiling data
…
Application Manager
Android Monitor Engine
Observer
Event Generators
Source
Android Model
Error Reports
17

Application Manager
Generates random events using Monkey
Source
Application Manager
Event Generators
$ adb shell monkey -p your.package.name -v 500
18

Monitor Engine
…
Source
Android Monitor Engine

Tools to extract information
DDMlib -> adb
JDI
DDMlib allow us to start Android Debug Bridge and get useful information from the sources.
JDI (Java Debug Interface) is needed to detect method entry event and other specific events.
19

Instrumentation and observers
Error Reports
Observer
Aspect Oriented Paradigm
Instrumentation : Spring AOP
DSL: Lambdaj + AspectJ
20
Example
A Runtime Verification Framework for ANDROID Applications
21

Activity Life Cycle
22

Activity Life Cycle
23
Static Monitor
A Runtime Verification Framework for ANDROID Applications
24

Static Monitor
Static data are properties or values from the:

Smart-phone: battery status, serial number…

I/O’s: GPS status, camera status, signal strength…

Applications: identifiers, names, main threads…

Components: types, set of states…
25

Static Monitor
Source
DDMlib
ANDROID MODEL
Static info
Build
26
Dynamic Monitor
A Runtime Verification Framework for ANDROID Applications
27

Dynamic Monitor
Dynamic data correspond to the sequence of
events fired by the system or by the user. We
define three types of events:
Actions related to the state of components
Method calls
Exceptions
LISTENERS
28

Dynamic Monitor

Source
Monitor
Application Manager
Android Monitor Engine
Android Model
USB or Wireless
Stimulation events
Return events
29
ConcluSIons & FUTURE WORK
A Runtime Verification Framework for ANDROID Applications
30

Conclusions
We have developed a tool capable of:

Verifying Android Applications on runtime

Extending the verification to other platforms

Saving a lot of verification properties

Writing the properties in a semantic language

31

Future Work
Improve the DRAGONFLY’s capabilities combining DDMlib with other tools


Improve DRAGONFLY’s efficency trying other types of instrumentations and DSL’s
32
Thanks!!
Questions?