View article

Android is an operating system designed mainly for mobile devices, such as smartphones and tablets. It accounts for a large percentage of operating systems used in mobile devices today, and it is increasingly targeted by malwares. In this paper, we present an approach to improve Android security via runtime verification. Our approach includes a custom reference monitor, residing in the Linux kernel underlying the Android OS, that enforces security policies written in a formal logical language called linear temporal logic (LTL). LTL formulas are used to specify malicious patterns of accesses, based on the history of system events in Android. In a previous work, we described the theoretical foundations underlying our monitoring framework and its realization in a customized Android OS called LogicDroid. Here we show a real case study demonstrating the effectiveness of the additional security mechanism in …