A Temporal Permission Analysis and Enforcement Framework for Android

Why Terminator

Permission-induced attacks, i.e., security breaches enabled by permission misuse, are among the most critical and frequent issues threatening the security of Android devices. By ignoring the temporal aspects of an attack during the analysis and enforcement, the state-of-the-art approaches aimed at protecting the users against such attacks are prone to have low-coverage in detection and high-disruption in prevention of permission-induced attacks. To address the aforementioned shortcomings, we present Terminator, a temporal permission analysis and enforcement framework for Android.

How Terminator Works

Leveraging temporal logic model checking, Terminator's analyzer identifies permission-induced threats with respect to dynamic permission states of the apps. At runtime, Terminator's enforcer selectively leases (i.e., temporarily grants) permissions to apps when the system is in a safe state, and revokes the permissions when the system moves to an unsafe state realizing the identified threats.

[Terminator picture]

Evaluation

The results of our experiments, conducted over thousands of apps, indicate that Terminator is able to provide an effective, yet non-disruptive defense against permission-induced attacks. We also show that our approach, which does not require modification to the Android framework or apps' implementation logic, is highly reliable and widely applicable.

The details of the evaluation results can be found here.

Artifacts

Our TLA+ model specifying the Android system with respect to permission-induced attacks can be found here.

Publications

More details about Terminator can be found in our publication:

[seal's logo]
[uci's logo]