.png){kind=icon}
.png){kind=icon}
Return
TapChecker: A Lightweight SMT-Based Conflict Analysis for Trigger-Action Programming
.png){kind=icon}
PRE
AI
DOI：10.1109/JIOT.2024.3374556.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Trigger-action programming (TAP) is a new programming paradigm enabling end-users to customize their smart devices by defining simple trigger-action rules. While it offers appealing convenience to end-users, TAP renders devices vulnerable to operation chaos and security risk resulting from potential defects in the rules. Verifying TAP rules defined by end-users is thereby necessary to detect such vulnerabilities at the early stage. However, such rules are difficult to analyze because their executions are often device-specific and environment-driven. Existing approaches require modeling them with their host devices and running environments, which is labor-consuming and hard to be automated. Moreover, the composition of devices causes state explosion, rendering the conflict analysis time-consuming. In this article, we first build a large corpus of TAP rules developed by end-users. Analyzing this corpus results in six types of conflicts and reveals that nearly 90% of end-users made conflicts in their customized rules, and on average, 3.7 rules contain a conflict, which concurs with the necessity of developing practical conflict analysis techniques. Empirical analysis motivates us to propose a lightweight SMT-based approach for conflict analysis from a programmatic perspective. Compared to the existing approaches, our approach does not require modeling devices; thus, it could be fully automatic and flexible in efficiently detecting various types of conflicts. We implement the approach in a tool TapChecker. We analyze 12 514 TAP rules collected from real-world TAP platforms (10 535) and laboratory experiments (1979). Experimental results show that our approach outperforms the state-of-the-art tool regarding the number of detected conflicts and efficiency.
Keywords:
Conflict verification
IFTTT
IoT
satisfiability modulo theory (SMT)
trigger-action programming (TAP)
Journal
IF:
8.9
Papers:
1.4W
Citations:
7.8W