# Detecting Colluding Inter-App Communication in Mobile Environment
## 3 Colluding Inter-App Communication Detection
The idea behind these properties is to obtain in a short time window four different sets of applications, each set related to a different collusion attacks (i.e., _SharedPreferences_, _ExternalStorage_, _BroadcastReceiver_, and _RPC_), and in each set we have the classes (i.e., the CCS automata) verifying the PUT and the \(GET\) properties for each collusion attack. The reduction in processing costs is given thanks to model checking (which considers as input a class modeled in terms of CCS and a temporal logic formula), which performs a screening and selects only the classes that could potentially generate a collusion. In this way, the number of classes to be tested is significantly reduced. Once obtained from the _Installed Applications_ the set of the applications that can potentially exhibit colluding behavior, the next steps depicted in Figure 1 detects whether two or more applications can effectively share information, thus performing a collusion attack. Thus, for each automata belonging to the _Candidate Colluding Apps_, we generate a simplified version containing only the action that can be involved in the collusion attack: for this reason, the actions that cannot be involved in the collusion attacks are set with \(\tau\) actions. In particular, the models resulting from the \(\tau\)-automata step contains the push action, symptomatic of read and write operations on a variable and a set of actions discriminating the _SharedPreferences_, the _ExternalStorage_, the _BroadcastReceiver_, and the _RPC_ colluding attacks. From the \(\tau\)-automata models we automatically generate a set of properties, aimed to verify whether two or more applications can effectively perform a colluding attack. Let us better understand how we built the \(\tau\)-automata with an example. In Listing 3, we show an example of automaton related to a PUT operation of an _ExternalStorage_ collusion attack, and in Listing 4, we show the related \(\tau\)-automaton. \begin{table}
\begin{tabular}{l l} \hline \hline \(Formula\_RPC\_PUT\) & \(Formula\_RPC\_PUT\) \\ \(\rho_{PUT}\) & \(=\)\(\mu X.\)\(\langle invokeputExtra\rangle\)\(\rho_{PUT_{1}}\vee\) \\  & \(\langle-invokeputExtra\rangle\)\(X\) \\ \(\rho_{PUT_{1}}\) & \(=\)\(\mu X.\)\(\langle invokestartService\rangle\)\(\tt t\vee\) \\  & \(\langle-invokestartService\rangle\)\(X\) \\ \hline \hline \end{tabular}
\end{table} 
Table 6: The \(\rho_{PUT}\) property detects methods invoking \(PUT\) operations on \(RemoteProcedureCalls(RPCs)\), while the \(\rho_{GET}\) property detects methods invoking \(GET\) operations by exploiting _RPC_. The automaton shown in Listing 3 results in _true_ to the property related to the _ExternalStorage_ PUT (i.e., \(\chi_{GET}\) in Table 4): as a matter of fact it shows an \(invokegetExternalStorage\) action and, after an undefined number of actions, the \(invokewrite\) one. Listing 4 shows the \(\tau\)-automaton related to the automaton shown in Listing 3: all the actions are translated into \(\tau\) actions (not of interest for the collusion detection), with the exception of the actions involving a _push_ operation (in this example _pushConstant1_, _pushConstant2_, and _pushConstant3_, respectively, to push into the stack the Constant1, Constant2, and Constant3 variables) and the \(invokegetExternalStorage\) one. In fact, we recall that for the GET and PUT automata, in addition to the push actions, the \(\tau\)-automata consider the \(invokegetExternalStorage\) action for the _ExternalStorage_ colluding attack whereas, for the _SharedPreferences_ attack we consider the \(invokegetSharedPreferences\) action and, for the _BroadcastReceiver_ attack we consider the \(invokeputExtra\), \(invokegendBoradcast\) (for the PUT), \(invokegStringExtra\), \(invokegStart\) (for the GET), and the push under analysis (for both the GET and PUT _BroadcastReceiver_ properties).