Explainability of Model Checking for Mobile Malicious Behavior Between Collaborative Apps Detection and Localisation

The technological development of recent years has made possible to improve the performance of mobile devices such as smartphones, tablets, smart TVs and wearable devices. This improvement has introduced the possibility of developing more complex applications able to manage sensitive user data. An example is represented by banking applications: they allow us to carry out all the financial operations that we can perform in a physical bank. Therefore, it is clear that in order to carry out these operations, we need a very high level of security to be sure that attackers do not use our account to transfer our money. Users typically install applications on their smartphones, without checking the required permissions before installation, because they do not know what risks they can encounter. Among the various malicious attacks that can be perpetrated, the collusive attack is emerging, as threat targeting devices based on the Android operating system. In this attack paradigm, two or more apps collaborate in some way to perform a malicious action that they are unable to do independently. Detection of colluding apps is a challenging task, as a matter of fact free and commercial antimalware analyse each app separately, hence fail to detect any joint malicious action performed by multiple collaborative apps through collusion. The contribution of this paper is a proposal of an explainable technique exploiting model checking, aimed to localise the malicious instructions in the application under analysis, by automatically identifying the bytecode instructions performing a malicious collusion and, for this reason, making the proposed method explainable.