Analysis and verification of security data for IoT devices

Context. The 'Internet of Things' (IoT) is an umbrella term to describe the embedding of sensors, actuators, computing and connectivity to physical objects like buildings, vehicles, wearables, and other sorts of objects. This brings a wide range of exciting applications, e.g., for home automation, infrastructure management, health care, and environmental monitoring. But while there are many advantages, the ubiquitous collection of data also raises concerns about the security and privacy of the data produced, exchanged, and consumed by the 20 billion connected devices by 2020 (according to Gartner). This makes it imperative to impose control mechanisms and have a clear understanding of data flows and impacts of changes and manipulation attempts to the system, while considering the resource constrained and tamper-prone environments the devices run in.
Aim and objectives. The aim of this project is, in essence, to help end-users answer "what-if" questions, such as: "What if I add this new device to my existing configuration? If I change my privacy policy in a particular way? What if some device I connected with was malicious, or a connection breaks down?" Answering such questions is crucial to help users engage with connected devices, and to design tools to define and enforce security and privacy policies. To complete this aim, the student will address three main objectives.
Objective 1. A model for a personal system of connected devices, taking into account existing and emerging protocols sourcing information from real-world devices (e.g., FIDO and OAuth for IoT for the authentication, HyperCAT for discovery). This objective will be facilitated by the involvement of ARM, designer of the mbed device platform for IoT devices and services, and from the the Building as a Lab initiative, within which real-world data can be obtained from the Urban Sciences Building, a "smart" and monitored building in which the School of Computing Science will move in 2017.

Objective 2. A mechanism for analysis and verification, such that the model can be abstracted for a particular analysis, and then refined to project the result of the analysis into the real-world. Different tool support needs to be considered, depending on the type of analysis: rewriting (Maude), probabilistic model-checking (PRISM), theorem-proving (Isabelle/ISAR). This step will benefit from the expertise of Dr Griesmayer, who has an established track record in verification and abstraction/refinement, and from the existing collaboration between Dr Griesmayer and Dr Morisset on using verification techniques for security policies, published at ESORICS 2013.
Objective 3. A proper and usable interface, co-created and validated through user studies, embedding the model into real life situations. This step will be facilitated by the track record of Dr Morisset on the definition and implementation of access control policies, and from the Access Control Live Lab, a recently set up environment at Newcastle University where studies can be conducted on the usage of connected devices for access control. In particular, user studies investigating the definition of security and privacy policies by end-users are expected.

Expected impact. The proposal covers a wide area of research and allows to adjust for the skills and background of the selected doctoral student and to react on developments and standardisation efforts in a rapidly developing environment. But while the emphasis of the work is flexible, the effort will result in a better understanding and improved quality of security and privacy in IoT. We also expect to make a strong case to further the collaboration between ARM and Newcastle University, to which this project is a stepping stone.