Model Checking to Detect the Hummingbad Malware

Typically, when a platform is widely disseminated, malicious writers focus their attention in order to perpetrate attacks on the widespread environment. This is the reason why nowadays there exists a series of attacks targeting the Android operating system, the most common platform available for mobile devices. In this paper we present a tool implementing a model checking-based approach to identify Android malware. Furthermore, the tool is also useful to localize the malicious behaviour of the application under analysis code. We evaluate the effectiveness of the tool on real-world samples belonging to the HummingBad malware family, one of the most recent and aggressive Android threats.