TAPFixer：基于否定属性推理的自动检测与修复家庭自动化漏洞
密码学与安全
2024-07-15 v1
摘要
触发-动作编程（TAP）是家庭自动化（HA）系统中流行的面向用户编程框架，使用户能够自定义家庭自动化并按预期控制设备。然而，其简化的语法也通过脆弱的规则交互引入了HA系统的新型安全威胁。在规则部署之前，准确地通过逻辑和物理消除其根本原因来修复这些漏洞至关重要。然而，这一问题尚未得到良好研究。本文提出了 TAPFixer，一个用于自动检测和修复HA系统中规则交互漏洞的新型框架。它从HA配置中提取 TAP 规则，将其翻译为包含物理和延迟特征的自动机模型，并进行各种正确性属性的模型检查。随后，它使用一种新的否定属性推理算法，通过模型抽象与细化和基于否定属性的模型检查来自动推断补丁。我们在市场HA应用（1177 条 TAP 规则和 53 个属性）上评估了 TAPFixer，发现其在修复规则交互漏洞方面可达 86.65% 的成功率。我们另邀请 23 名 HA 用户进行用户研究，表明 TAPFixer 在实际HA场景中进行漏洞修复具有实际用途。
引用
@article{arxiv.2407.09095,
title = {TAPFixer: Automatic Detection and Repair of Home Automation Vulnerabilities based on Negated-property Reasoning},
author = {Yinbo Yu and Yuanqi Xu and Kepu Huang and Jiajia Liu},
journal= {arXiv preprint arXiv:2407.09095},
year = {2024}
}