Exploiting model checking for mobile botnet detection

Android malware is increasing from the point of view of the complexity and the harmful actions. As a matter fact, malware writers are developing sophisticated techniques to infect mobile devices very closed to their counterpart for personal computers. One of these threats is represented by the possibility to control the infected devices from the attacker i.e., the so-called botnet. In this paper a method able to identify botnet in Android environment through model checking is proposed. Starting from the malicious payload definition, the proposed method is able to detect and to localize the code related to the malicious botnet. We experiment real-world botnet based Android malware, obtaining encouraging results.