The diffusion of personal, network-enabled, electronic devices is forcing organizations to consider the enforcement of bring your own device (BYOD) policies; this proves to be true also for organizations that do not support BYOD computing models at all due to security concerns. In some cases, policies could be as simple as making “off limits” all kinds of personal devices, while in other cases, access to enterprise applications could be granted, subject to security and management policies.

This paper discusses the automatic enforcement of BYOD policies, not only in an empirical manner, but also through the application of formal methods. The proposed framework covers the aspects related to the enforcement of security policy and the analysis of application behaviors, aiming at a transparent user experience, minimizing changes to operating system interfaces and workflow, and providing ways to ensure device safety in a fully automated way.

The policy specification is provided using Hennessy-Milner logic (HML) and applying partial model checking (PMC) to create a specialized security policy. A formal proof of validity is given, together with empirical evidence of the feasibility of the proposed approach, obtained through the testing of 261 Android applications available from Google Play. This paper is interesting mainly for the use of formal methods to analyze the system, to provide correspondence between system description and properties of interest, and to pave the road toward the efficient automation of security processes.