Capturing mobile security policies precisely
The security policies of mobile devices that describe how we should use these devices are often informally specified. Users have preferences for some apps over others. Some users may avoid apps which can access large amounts of their personal data, whilst others may not care. A user is unlikely to write down these policies or describe them using a formal policy language. This is unfortunate as without a formal description of the policy we cannot precisely reason about them. We cannot help users to pick the apps they want if we cannot describe their policies. Companies have mobile security policies that definehowan employee should use smart phone devices and tablet computers from home at work. A company might describe the policy in a natural language document for employees to read and agree to. They might also use some software installed on employee’s devices to enforce the company rules. Without a link between the specification of the policy in the natural language document and the implementation of the policy with the tool, understanding how they are related can be hard. This thesis looks at developing an authorisation logic, called AppPAL, to capture the informal security policies of the mobile ecosystem, which we define as the interactions surrounding the use of mobile devices in a particular setting. This includes the policies of the users, the devices, the app stores, and the environments the users bring the devices into. Whilst earlier work has looked on checking and enforcing policies with low-level controls, this work aims to capture these informal policy’s intents and the trust relationships within them separating the policy specification from its enforcement. This allows us to analyse the informal policies precisely, and reason about how they are used. We show how AppPAL instantiates SecPAL, a policy language designed for access control in distributed environments. We describe AppPAL’s implementation as an authorisation logic for mobile ecosystems. We show how we can check AppPAL policies for common errors. Using AppPAL we show that policies describing users privacy preferences do not seem to match the apps users install. We explore the di↵erences between app stores and how to create new ones based on policy. We look at five BYOD policies and discover previously unexamined idioms within them. This suggests aspects of BYOD policies not managed by current BYOD tools.