# Call Graph and Model Checking for Fine-Grained Android Malicious Behaviour Detection
## 1 Introduction  
Mobile devices, such as smartphones but also smart TVs, wearables and voice assistants, play a fundamental role in our increasingly connected world. As a matter of fact, nowadays we use mobile devices for the most disparate tasks, such as turning on the heating in the house while we are coming back from the office or sharing the path taken by running with people who share the same passion. Clearly, the amount of information we daily share, even unknowingly, is really impressive. Indeed, 500 million tweets are posted every day and 294 billion emails are sent [1]. Four petabytes of data are created alone by Facebook users. Moreover, 65 billion messages are estimated on WhatsApp [2]. Following this data prediction, in 2025 we could estimate a trend of 463 exabytes of daily information: the equivalent of 212,765,957 DVDs per day [3]. Obviously, this great amount of private and sensitive information is of interest for attackers and, generally speaking, malicious users that are developing every day more and more aggressive techniques to exfiltrate data from our mobile devices. Even critical infrastructure are afflicted by malicious attacks, such as military [4], government [5] and healthcare [6]: these contexts are really crucial because attacks can have direct consequences also on human lives. Typically, malicious code developers focus on the platform that allows them to have the greatest attack surface. Indeed, the Android operating system, since 2017 the most widespread operating system in the world [7, 8] has largely attracted the interest of malicious developers. According to thesecurity experts of AV-Test, the cumulative number of Android malware was around 480 thousand samples in March 2020, with \"trojans\" as the most common type of malware [9]. The current techniques employed in commercial use to detect malicious mobile application are the same techniques adopted for malicious computer software (i.e., signature-based approach). In practice, the security analyst receives an application to analyse, and through a typically manual inspection process, detects the payload or the malicious code of the application. Subsequently, a signature will be generated from this code, which will be used to detect the same malicious code on user's devices. The main problem with this paradigm is that the malicious applications arrive in the labs of security experts, typically, when they are already widespread on the user's devices. Moreover, the attackers can generate obfuscated versions of the original malware and then bypass the antimalware checks. Trivial obfuscation and perturbation techniques, such as code reordering or junk code insertion, can effectively change the signature of malware, which will be no longer detected by antimalware. Based on these considerations, there is a need for novel methods for the detection of malware, especially in the Android environment due to its diffusion. In this paper, we propose an approach exploiting model checking for the detection of malicious families in Android malware. Basically, we represent an Android application as an automaton and, by exploiting a set of Temporal Logic formulae, we consider a formal verification environment to detect whether the behaviour codified in the formulae is exhibited from the automaton. Moreover, we improve the efficiency and precision of the detection by adopting two graphs data structure; we apply static analysis for reducing the search space and also detect the malicious code to a lower level. In detail, two different representations of the same application are considered. The first automaton is built starting from the Control Flow Graph (CFG) containing all the bytecode instructions; the second one is built starting from the Call Graph (CG), representing the call relationships between methods (and classes) of the application under analysis.