VeriIoT: 在物聯網中檢驗觸發式自動化規則

Abstract

物聯網設備的增加正在改變我們的生活型態：當所有感應器和裝置透過網路彼此溝通，使用者就可以透過客製自動化規則來滿足他們的需求。然而，除非謹慎地設計規則，這些自動化規則可能輕易地成為安全的缺口。對於一個未授權的使用者來說，裝置的主人可能不經意地透過規則提供更多裝置的權限（權限提升）或是洩漏機密的裝置資訊（隱私洩漏）。這篇論文探討當使用者利用觸發式自動化規則來客製化所造成的安全問題，並提出一個名為「VeriIoT」的系統，透過模型檢查來偵測隱藏的自動化規則攻擊路徑：在有線自動機上面定義權限提升和隱私洩漏，透過剪枝和分群來降低驗證的複雜度，並探討一個貪婪演算法來自動提供修補。根據安全分析和實驗，VeriIoT 在檢測弱點和提供自動化修補的同時，也減少對於使用者的影響。

Proliferation of Internet of Things (IoT) is reshaping our lifestyle; with all IoT sensors and devices that communicate with each other via the Internet, people can customize operating rules to meet their needs. Unless carefully defined, however, such rules can easily become the point of security failure as the number of devices and the complexity of rules increase; to unauthorized users, device owners may end up unintentionally providing privileges to additional devices (privilege escalation), or revealing private information (privacy leakage). This paper explores the security vulnerabilities when users have freedom to customize automation rules using trigger-action programming, and proposes VeriIoT, a model checking-based solution to detect hidden attack paths that exploit automation rules. We formulate privilege escalation and privacy leakage in finite state machines, reduce verification complexities using the pruning and grouping optimizations, and discuss a greedy method to suggest automatic fixes. According to the security analysis and experiments, VeriIoT efficiently detects vulnerabilities and suggests automatic fixes to stop attacks while minimizing the impact on the intended usage and user involvement.