Improving the safety of IoT systems using usable policy enforcement
Creators: name: Mazhar, Muhammad Hammad
Publisher: name: University of Iowa
Year: 2023
Subjects: IoT Systems
Policy Enforcement
Usability
public abstract

description: 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.