Dissertation
Improving the safety of IoT systems using usable policy enforcement
University of Iowa
Doctor of Philosophy (PhD), University of Iowa
Autumn 2023
DOI: 10.25820/etd.006848
Abstract
IoT systems have proliferated our day-to-day lives, often residing in our personal spaces. The number of deployed IoT devices is predicted to increase from 13.5 billion in 2022 to 29.4 billion by 2030. IoT devices are typically designed with limited computational capabilities conforming only to their intended functionality, as well as driven by market pressures to reduce cost to ensure market reach. Such devices are commonly deployed in various configurations, where their individual functionalities combine in varying forms of complexity based on user requirements. To allow customization of the functionality and remote monitoring of these IoT systems, different (third-party) automation services have been deployed (e.g., IFTTT, OpenHAB, SmartThings). When automation services are integrated with a programmable IoT system, (custom) automation applications (or, just apps) — often obtained from untrusted sources, can be installed. Misbehavior of these installed apps can, however, result in the violation of the IoT system’s overall expected security and privacy properties. For users’ security and privacy, it isthus crucial to ensure that these automation-service-integrated-IoT systems behave as intended. In this thesis, we concretely capture this abstract guarantee in the form of the IoT system safety problem. In full generality, we prove that solving this problem is undecidable by reducing it to the Turing Machine Halting problem i.e. determining if a policy can transition an IoT system from an unsafe state to a safe one is undecidable. Even with this negative result, we show that it is possible to develop MAVERICK which solves this problem efficiently and in a platform-agnostic way while making assumptions that are reasonable in practice such as the number of devices, their behavior and the nature of communication. Unlike MAVERICK, prior work either does not support rich temporal invariants or cannot recover from unsafe state transitions. To aid users in configuring MAVERICK properly, we also develop an automated invariant synthesis approach along with a policy analysis approach. We implement MAVERICK in a prototype that has been shown to be effective in both physical and software-based test-beds while incurring only modest overhead. To further understand how users may interact with such policy enforcement systems, we also conduct a series of pilot user studies to measure the capability of users to write safety policies and measure the effects of training on such capabilities. While our study ran into issues due to participant unwillingness to engage with the surveys, we found that our participants (where willing) were often unable to define the correct policy statements for the given task. However, participants that were able to do so were mostly also able to internalize that policy, by describing cases where their policy would allow IoT device actions and where it would not. The general performance of the study also provided us with means to improve our survey methodology for future runs of our studies.
Details
- Title: Subtitle
- Improving the safety of IoT systems using usable policy enforcement
- Creators
- Muhammad Hammad Mazhar
- Contributors
- Omar Haider Chowdhury (Advisor)Alberto Maria Segre (Committee Member)Kasturi Varadarajan (Committee Member)Octav Chipara (Committee Member)Endadul Hoque (Committee Member)
- Resource Type
- Dissertation
- Degree Awarded
- Doctor of Philosophy (PhD), University of Iowa
- Degree in
- Computer Science
- Date degree season
- Autumn 2023
- Publisher
- University of Iowa
- DOI
- 10.25820/etd.006848
- Number of pages
- x, 81 pages
- Copyright
- Copyright 2023 Muhammad Hammad Mazhar
- Language
- English
- Date submitted
- 11/30/2023
- Description illustrations
- illustrations, graphs, tables
- Description bibliographic
- Includes bibliographical references (pages 64-70).
- Public Abstract (ETD)
- The Internet of Things, or IoT, has seen wide proliferation in various spheres of life including residential, commercial and industrial. Users deploy IoT devices in various complex configurations often called IoT systems, and often ’program’ these systems to perform meaningful tasks automatically (through automation rules). However, complex interactions between IoT device activity, environmental stimuli and malicious actors can influence an IoT system to act in ways unintended by the original user, leading to issues of safety, privacy or even efficiency. To that end, prior work has proposed solutions to curb such intended actions via enforcement of safety policies, but falls short of potentially solving the problem due to informal treatment of system structure and sources of unintended actions. In this thesis, we propose a formalized construction of this problem called the IoT System Safety Problem, or ISSP. ISSP is the problem of ensuring that a given IoT system satisfies a given policy by preventing IoT system actions that would lead to policy violations, or recover from a policy violation through the use of corrective actions. Through this construction, we show that the ISSP is theoretically undecidable by reducing the Turing Machine Halting Problem to solving the Decision ISSP problem i.e. determining that a series of corrective actions would recover a system from a policy violation is undecidable. Despite this result, we show that it is still possible to solve a tractable version of ISSP using reasonable assumptions applicable in real-world scenarios. We illustrate this result through MAVERICK, a dynamic runtime-monitoring system that enforces user-defined policies in programmable IoT systems. Additionally, we also study the usability of policy enforcement in IoT systems by studying user capability for defining safety policies for given configurations of IoT systems and automation rules as well as the effect of training on said capability. We conducted an online pilot study of 300 participants recruited through Amazon Mechanical Turk, and despite a majority of responses that were rejected due to attempted fraud, our study shows that users are unable to define policy for IoT systems and training had no effect on their capability.
- Academic Unit
- Computer Science
- Record Identifier
- 9984546541702771
Metrics
3 File views/ downloads
37 Record Views