# Call Graph and Model Checking for Fine-Grained Android Malicious Behaviour Detection
## 4 Experimental Analysis
### The \(\mu\)-Calculus Formulae
In this case, the property for the identification of the malicious behaviour is the one shown in Table 4.

The temporal property is aimed to confirm that the sample under analysis is effectively performing a ciphering operation coherently with the Simplelocker family behaviour; in particular, the property verifies that the CG slice automaton simultaneously exhibits the javatilArrayList_init,javaioFile_delete,javaioFile,javacryptoCipherOutputStream_write and the javasecurityMessageDigest_update actions, symptomatic of the operation related to file reading, ciphering and deleting. ### Implementation

For the generation of the CFG automata, we obtain the Java bytecode representation for each method of Android applications by invoking the _dex2 jar_ tool [33]. Starting from the _dex_ file (the executable file of the Android virtual machine), the tool extracts the _class_ files zipped as _.jar_, which makes possible to represent the Java byte-code representations of the class files stored in the _.jar_. The Soot framework was exploited to generate the CGs. Soot is a framework developed by the Sable Research Group at McGill University [34]. It supports the analysis and transformation of Java bytecode for optimization tasks and it is an open-source software available online [35]. We implemented a static analysis to generate the CG subgraph and to output the result as a CSS process. We are extending the Soot framework with more operations for handling, generate and export graph to CCS, our tool is available on Github [36]. Soot provides four different intermediate representations for Java bytecode. Among these, we used Jimple, a typed 3-address intermediate representation that forms a simplified version of Java source code. To apply Soot graph analyses, Java bytecode is converted to Jimple, where all the call statements (_InvokeStmt_ in Jimple) are marked to create the CG. Our tool implements a \begin{table}
\begin{tabular}{l l} \hline \(\psi_{1}\) & \(=\)\(\mu X.\)\(\langle javautilArrayList\_init\rangle\)tt\(\vee\)\(\langle-javautilArrayList\_init\rangle\)\(X\) \\ \(\psi_{2}\) & \(=\)\(\mu X.\)\(\langle javaioFile\_delete\rangle\)tt\(\vee\)\(\langle-javaFile\_delete\rangle\)\(X\) \\ \(\psi_{3}\) & \(=\)\(\mu X.\)\(\langle javaioFile\rangle\)tt\(\vee\)\(\langle-javaioFile\rangle\)\(X\) \\ \(\psi_{4}\) & \(=\)\(\mu X.\)\(\langle javascryptoCipherOutputStream\_write\rangle\)tt\(\vee\)\(\langle-javacryptoCipherOutputStream\_write\rangle\)\(X\) \\ \(\psi_{5}\) & \(=\)\(\mu X.\)\(\langle javasecurityMessageDigest\_update\rangle\)tt\(\vee\)\(\langle-javasecurityMessageDigest\_update\rangle\)\(X\) \\ \(\tilde{\psi}\) & \(=\)\(\psi_{1}\wedge\psi_{2}\wedge\psi_{3}\wedge\psi_{4}\wedge\psi_{5}\) \\ \hline \end{tabular}
\end{table} 
Table 4: Temporal logic property for Simplelocker malicious behaviour detection. \(SceneTransformer\) in the whole-jimple transformation pack (\(wjtp\)) to perform analyses to generate incrementally CFG, Program Dependence Graph and then the CG. ### Experimental Results

Below, we present the results obtained by the proposed approach. To evaluate the effectiveness in term of malicious family detection, we compute the precision, recall, F-measure and accuracy metrics. The _Precision_ represents the proportion of the Android applications truly belonging to a certain family among all those which were labelled to belonging to this family. It is the ratio of the number of relevant applications retrieved to the total number of irrelevant and relevant applications retrieved:

\[Precision=\frac{tp}{tp+fp}\]

where _tp_ represents the true positives number and _fp_ represents the false positives number. The _Recall_ is defined as the proportion of Android applications assigned to a certain malicious family, among all the Android applications truly belonging to the family under analysis; in other words, how many samples of the family under analysis were retrieved.