| Summary: | The difference between a malicious and a benign Android application can often be characterised by context and sequence in which certain permissions and APIs are used. We present a new technique for checking temporal properties of the interaction between an application and the Android event system. Our tool can automatically detect sensitive operations being performed without the user's consent, such as recording audio after the stop button is pressed, or accessing an address book in the background. Our work centres around a new abstraction of Android applications, called a Permission Event Graph, which we construct with static analysis, and query using model checking. We evaluate application-independent properties on 152 malicious and 117 benign applications, and application-specific properties on 8 benign and 9 malicious applications. In both cases, we can detect, or prove the absence of malicious behaviour beyond the reach of existing techniques.
|
|---|