TAPInspector：并发触发-动作物联网系统的安全性与活性验证
密码学与安全
2022-11-04 v2 人机交互
网络与互联网体系结构
软件工程
摘要
触发-动作编程（TAP）是一种流行的终端用户编程框架，可通过简单的触发-动作规则简化物联网（IoT）自动化，但也引入了新的安全与威胁。已有大量先进技术被提出以应对该问题。严格推理基于 TAP 的 IoT 系统的安全性，需要一个针对规则语义与物理世界特征（例如并发性、规则延迟、扩展动作、迟滞属性以及基于连接的规则交互）的明确定义模型与验证方法，而这一点此前一直缺失。通过分析这些特征，我们发现了 9 种新型规则交互漏洞，并在两个商用 IoT 平台上进行了验证。随后我们提出 TAPInspector，一种用于检测并发 TAP 物联网系统中此类交互漏洞的新系统。它自动从 IoT 应用中提取 TAP 规则，通过模型切片与状态压缩将其翻译为混合模型，并利用多种安全性与活性性质进行语义分析与模型检测。我们的实验证实 TAPInspector 具有实用性：它从 1108 个真实市场 IoT 应用中识别出 533 个与规则交互相关的违规，且比无优化的基线至少快 60000 倍。
引用
@article{arxiv.2102.01468,
title = {TAPInspector: Safety and Liveness Verification of Concurrent Trigger-Action IoT Systems},
author = {Yinbo Yu and Jiajia Liu},
journal= {arXiv preprint arXiv:2102.01468},
year = {2022}
}