# Detecting Colluding Inter-App Communication in Mobile Environment
## 3 Colluding Inter-App Communication Detection
In Figure 3, we show the bytecode related to the Android application performing the \(PUT\) with the _ExternalStorage_ (1-Bytecode PUT in Figure 3), the CCS automaton generated by this bytecode snippet (2-CCS PUT in Figure 3) and the related \(\tau\)-automaton (indicated as 3-CCS \(\tau\)-PUT in Figure 3). The instructions in the bytecode performing the \(PUT\)_ExternalStorage_ are in lines 146 (the invocation for the SD card access) and 151 (the resource used fro data writing) and are translated with the processes in lines 4 and 8 of the CCS automata, as shown from Figure 3.  
Figure 4 shows the properties automatically generated. In particular, coherently with the formulae explained in Table 7, for each _push_ actions a formula is generated. In the method related to the \(PUT\)_ExternalStorage_ behaviors there are push actions related to following variable: \(HKABGLTZGMM4H2M\), 2500, \(r\), _Filesize_ \begin{table}
\begin{tabular}{l l} \hline \hline \(Formula\_Constant1\_push\) & \\ \(\zeta_{push1}\) & \(=\)\(\mu X\). \(\langle invokgeetExternalStorageDirectory\rangle\)\(\zeta_{push12}\)\(\vee\) \\  & \(\langle-invokgeetExternalStorageDirectory\rangle\)\(X\) \\ \(\zeta_{push12}\) & \(=\)\(\mu X\). \(\langle pushConstant1\rangle\) tt\(\vee\) \\  & \(\langle-pushConstant1\rangle\)\(X\) \\ \(Formula\_Constant2\_push\) & \\ \(\zeta_{push2}\) & \(=\)\(\mu X\). \(\langle invokgeetExternalStorageDirectory\rangle\)\(\zeta_{push22}\)\(\vee\) \\  & \(\langle-invokgeetExternalStorageDirectory\rangle\)\(X\) \\ \(\zeta_{push22}\) & \(=\)\(\mu X\). \(\langle pushConstant2\rangle\) tt\(\vee\) \\  & \(\langle-pushConstant2\rangle\)\(X\) \\ \(Formula\_Constant3\_push\) & \\ \(\zeta_{push3}\) & \(=\)\(\mu X\). \(\langle invokgeetExternalStorageDirectory\rangle\)\(\zeta_{push32}\)\(\vee\) \\  & \(\langle-invokgeetExternalStorageDirectory\rangle\)\(X\) \\ \(\zeta_{push32}\) & \(=\)\(\mu X\). \(\langle pushConstant3\rangle\) tt\(\vee\) \\  & \(\langle-pushConstant3\rangle\)\(X\) \\ \hline \hline \end{tabular}
\end{table} 
Table 7: The properties automatically generated for the \(\tau\)-automaton shown in Listing 4: the \(\zeta_{push1}\) property is related to the \(pushConstant1\) action, the \(\zeta_{push2}\) property is related to the \(pushConstant2\) action and the \(\zeta_{push3}\) property is related to the \(pushConstant3\) action. 140 TyrCatch: L19 to L20 handled by L21: jawa/io/IOException
141 new jawa/io/File
142 dup
143 new jawa/lang/StringBuilder
144 dup
145 invokespecial jawa/lang/StringBuilder. (initU)V
146 invokespecial jawa/lang/StringBuilder. (initU)V
147 invokesticat android/os/Inversion.getVertemalStorageDirectory()Ljava/io/File:
148 invokestitural jawa/lang/StringBuilder.append(Ljava/lang/String)Ljava/lang/StringBuilder;
149 lde -(java.lang/String)
150 invokestitural jawa/lang/StringBuilder.append(Ljava/lang/String)Ljava/lang/StringBuilder;
151 ldc -(TBDEGITZ02 MCM) (java.lang.String)
152 invokestitural jawa/lang/StringBuilder.append(Ljava/lang/String)Ljava/lang/StringBuilder;
153 invokestitural jawa/lang/StringBuilder.toString(Ljava/lang/String);
154 invokespecial jawa/io/File. Once the _PUT_ model is detected, with the relative property, able to potentially perform a collusion, in order to verify whether the collusion can be successfully perpetrated, there is the need to find the \(GET\) application. Figure 5 shows a snippet belonging to an Android application performing a \(GET\) operation on an _ExternalStorage_. In particular, we show the bytecode related to the Android application performing the \(GET\) with the _ExternalStorage_ (1-Bytecode GET in Figure 5), the CCS automaton generated by this bytecode snippet (2-CCS GET in Figure 5) and the related \(\tau\)-automaton (indicated as 3-CCS \(\tau\)-GET in Figure 5).