# Call Graph and Model Checking for Fine-Grained Android Malicious Behaviour Detection
## 4 Experimental Analysis
### The \(\mu\)-Calculus Formulae
\begin{table}
\begin{tabular}{l c c c c} \hline \hline
**Family** & **Precision** & **Recall** & **F-Measure** & **Accuracy** \\ \hline FakeInstaller & 0.97 & 0.97 & 0.97 & 0.97 \\ Plankton & 1 & 1 & 1 & 1 \\ DroidKungFu & 0.98 & 0.99 & 0.98 & 0.98 \\ GinMaster & 0.98 & 0.98 & 0.98 & 0.98 \\ BaseBridge & 0.98 & 1 & 0.98 & 0.99 \\ Adrd & 0.97 & 0.98 & 0.97 & 0.98 \\ Kmin & 0.99 & 0.97 & 0.97 & 0.98 \\ Geinimi & 0.98 & 0.97 & 0.97 & 0.98 \\ DroidDream & 0.99 & 0.99 & 0.99 & 0.99 \\ Opfake & 1 & 1 & 1 & 1 \\ Doublelocker & 1 & 1 & 1 & 1 \\ Fusob & 0.98 & 1 & 0.98 & 0.99 \\ Jisuit & 0.98 & 0.99 & 0.98 & 0.99 \\ Koler & 0.98 & 0.98 & 0.98 & 0.98 \\ Locker & 1 & 1 & 1 & 1 \\ Lockerpin & 0.99 & 1 & 0.99 & 0.99 \\ Pletor & 0.98 & 1 & 0.98 & 0.98 \\ Porndroid & 0.99 & 1 & 0.99 & 0.99 \\ Simpleocker & 1 & 1 & 1 & 1 \\ Svpeng & 0.98 & 1 & 0.98 & 0.98 \\ Xbot & 0.99 & 1 & 0.99 & 0.99 \\ \hline \hline \end{tabular}
\end{table} 
Table 5: Performance evaluation. In addition, the paper by [PERSON] et al. [38] detected Android malware and classified them in families using formal methods. Our dataset includes also the two families analysed by their approach (\(DroidKungFu\) and \(Opfake\)), and we outperform their results on both of the families. A similar approach is applied by the Talos tool [8], which is focused on ransomware. It is able to pinpoint the payload location, achieves an accuracy of 0.99 and is also robust to obfuscation. The possibility to identify the malicious payload in Android malware using a model checking based approach were explored also by these papers [40; 41]. Being able to locate the payload code is essential for automatizing and extend the scope of formal verification tools, because allow formalising more and more specific and efficient Temporal Logic formulas by manual analysing the code. The paper by [PERSON] et al. [42] presents an approach to modelling a malware with Colored Petri nets, and discusses its possible applications. The paper is mainly theoretical and it does not provide experimental results to compare the approaches. [PERSON] et al. [43] presents the theoretical base for a framework able to produce abstracted program traces from malware, independently by the software language implementation. Their approach was applied to information leak detection task. They obtained a CFG from static analysis and collect the program set of traces. They also represent some malicious behaviour with First-Order Linear Temporal Logic, and then check if some of these behaviours were detected in the program traces. There are many similarities in our approaches, they also took into account the feasibility of the detection task in the search space, trying to address the problem of path explosion by applying techniques to restrict the set of traces. We also studied this problem and adopt the use of two graph data structures to reduce the search space and detection tasks to different granularities. The main difference resides in the practical application of the approaches proposed. While the work of [PERSON] et al. presents a formal framework mainly at a theoretical level, we provide a functional methodology for a well-defined problem in Android environment and present a robust experimental analysis to support our approach. In addition, the work by [PERSON] et al. [44] presents an interesting dynamic approach that takes into account, with static analysis, the problem of search space explosion. The authors have built a framework named DroidPF, based on Java PathFinder, which use software model checking to verify Android apps. The framework runs internally the application and explores the concrete state spaces, including simulated user interaction and environmental input. The state space is reduced using static analysis techniques and then the software model checking is applied to verify security properties and, eventually, pinpoint the actual violations and data leakage. Although this approach mainly uses dynamic tests on the apps, it adopts static analysis to reduce the problem of search space explosion.