# Call Graph and Model Checking for Fine-Grained Android Malicious Behaviour Detection
## 1 Introduction
For this reason, two different sets of formulas are considered: the first set, related to the automaton built from the CFG, aims to verify whether a certain, possible, malicious action is present into the application, while the second set aims to check if this behaviour is invoked in a certain path of the application. We demonstrate the effectiveness of the proposed model checking approach in the experimental analysis, obtaining an accuracy ranging from 0.97 to 1 in the evaluation of 2552 malware samples belonging to 21 different Android malware families and 500 more samples of legitimate applications. The malware families exhibit different behaviour, from payload able to extort private information to most recent locker and cypher ransomware. In the last years, researchers developed several methods aimed to detect malware in the mobile environment [10; 11], mainly based on machine learning techniques [12]. The main criticism of these techniques is the lack of explainability and interpretability. Indeed, machine learning models usually output a prediction (i.e., a label) without explaining the reason why some decisions were made [13]. Contrarily, formal methods can offer the opportunity to better understand the rationale behind a Temporal Logic formula, also through the adoption of the counterexample that can help the analyst to understand the reason why a formula is resulting false on a certain automaton [8]. Moreover, with the proposed method, we are able to localise the class, the method and also the instruction into the bytecode symptomatic of the malicious behaviour, reaching a very fine grain in the malware analysis. We summarize the main distinctive points of this work as follows:  
* we adopt two different graph data structures (CFGs and CGs) to describe the malware functionalities, using intra- and inter-procedural analysis;
* we exploit the strengths of the two graph data structures and the formal methods to reduce the search space and then mitigate one of the biggest weakness of the static analysis approaches;
* we propose a method able to precisely distinguish between malware and trusted application, and then also classify the malware into families;
* we propose a method able to precisely localize the malicious code in the malware under analysis;* we support the formal methods approaches as an interpretable approach to address malware classification tasks. Indeed, the Temporal Logic formulae are able to classify malware and also provide precise and soundness explanation of the outcome by using the counter-example;
* the experimental results reach an accuracy of 0.988, on a dataset of more than 3000 real-world Android samples, constituting 2552 malware belonging to 21 malicious families and 500 trusted applications. The paper proceeds as follows: the next section presents a short background about model checking, in order to introduce relevant notions for the readers who are not familiar with model checking. Section 3 describes the proposed method for malicious family detection in Android environment, while the experimental analysis results performed on a real-world Android dataset are discussed in Section 4. Section 5 reports a comparison with the current state-of-the-art literature and, finally, conclusion and future research works are discussed in Section 6.