# Call Graph and Model Checking for Fine-Grained Android Malicious Behaviour Detection
## 4 Experimental Analysis
### The \(\mu\)-Calculus Formulae
Basically, it exhibits several instructions aimed to cipher a file using the AES encryption. ```
1 public(finalString){
2 finalMessageDigestinstance-MessageDigest.getInstance(\"SHA-256\");
3 instance.update(s.getBytes(\"UTF-8\"));
4 finalbyte1 array-newbyte[32];
5 System.arraycopy(instance.digest(),0,array,0,array.length);
6 this.a-Cipher.getInstance(\"AES/CBC/PKCS/Padding\");
7 this.b-newSecretKeySpec(array,\"AES\");
8 this.c-newI%ParameterSpec(newbyte[16]);
9}
```  
Listing 3: A Java code snippet of a samples belonging to the Simplelocker family. ```
1 publica(java.lang.StringargO){//<init>//(Ljava/lang/String;)}
2 alood/referencetoself;
3 invokespecialjava/lang/Object.<init>()V
4 ldc\"SHA-256\"{java.lang.String}
5 invokesstaticjava/security/MessageDigest.getInstance(Ljava/lang/String;)Ljava/security/MessageDigest;
6 astore2
7 aload2
8 aload1
9 ldc\"UTF-8\"{java.lang.String}
10 invokesvirtualjava/lang/String.getBytes(Ljava/lang/String;)[B
11 invokesvirtualjava/security/MessageDigest.update((B)V
12 bipush32
13 newarrayB
14 astore1
15 aload2
16 invokesvirtualjava/security/MessageDigest.digest()[B
17 iconst_0
18 aload1
19 icomst_0
20 aload1
21 araylength
22 invokestitematicjava/lang/System.arraycopy(Ljava/lang/Object;ILjava/lang/Object;II)V
23 alood/referencetoself
24 lde\"AES/CBC/PKCSPadding\"{java.lang.String}
25 invokestitaticjava/crypto/Cipher.getInstance(Ljava/lang/String;)Ljava/crypto/Cipher;
26 purtiefalorgsimpledcker/a.a:javax.crypto.Cipher
27 alood/referencetoself
28 newjava/crypto/spec/SecretKeySpec
29 dup
30 aload1
31 ldc\"AES\"{java.lang.String}
32 invokespecialjava/crypto/spec/SecretKeySpec.<init>({BLjava/lang/String;)V
33 purtiefalorgsimpledcker/a.b:javax.crypto.spec.SecretKeySpec
34 alood/referencetoself
35 newjavax/crypto/spec/I%ParameterSpec
36 dup
37 bibush16
38 newarrayS
39 invokespecialjava/crypto/spec/I%ParameterSpec.<init>({BLV}
40 purtiefalorgsimpledcker/a.c:java.security.spec.AlgorithmParameterSpec
41 return
42}
```  
Listing 4: A Java bytecode snippet of a samples belonging to the Simplelocker family. As shown from the Java bytecode snippet in Listing 4, there are several _ldc_ instructions, aimed to push a one-word constant into the operand stack, containing all the arguments used by the ciphering operation. Moreover, in the bytecode we found also the invocation of classes considered for ciphering, such as MessageDigest, Cipher and SecretKeySpec. As stated in the method section, we resort to bytecode because it is always obtainable, even if the application is obfuscated with strong morphing techniques. In Figure 3, there is a fragment of CCS automaton obtained from the Java bytecode snippet shown in Listing 4. The fragment basically shows the sequence of the bytecode instruction, with the only exception that the bytecode ldc instructions are replaced with the push ones. Table 3 shows the Temporal Logic property for the identification of potentially malicious behaviour belonging to the Simplelocker family. The model is resulting true if the different actions (i.e., bytecode instructions) expressed in the property are present in the model, regardless of the number of other actions that are within the model. In this case, the CFG automaton is resulting true, because it exhibits the following actions: pushSHA256 (in the row 2 of the fragment in Figure 3), invokegetInstancepushAESCBPKCS7 Padding (in the row 15 of the fragment in Figure 3), newjavaxcryptospecSecretKeySpec (in the row 17 of the fragment in Figure 3), pushAES (in the row 18 of the fragment in Figure 3) and invokeinit (in the row 19 of the fragment in Figure 3). In this case, we mark the application under analysis as potentially malicious. As a matter of fact, there are several applications that can be performed for legitimate purposes ciphering operations; for instance, for data protection.