Scalable Analysis of Interaction Threats in IoT Systems

The ubiquity of Internet of Things (IoT) and our growing reliance on IoT apps are leaving us more vulnerable to safety and security threats than ever before. Many of these threats are manifested at the interaction level, where undesired or malicious coordinations between apps and physical devices can lead to intricate safety and security issues. This paper presents IotCom, an approach to automatically discover such hidden and unsafe interaction threats in a compositional and scalable fashion. It is backed with automated program analysis and formally rigorous violation detection engines. IotCom relies on program analysis to automatically infer the relevant app's behavior. Leveraging a novel strategy to trim the extracted app's behavior prior to translating them to analyzable formal specifications, IotCom mitigates the state explosion associated with formal analysis. Our experiments with numerous bundles of real-world IoT apps have corroborated IotCom's ability to effectively detect a broad spectrum of interaction threats triggered through cyber and physical channels, many of which were previously unknown, and to significantly outperform the existing techniques in terms of scalability.