  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 states, e.g., concurrency, rule latency, and
connection-based interactions, which has been missing until now. This paper
presents TAPInspector, a novel system to detect vulnerabilities in concurrent
TAP-based IoT systems using model checking. It automatically extracts TAP rules
from IoT apps, translates them into a hybrid model with model slicing and state
compression, and performs model checking with various safety and liveness
properties. Our experiments corroborate that TAPInspector is effective: it
identifies 533 violations with 9 new types of violations from 1108 real-world
market IoT apps and is 60000 times faster than the baseline without
optimization at least.
