# Detecting Colluding Inter-App Communication in Mobile Environment
## 3 Colluding Inter-App Communication Detection
\begin{table}
\begin{tabular}{l l} \hline \hline \(Formula\_SP\_PUT\) & \(\varphi_{PUT}\) \\ \(\varphi_{PUT}\) & \(=\)\(\mu X.\) (\(invokegetSharedPreferences\)) \(\varphi_{PUT_{1}}\vee\) \\ \(\langle-invokegetSharedPreferences\rangle\)\(X\) \\ \(\varphi_{PUT_{1}}\) & \(=\)\(\mu X.\) (\(invokeedit\)) \(\varphi_{PUT_{2}}\vee\langle-invokedit\rangle\)\(X\) \\ \(\varphi_{PUT_{2}}\) & \(=\)\(\mu X.\) (\(invokegetString,invokepInt,invokegetFloat\)) \(\varphi_{PUT_{3}}\vee\) \\ \(\langle-invokegetString,invokeputInt,invokeputFloat\rangle\)\(X\) \\ \(\varphi_{PUT_{3}}\) & \(=\)\(\mu X.\) (\(invokecommit\)) \(\mathtt{tt}\vee\langle-invokecommit\rangle\)\(X\) \\ \(Formula\_SP\_GET\) & \(=\)\(\mu X.\) (\(invokegetSharedPreferences\)) \(\varphi_{GET_{1}}\vee\) \\ \(\langle-invokegetSharedPreferences\rangle\)\(X\) \\ \(\varphi_{GET_{1}}\) & \(=\)\(\mu X.\) (\(invokegetString,invokegetInt,invokegetFloat\)) \(\mathtt{tt}\vee\) \\ \(\langle-invokegetString,invokegetInt,invokegetFloat\rangle\)\(X\) \\ \hline \hline \end{tabular}
\end{table} 
Table 3: The \(\varphi_{PUT}\) property detects methods invoking \(PUT\) operations on _SharedPreferences_, while the \(\varphi_{GET}\) property detects methods invoking \(GET\) operations on _SharedPreferences_. \begin{table}
\begin{tabular}{l l} \hline \hline \(Formula\_SP\_PUT\) & \(\varphi_{PUT}\) \\ \(\varphi_{PUT}\) & \(=\)\(\mu X.\) (\(invokegetSharedPreferences\)) \(\varphi_{PUT_{1}}\vee\) \\ \(\langle-invokegetSharedPreferences\rangle\)\(X\) \\ \(\langle-invokegetSharedPreferences\rangle\)\(X\) \\ \(\langle-invokegetSharedPreferences\rangle\)\(X\) \\ \(\varphi_{GET_{1}}\) & \(=\)\(\mu X.\) (\(invokegetString,invokegetInt,invokegetFloat\)) \(\mathtt{tt}\vee\) \\ \(\langle-invokegetString,invokegetInt,invokegetFloat\rangle\)\(X\) \\ \hline \hline \end{tabular}
\end{table} 
Table 4: The \(\chi_{PUT}\) property detects methods invoking \(PUT\) operations on _ExternalStorage_, while the \(\chi_{GET}\) property detects methods invoking \(GET\) operations on _ExternalStorage_. \begin{table}
\begin{tabular}{l l} \hline \hline \(Formula\_BR\_PUT\) & \(\psi_{PUT}\) \\ \(\psi_{PUT}\) & \(=\)\(\mu X.\) (\(invokegetExtra\)) \(\psi_{PUT_{1}}\vee\) \\ \(\langle-invokegetExtra\rangle\)\(X\) \\ \(\psi_{PUT_{1}}\) & \(=\)\(\mu X.\) (\(invokesendBroadcast\)) \(\mathtt{tt}\vee\) \\ \(\langle-invokesendBroadcast\)) \(\mathtt{X}\) \\ \(\langle-invokesendBroadcast\)) \(\mathtt{X}\) \\ \(Formula\_BR\_GET\) & \(\psi_{GET_{1}}\vee\) \\ \(\langle-invokegetStringExtra\rangle\)\(X\) \\ \(\psi_{GET_{1}}\) & \(=\)\(\mu X.\) (\(invokestart\)) \(\mathtt{tt}\vee\) \\ \(\langle-invokestart\rangle\)\(X\) \\ \hline \hline \end{tabular}
\end{table} 
Table 5: The \(\psi_{PUT}\) property detects methods invoking \(PUT\) operations on _BroadcastReceiver_, while the \(\psi_{GET}\) property detects methods invoking \(GET\) operations on _BroadcastReceiver_. In Table 6, we show the \(\rho_{PUT}\) and the \(\rho_{GET}\) detect PUT and GET operations, respectively, when the _RPC_ channel is exploited. In this case, we encode the following actions by exploiting the \(\mu\)-calculus logic:  
* when an application executes a PUT action on a Remote Procedure Call (RPC) channel, the formula (Table 6--\(Formula\_RPC\_PUT\)) results true if the following actions are performed: _invokeputExtra, invokestartService_;
* when instead an application executes a GET action on a RPC channel, the formula (Table 6--\(Formula\_RPC\_GET\)) results true if the following actions are performed: _invokegetStringExtra_ and _invokewirtual_. We highlight that the CWB-NC is exploited in two different times by the proposed method: the first one to detect the methods candidate for the collusion (by detecting \(GET\) and \(PUT\)), and the second time to detect the applications that collude with each other, by identifying also the shared resources.