# Detecting Colluding Inter-App Communication in Mobile Environment
## 3 Colluding Inter-App Communication Detection
Once obtained, all the \(\tau\)-automata for the GET and the PUT operations for the three collusion attacks we considered, we designed an algorithm, the flowchart of which is shown in Figure 2 for the automatic _Colluding Properties Generation_ step, in particular, for the generation of the properties for the _ExternalStorage_, the _SharedPreferences_, the _BroadcastReceiver_, and the _RemoteProcedureCall_ colluding detection. The idea behind the designed algorithm is to automatically infer a set of properties and, whether a PUT and a GET automata (related to _SharedPreferences_, _ExternalStorage_, _BroadcastReceiver_, or the _RemoteProcedureCall_) result in true to the properties including the same push action, in this case, we mark the PUT and the GET automata as performing a colluding attack. Below, we explain the algorithm steps in detail by considering the flowchart shown in Figure 2.  
For each attack, we consider i.e., _SharedPreferences_, _ExternalStorage_, _BroadcastReceiver_, and _RPC_, we take as input the set of \(\tau\)-automata related to the PUT operation (_set of PUT t-automata_ in the flowchart in Figure 2). For each PUT automaton, we obtain all the PUSH operations (by performing a _sort_ operation for displaying the set of visible actions of the automata ([[http://courses.cs.vt.edu/](http://courses.cs.vt.edu/)]([http://courses.cs.vt.edu/](http://courses.cs.vt.edu/))cs5204/fall00/CWB/top-level-coms.html)) and, for each action considering a push operation we automatically generate rules involved the push and following actions:  
* with regard to the _SharedPreferences_, we consider the \(invokegetSharedPreferences\) and the push under analysis;
* with regard to the _ExternalStorage_, we consider the \(invokegetExternalStorage\) and the push under analysis;
* with regard to the _BroadcastReceiver_, we consider the \(invokeptExtra\), \(invokegSend\)_Boradcast_ (for the PUT property), \(invokegTingExtra\), and \(invokStart\) (for the GET property);
* with regard to the _RemoteProcedureCall_, we consider the \(invokeptExtra\), \(invokestartservice\) (for the PUT property), \(invokegetStringExtra\), and \(invokevirtual\) (for the GET property). The properties are automatically generated by looking only the PUT \(\tau\)-automata, as shown from the flowchart in Figure 2.  
Figure 2: The colluding properties generation step. For instance, considering the PUT _ExternalStorage_\(\tau\)-automaton shown in Listing 4, the properties automatically generated by the proposed algorithm are shown in Table 7: for each push action of the \(\tau\)-automaton a property is generated. This process is repeated for each push action belonging to the PUT \(\tau\)-automata considered. When all the properties are generated for all the push actions of all the \(\tau\)-automata, the properties are stored in a file (_write generated properties_ in the flowchart in Figure 2). Subsequently, the model checker with the PUT and GET _t-automata_ and the properties obtained from the _Colluding Properties Generation_ step in Figure 1 is invoked: the properties are first verified on the PUT _t-automata_ and the formulae resulting TRUE are then checked with the GET _t-automata_: if the same property is resulting TRUE also on the GET \(\tau\)-automata there is a collusion. In this way, we found that the colluding attack is possible between the PUT and GET _t-automata_ i.e., between the (two or more) applications, whose PUT and GET models result in TRUE to the automatically generated property. Once we explained how the proposed approach works, below we present an example to better understand how the CCS automaton are built and how the automatic properties can detect the colluding attack. We consider two real-world applications performing a colluding attack by exploiting the _ExternalStorage_, in particular we consider a \(GET\) application (identified by the \(TZ35A08L2 KH3 CZ0 ILUCFMXLKP15N97M4\) hash) and a \(PUT\) application (identified by the \(VYFLWYY4J0 SHZ19 DIVWSTB1 CKMQLMS38\) hash).