Contextual Policy Enforcement in Android Applications with Permission Event Graphs
Kevin Chen, Noah Johnson, Vijay D’Silva, Shuaifu Dai, Kyle MacNamara, Tom Magrino, Edward Wu, Martin Rinard*, and Dawn Song
University of California, Berkeley
*Massachusetts Institute of Technology
Android
Figure: Google Play App Market Growth
Android Malware
-Trend Micro Annual Threat Report
Figure: Google Play App Market Growth
Android Malware Detection
...
...
...
...
...
...
...
APP
Permission
Pkg
Author
Our approach
Undetected Malware Example
User Intended Policy
"The recording can only be started by clicking the REC button, and it will be stopped when the user clicks the STOP button."
Intuition
A representation that summarizes the event dependencies and their API/permission level behaviors (The Permission Event Graph), and a policy language based on that.
Permission Event Graph (PEG)
0
1
2
initialization
sub-graph
finalization
sub-graph
REC.onClick
Start-Recording
STOP.onClick
Stop-Recording
onCreate
onResume
startService
"The recording can only be started by clicking the REC button, and it will be stopped when the user clicks the STOP button."
PEG: States
0
1
2
initialization
sub-graph
finalization
sub-graph
PEG: States
0
1
2
initialization
sub-graph
finalization
sub-graph
State s: {true, false} ^ ModeVar
Predicate abstraction of event states.
e.g.
PEG: Transitions
0
1
2
initialization
sub-graph
finalization
sub-graph
REC.onClick
STOP.onClick
onCreate
onResume
PEG: Labels
0
1
2
initialization
sub-graph
finalization
sub-graph
REC.onClick
Start-Recording
STOP.onClick
Stop-Recording
onCreate
onResume
startService
Sound Recorder: The Good Part
0
1
2
initialization
sub-graph
finalization
sub-graph
REC.onClick
Start-Recording
STOP.onClick
Stop-Recording
onCreate
onResume
startService
The Complete PEG
0
6
5
4
1
2
3
initialization
Recorder Activity
finalization
finalization
Recorder Service
REC.onClick
Start-Recording
STOP.onClick
Stop-Recording
onCreate
onStart
onCreate
Timer.run
Stop-Recording
Timer.run
Start-Recording
onResume
startService
PEG: Context of the Benign Use
0
6
5
4
1
2
3
initialization
Recorder Activity
finalization
finalization
Recorder Service
REC.onClick
Start-Recording
PEG: Context of the Malicious Use
0
6
5
4
1
2
3
initialization
Recorder Activity
finalization
finalization
Recorder Service
Timer.run
Start-Recording
onResume
startService
Formal Specification
"The recording can only be started by clicking the REC button, and it will be stopped when the user clicks the STOP button."
0
1
2
...
...
Approach Overview
Abstraction
Phase
Verification
Phase
Apps
Permission Event Graph
Conformance or counter- examples
Policies
Case Study: Geotag
"Mark location of your photos"
Case Study: Geotag
"Mark location of your photos"
Case Study: Geotag
"Mark location of your photos"
Case Study: SMS Replicator Secret
A spyware that secretly forwards every SMS to another number.
Case Study: SMS Replicator Secret
A spyware that secretly forwards every SMS to another number.
LIFE PEG
Abstraction
Phase
Verification
Phase
Apps
Permission Event Graph
Conformance or counter- examples
Policies
OF
Abstraction
Abstraction
Phase
Apps
Permission Event Graph
Abstraction: The Android Trinity
Event System
Sys. Libraries
Application
Application Code
System Code
Abstraction: The Android Trinity
Event System
Sys. Libraries
Application
States
Call event handler
Application Code
System Code
Abstraction: The Android Trinity
Event System
Sys. Libraries
Application
States
Call event handler
Call API
Application Code
System Code
Abstraction: The Android Trinity
Event System
Sys. Libraries
Application
States
Call event handler
Call API
Register handler
Application Code
System Code
Abstraction: The Algorithm
Summary-based
Abstract Interpretation on (P(aState) x P(API) x P(aState)).
Interprocedural CFG with a partially context sensitive points-to analysis
Summary-based
1200+ APIs
63 Kinds of Events
Event Semantics Engine
API Semantics Engine
Application Analyzer
SrcStates
(SrcStates, DstStates) Pairs
Event Handler
PEG
* Partial Valuation of the vars in ModeVar
* Partial Valuation of the vars in ModeVar
Verification: BFS for Conformance
Verification
Phase
Permission Event Graph
Conformance or counter- examples
Policies
Evaluation: PEG size (# states, CDF)
* 269 applications. Binary code sizes vary from 4KB to 6MB
LOG scale
CDF
# of States
Evaluation: Abstraction Time (CDF)
Sec
CDF
Evaluation: Verification Time (CDF)
* Always terminate within 3.6 hours
LOG scale
Sec
CDF
Conclusion
Questions ?
Kevin Chen <kevinchn@cs.berkeley.edu>
Backup Slides
Backup Slides
A
Native Code
Rewriting
Unresolved Reflection
Unresolved Dynamic dispatching
API Frequency in 95,000 Apps
Specification Constructs
Information Type | Example |
System status variables (Mode variables) | STOPButton.registered, MyActivity.inBackground |
System APIs and their arguments | android.location.Location: double getLatitude(), "content://com.android.contacts/contacts" |
Permissions | "android.permission.INTERNET" |
Specification Checker Interface
Bounded BFS for conformance analysis
Write the specification FSM using the following interfaces:
public int getStateId();
public void restoreFromStateId(int id);
public ListenerResult stateListener(ModelState state);
public ListenerResult actionListener(EventModality action);
public ListenerResult methodListener(PathItemMethod method);
Evaluation
Applications