Identifying Insecure Features in Android Applications using Model Checking

Nowadays Android is the most widespread operating system. This is the reason why malware writers target it. Both researchers and commercial antimalware provide several solutions to fix and detect this phenomenon. They analyze one single application per time using combinations of static, dynamic and behavior based techniques. However, one of the last new threats is the collusion attack. In order to perpetrate this attack the malicious behaviour is divided between two or more applications: collusion refers to multiple applications that accomplish their fragment of malicious behaviour and then communicate using the Inter Component Communication mechanism provided by Android platform. Basically the colluded applications intentionally put in view private and sensitive information. The aim of this paper is to investigate whether legitimate and malware applications share private data. One way to exchange data between different applications in Android environment is through Shared Preferences. In this preliminary work we investigate whether an application transfers data using Shared Preferences with public visibility.