  The proliferation of Internet of Things (IoT) is reshaping our lifestyle.
With IoT sensors and devices communicating with each other via the Internet,
people can customize automation rules to meet their needs. Unless carefully
defined, however, such rules can easily become points of security failure as
the number of devices and complexity of rules increase. Device owners may end
up unintentionally providing access or revealing private information to
unauthorized entities due to complex chain reactions among devices. Prior work
on trigger-action programming either focuses on conflict resolution or
usability issues, or fails to accurately and efficiently detect such attack
chains. This paper explores security vulnerabilities when users have the
freedom to customize automation rules using trigger-action programming. We
define two broad classes of attack--privilege escalation and privacy
leakage--and present a practical model-checking-based system called SAFECHAIN
that detects hidden attack chains exploiting the combination of rules. Built
upon existing model-checking techniques, SAFECHAIN identifies attack chains by
modeling the IoT ecosystem as a Finite State Machine. To improve
practicability, SAFECHAIN avoids the need to accurately model an environment by
frequently re-checking the automation rules given the current states, and
employs rule-aware optimizations to further reduce overhead. Our comparative
analysis shows that SAFECHAIN can efficiently and accurately identify attack
chains, and our prototype implementation of SAFECHAIN can verify 100 rules in
less than one second with no false positives.
