# Call Graph and Model Checking for Fine-Grained Android Malicious Behaviour Detection
## 4 Experimental Analysis
### The \(\mu\)-Calculus Formulae  
In this section, we show an example of \(\mu\)-calculus formula we exploited for the detection of malicious payloads in Android environment. The formulae are generated from authors by deeply inspecting the code of a couple of malicious samples for family. The idea is to codify the malicious payload in a Temporal Logic formula to easily verify the maliciousness of an application without additional work from the security analysts, providing also a method for end user for malware detection. We recall also that the proposed method is aimed to exactly detect the package, the class and the method with the related Java byte code instructions performing the harmful action. As previously stated in the method section, we represent Android applications in terms of automaton and we verify several Temporal Logic properties (expressed in \(\mu\)-calculus to verify in a first step whether the application under analysis exhibit behaviour potentially malicious and, in a second step, to effectively check the maliciousness). We formulate two properties for each considered family: the first property is aimed to detect if the \(aua\) can exhibit a potentially malicious behaviour belonging to this family, while the second one to confirm the maliciousness of the analysed application. In particular, with the first property, we aim to detect if in the application exists a method showing a behaviour that can be sued for malicious purposes then, with the second property, we verify if this behaviour is effectively considered for malicious purposes. We evaluate the first property on an automaton build by exploiting the CFG of the application, while the second property is evaluated on an automaton built on the application CG. Below, we show a series of code snippets to better understand how we built both the properties and the related automata. In detail, the following snippets are related to a malicious Android sample identified by the _6 fdb3e091 ea01a692d2842057717971_ hash, belonging to the Simplelocker family. \begin{table}
\begin{tabular}{l l} \hline \hline
**Family** & **Description** & **\#** \\ \hline
**Fakelnstaller** & server-side polymorphic behaviour & 50 \\
**Plankton** & it exploits class loading to send user information & 50 \\
**DroidKungFu** & it executes a backdoor & 50 \\
**GimMaster** & it executes a malicious background service for devices rooting & 50 \\
**BaseBridge** & it sends sensitive information to a Command \& Control server & 50 \\
**Add** & it steals user and device information & 50 \\
**Kmin** & it forwards user information by sending messages to premium-rate numbers & 50 \\
**Geinimi** & first Android botnet & 50 \\
**DroidDream** & able to obtain root accesses & 50 \\
**Opfake** & first server side polymorphic Android malware & 50 \\
**Doublelocker** & able to change the PIN and to cipher device files by exploiting the AES algorithm & 3 \\
**Fusob** & It asks to pay a ramson from $100 to $200 United States dollars & 271 \\
**Jisuit** & it is aimed to show user information on the QQ social network & 173 \\
**Koler** & porting in the Android world of the Revetron ransomware & 183 \\
**Locker** & it shows a ransom messages quoting a Criminal Code article & 248 \\
**Lockerpin** & it is aimed to change the PIN on the infected device, but also to change it if it was already enabled & 181 \\
**Pictor** & mobile porting of the Cryptolocker ransomware & 278 \\
**Porndroid** & able to reset the PIN lock of the screen & 272 \\
**Simplelocker** & able to cipher the SD card files with the AES algorithm with a key hardcoded in the samples. & 221 \\
**Svpeng** & a keylogger able to steal bank credentials & 186 \\
**Xbot** & it exploits phishing to steal credit card data and banking credentials & 36 \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Malicious families’ description with the relative number of samples. Listing 3 shows the Java code snippet obtained for the sample belonging to the Simplelocker application.