Comparing formal models of IoT app coordination analysis

The rising popularity of the Internet-of-Things (IoT) devices has driven their increasing adoption in various settings, such as modern homes. IoT systems integrate such physical devices with third-party apps, which can coordinate in arbitrary ways. However, malicious or undesired coordination can lead to serious vulnerabilities. This paper explores two different ways, i.e., a commonly-used state-based approach and a holistic, rule-based approach, to formally model app coordination and the safety and security thereof in the context of IoT platforms. The less common rule-base approach allows for a smaller, more scalable model. We realize both modeling approaches using bounded model checking with Alloy to automatically identify potential cases where apps exhibit coordination relationships. We evaluate the effectiveness of the modeling approaches by checking a corpus of real-world IoT apps of Samsung SmartThings and IFTTT. The experimental results demonstrate that our rule-based modeling leads to a more scalable analysis.