TAPFixer: Automatic Detection and Repair of Home Automation Vulnerabilities based on Negated-property Reasoning

Trigger-Action Programming（TAP）是家庭自动化（HA）系统中流行的终端用户编程框架，它使用户可以按预期自定义家庭自动化和控制设备。然而，它简化的语法也通过易受攻击的规则交互引入了新的安全威胁到HA系统中。在规则部署之前，通过逻辑和物理上消除其根本原因来准确修复这些漏洞至关重要。然而，这方面的研究还不充分。本文提出了TAPFixer，一种新颖的框架，用于自动检测和修复HA系统中的规则交互漏洞。它从HA配置文件中提取TAP规则，将其转换为具有物理和延迟特性的自动机模型，并使用各种正确性属性进行模型检查。然后，它使用一种新颖的否定属性推理算法，通过模型抽象和细化以及基于否定属性的模型检查自动推断出补丁。我们在市场上的HA应用程序（1177个TAP规则和53个属性）上评估了TAPFixer，并发现它可以在修复规则交互漏洞方面达到86.65％的成功率。我们还招募了23名HA用户进行用户研究，证明了TAPFixer在实际HA场景中用于漏洞修复的实用性。

TAPFixer试图解决Home Automation系统中Trigger-Action Programming (TAP)框架的规则交互漏洞问题。这是否是一个新问题？

TAPFixer采用模型检查和负属性推理算法来自动检测和修复规则交互漏洞。这种方法通过逐步抽象和细化模型来推断补丁，从而消除漏洞的根本原因。

论文使用市场上的HA应用程序进行了评估，发现TAPFixer在修复规则交互漏洞方面可以达到86.65%的成功率。此外，论文还进行了用户研究，证明了TAPFixer在实际HA场景中修复漏洞的实用性。

该领域的相关研究包括："Towards Automated Dynamic Analysis for Smart Home Apps"，"Towards Automated Testing and Fuzzing of Smart Home Applications"等。