Trigger-Action Programming (TAP) is a popular end-user programming framework in the home automation (HA) system, which eases users to customize home automation and control devices as expected. However, its simplified syntax also introduces new safety threats to HA systems through vulnerable rule interactions. Accurately fixing these vulnerabilities by logically and physically eliminating their root causes is essential before rules are deployed. However, it has not been well studied. In this paper, we present TAPFixer, a novel framework to automatically detect and repair rule interaction vulnerabilities in HA systems. It extracts TAP rules from HA profiles, translates them into an automaton model with physical and latency features, and performs model checking with various correctness properties. It then uses a novel negated-property reasoning algorithm to automatically infer a patch via model abstraction and refinement and model checking based on negated-properties. We evaluate TAPFixer on market HA apps (1177 TAP rules and 53 properties) and find that it can achieve an 86.65% success rate in repairing rule interaction vulnerabilities. We additionally recruit 23 HA users to conduct a user study that demonstrates the usefulness of TAPFixer for vulnerability repair in practical HA scenarios.

翻译：触发-动作编程（TAP）是家庭自动化（HA）系统中一种流行的终端用户编程框架，它使用户能够轻松地按预期定制家庭自动化并控制设备。然而，其简化的语法也通过脆弱的规则交互为HA系统引入了新的安全威胁。在规则部署之前，通过逻辑和物理方式消除其根本原因来准确修复这些漏洞至关重要。然而，这一问题尚未得到充分研究。本文提出TAPFixer，一种用于自动检测和修复HA系统中规则交互漏洞的新颖框架。它从HA配置文件中提取TAP规则，将其转换为具有物理和延迟特征的自动机模型，并利用各种正确性属性执行模型检测。随后，该框架采用一种新颖的否定性质推理算法，通过基于否定性质的模型抽象与精化以及模型检测，自动推断出修复补丁。我们在市售HA应用（包含1177条TAP规则和53项属性）上评估TAPFixer，发现其在修复规则交互漏洞方面能达到86.65%的成功率。我们还额外招募了23名HA用户进行了一项用户研究，结果证明了TAPFixer在实际HA场景中修复漏洞的有效性。