Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System

TL;DR

This paper introduces a new runtime monitoring approach using metric temporal logic with recursive definitions to detect privilege escalation in Android, demonstrating practical effectiveness on real devices.

Contribution

It develops a novel security policy language based on MTL with recursive call chain expressions and an efficient monitoring algorithm suitable for mobile devices.

Findings

Effective detection of privilege escalation attacks in Android

Monitor implementation does not require full event history

Modified Android kernel successfully integrated the monitoring system

Abstract

We present a design and an implementation of a security policy specification language based on metric linear-time temporal logic (MTL). MTL features temporal operators that are indexed by time intervals, allowing one to specify timing-dependent security policies. The design of the language is driven by the problem of runtime monitoring of applications in mobile devices. A main case the study is the privilege escalation attack in the Android operating system, where an app gains access to certain resource or functionalities that are not explicitly granted to it by the user, through indirect control flow. To capture these attacks, we extend MTL with recursive definitions, that are used to express call chains betwen apps. We then show how the metric operators of MTL, in combination with recursive definitions, can be used to specify policies to detect privilege escalation, under various fine grained constraints. We present a new algorithm, extending that of linear time temporal logic, for monitoring safety policies written in our specification language. The monitor does not need to store the entire history of events generated by the apps, something that is crucial for practical implementations. We modified the Android OS kernel to allow us to insert our generated monitors modularly. We have tested the modified OS on an actual device, and show that it is effective in detecting policy violations.