StateDroid: Stateful Detection of Stealthy Attacks in Android Apps via Horn-Clause Verification

Profit-driven cyber-criminals are motivated to prolong Android malware's lifetime by hiding malicious behaviors from raising suspicion. Stealthy malware has become an emerging challenge to Android security as it can remain undetected for quite a long time. However, traditional defense techniques are insufficient in face of this new threat. Our in-depth study on published malware analysis reports and corresponding code analysis leads to three key observations: 1) a stealthy attack goes through multiple states; 2) state transitions are caused by a sequence of attack actions; 3) an attack action typically involves several Android APIs on different objects.

These insights motivate us to design a two-layer finite state machine (FSM) model, named StateDroid, to depict multi-step stealthy attacks in terms of state transitions. Our goal is to reason about various stealthy attacks from an Android app in one pass. However, the heterogeneous characteristics of attack actions make automatic construction of accurate detection model a challenging work. To overcome this obstacle, StateDroid abstracts the semantics of Android APIs and attacks as Horn clauses, and then it automatically constructs the two-layer FSM model via Horn-clause verification. We have developed an open-source prototype of StateDroid and evaluated it extensively with ground truth dataset, 1,505 Google Play apps, and 1,369 malicious apps, respectively. The encouraging experimental results demonstrate the efficacy of StateDroid. Our study shows stealthy attacks have been quite common among new-generation malware such as notorious ransomware, and we even identify 7.5% of recent Google Play apps exhibit unexpected stealthy behaviors.