TAPInspector: Safety and Liveness Verification of Concurrent Trigger-Action IoT Systems

TL;DR

TAPInspector is a system that automatically detects safety and liveness rule interaction vulnerabilities in concurrent trigger-action IoT systems, addressing a gap in formal verification methods for such platforms.

Contribution

It introduces a novel hybrid model checking approach for verifying trigger-action IoT rules, identifying new interaction vulnerabilities and demonstrating practical effectiveness.

Findings

Identified 9 new rule interaction vulnerabilities in IoT platforms.

Detected 533 violations in real-world IoT apps.

Achieved at least 60000x speedup over baseline methods.

Abstract

Trigger-action programming (TAP) is a popular end-user programming framework that can simplify the Internet of Things (IoT) automation with simple trigger-action rules. However, it also introduces new security and safety threats. A lot of advanced techniques have been proposed to address this problem. Rigorously reasoning about the security of a TAP-based IoT system requires a well-defined model and verification method both against rule semantics and physical-world features, e.g., concurrency, rule latency, extended action, tardy attributes, and connection-based rule interactions, which has been missing until now. By analyzing these features, we find 9 new types of rule interaction vulnerabilities and validate them on two commercial IoT platforms. We then present TAPInspector, a novel system to detect these interaction vulnerabilities in concurrent TAP-based IoT systems. It automatically extracts TAP rules from IoT apps, translates them into a hybrid model by model slicing and state compression, and performs semantic analysis and model checking with various safety and liveness properties. Our experiments corroborate that TAPInspector is practical: it identifies 533 violations related to rule interaction from 1108 real-world market IoT apps and is at least 60000 times faster than the baseline without optimization.