# Call Graph and Model Checking for Fine-Grained Android Malicious Behaviour Detection
## 4 Experimental Analysis
### The \(\mu\)-Calculus Formulae
It represents the ratio of the number of relevant applications retrieved to the total number of relevant applications:

\[Recall=\frac{tp}{tp+fn}\]

where _fn_ is the false negatives number. The _F-Measure_ represents the weighted average between the recall and the precision metrics:

\[F-Measure= 2*\frac{Precision*Recall}{Precision+Recall}\]

The _Accuracy_ represents the classifications fraction resulting as correct and it is calculated as the sum between _tp_ and _tn_ divided by the full set of the the Android applications considered:

\[Accuracy= \frac{tp+tn}{tp+fn+fp+tn}\]

where _tn_ represents the true negative number. In Table 5, we present the results we obtained using the proposed approach. The proposed approach reaches an accuracy ranging between 0.97 and 1. In particular, for several families (Plankton, Opfake, Doublelocker, Locker and Simplelocker) we obtain an accuracy equal to 1, symptomatic that we are able to detect all the samples belonging to the specific family without misclassifying samples belonging to others families. An accuracy of 0.97 is obtained for the FakeInstaller family, while for the DroidKungFu, GinMaster,Add, Kmin, Geinimi, Koler, Pletor and Svpeng families we obtain an accuracy of 0.98. The remaining families (i.e., DroidDream, Fusob, Jisuit, Lockerpin and Porndroid) obtain an accuracy of 0.99, showing the ability of the proposed method to correctly detect most of the samples with the right belonging family. ## 5 Related Work

Previous researches demonstrated that formal verification can help to detect malware [8; 37; 38]. In the following, we describe malware detection methodologies employing formal methods, and briefly compare them to our approach. This section focuses mainly on Android malware detection with static analysis approaches, to compare our methodology with similar ones. We adopted the process algebra as the Formal Model to describe the functionalities of the malware under analysis, but many more approaches were adopted in the literature. For instance, the work by [PERSON] et al. [39] models the inner-working of the applications as a sequential program (PushDown System), and then classifies the applications by checking the model over Linear Temporal Logic formulas that express malicious behaviour. Similarly to our approach, the applications were first disassembled to smali code into Control Flow Graphs. Nevertheless, including the different Formal Models adopted, the two approaches differ also on the detection task. In our methodology, we tried to find formulas able to describe the behaviours of an entire malware family, while in the approach of [PERSON] et al. each formula expresses a specific malicious behaviour, not related to any malware family or malware variants. By doing so, they have to analyse the entire application in order to detect at least one of the malicious behaviours; contrarily, our approach focuses on specific behaviour per family and splits the analysis into two granularity levels, thus, it can efficiently detect malware by analysing only subsets of the Formal Model. Similarly to our approach, the Leila tool [28] also classifies Android apps into malware families by using a behavioural based approach. The tool is able to classify the application as belonging to a malware family and also localize the payload and the malicious code. The Leila tool adopts the process algebra to convert malicious behaviour to Temporal Logic formula, and their methodology can be easily compared to our second step of the analysis, the potentially malicious detection step. Nevertheless, our first step of the methodology narrows down the number of methods to analyse and make the entire approach liWeghter than the Leila one, preserving all the benefits. Moreover, the Leila tool was tested on 300 malware samples split among 6 different families, and 4 of them are included also in our dataset (\(FakeInstaller\), \(Plankton\), \(GinMaster\) and \(Opfake\)); we achieved better performance comparing the evaluation results of the four families in common between our datasets.