Automatic security verification of mobile app configurations

The swift and continuous evolution of mobile devices is encouraging both private and public organizations to adopt the Bring Your Own Device (BYOD) paradigm. As a matter of fact, the BYOD paradigm drastically reduces costs and increases productivity by allowing employees to carry out business tasks on their personal devices. However, it also increases the security concerns, since a compromised device could disruptively access the resources of the organization. The current mobile application distribution model based on application markets does not cope with this issue. In a previous work the concept of secure meta-market has been introduced as a mean to distribute mobile applications always guaranteed to comply with any given BYOD policy. This is achieved through a suitable combination of static analysis (i.e. model checking) and code instrumentation techniques. Although crucial, enforcing security policies over individual applications is not sufficient in general. Indeed, several well documented threats arise from the malicious interaction among applications which are harmless if isolated. In this paper, a novel technique for the security verification of groups of mobile app is proposed. The approach relies on partial model checking (PMC) to extend the existing security guarantees to groups of applications. The experimental results demonstrate the viability of the approach. Moreover, we show through a case study that even a fairly simple security policy can be violated by applications which are compliant if considered one by one.