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

arXiv: https://arxiv.org/abs/2102.01468 · HTML: https://mlsanity.com/paper/2102.01468/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Feb 2021.

## Built on by (most cited first, 1 of 1)

- [Proactive Detection of Physical Inter-rule Vulnerabilities in IoT Services Using a Deep Learning Approach](https://mlsanity.com/paper/2406.03836/) (2024)

## Abstract (arXiv)

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.