Abstract

The number of devices (phones, tablets, smart TVs, ...) using Android OS is continuously and rapidly growing. Together with the devices, also the amount of applications and on-line application market- places is increasing. Unfortunately, security guarantees are not evolving concurrently and security flaws have been reported. Far from discouraging them, more and more users and organisations rely on Android even for security critical activities. The bring your own device (BYOD) paradigm con- firms this trend. Indeed, it allows mobile devices to join a virtual organisation (consisting of a set of federated devices) in order to access to services and functionalities. Needless to say, the basic security support offered by Android and application markets is totally inappropriate for dealing with the security requirements involved in BYOD-like scenarios. In this work we describe a technique for guaranteeing that devices comply with a security policy. To do that, we use a type and effect system to infer behavioural models from applications imple- mentation and we validate them against policy specification. Moreover, we define a novel approach, based on partial model checking, for partially evaluating the security policy depending on devices configurations. Finally, we present a prototype under implementation, called BYODroid, which con- cretely applies these techniques to secure the devices joining a virtual organisations in the BYOD style.