Formal modeling and automatic enforcement of Bring Your Own Device policies

The emerging Bring Your Own Device (BYOD) paradigm is pushing the adoption of employees’ personal mobile devices (e.g., smartphones and tablets) inside organizations for professional usage. However, allowing private, general purpose devices to interact with proprietary, possibly critical infrastructures enables obvious threats. Unfortunately, current mobile OSes do not seem to provide adequate security support for dealing with them. In this paper, we present a formal modeling and assessment of the security of mobile applications. In particular, we propose a security framework for verifying and enforcing BYOD security policies on Android devices. Interestingly, our approach is non-invasive and only requires minor platform modifications at application level. Finally, we provide empirical evidence of the practical feasibility of the approach by means of a prototype which we used to validate a set of real Android applications.