臺灣博碩士論文加值系統

物聯網設備的增加正在改變我們的生活型態：當所有感應器和裝置透過網路彼此溝通，使用者就可以透過客製自動化規則來滿足他們的需求。然而，除非謹慎地設計規則，這些自動化規則可能輕易地成為安全的缺口。對於一個未授權的使用者來說，裝置的主人可能不經意地透過規則提供更多裝置的權限（權限提升）或是洩漏機密的裝置資訊（隱私洩漏）。這篇論文探討當使用者利用觸發式自動化規則來客製化所造成的安全問題，並提出一個名為「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.

口試委員會審定書iii
誌謝v
Acknowledgements vii
摘要ix
Abstract xi
1 Introduction 1
2 Background 5
2.1 Trigger-Action Rules and IFTTT 5
2.2 Model Checking 6
2.3 A Motivating Example 7
3 Problem Definition 9
3.1 Threat Model 10
3.2 System Model 11
3.3 Desired Properties 13
4 VeriIoT 15
4.1 High-Level System Overview 16
4.2 Modeling 17
4.3 Verification 20
4.4 Optimization 23
4.5 Mitigation 27
5 Evaluation and Implementation 31
5.1 Security comparison 31
5.2 Implementation 33
5.3 Performance Evaluation 35
6 Discussion 39
7 Related Work 43
8 Conclusion 45
Bibliography 47

[1] Automate processes + tasks | Microsoft Flow. https://flow.microsoft.com/en-us/.
[2] Eclipse Kura ™ - Open Source framework for IoT. https://eclipse.org/kura/.
[3] Fridge sends spam emails as attack hits smart gadgets. http://www.bbc.com/news/technology-25780908.
[4] Gartner Says 8.4 Billion Connected ”Things” Will Be in Use in 2017, Up 31 Percent From 2016. https://www.gartner.com/newsroom/id/3598917.
[5] Getting lost near the Kremlin? Russia could be ’GPS spoofing’. http://money.cnn.com/2016/12/02/technology/kremlin-gps-signals/.
[6] Hackers can hijack Wi-Fi Hello Barbie to spy on your children. https://www.theguardian.com/technology/2015/nov/26/hackers-can-hijack-wifi-hello-barbie-to-spy-on-your-children.
[7] Home - Android Vulnerabilities. http://www.androidvulnerabilities.org/.
[8] Households have 10 connected devices now, will rise to 50 by 2020 |ET CIO. http://cio.economictimes.indiatimes.com/news/internet-of-things/households-have-10-connected-devices-now-will-rise-to-50-by-2020/53765773.
[9] Javaluator Home Page. http://javaluator.sourceforge.net/en/home/.
[10] Learn how IFTTT works - IFTTT. https://ifttt.com/.
[11] New study details a security flaw with Philips Hue smart bulbs. https://www.cnet.com/news/new-study-details-a-security-flaw-with-philips-hue-smart-bulbs/.
[12] NVD - Home. https://nvd.nist.gov/.
[13] Smart meters can be hacked to cut power bills. http://www.bbc.com/news/technology-29643276.
[14] SmartThings. Add a little smartness to your things. https://www.smartthings.com/.
[15] The future is this one-click remote for everything in your life. https://qz.com/346767/ifttt-pares-down-its-automation-service-to-prepare-forthe-one-click-smartwatch-future/.
[16] Zapier: The best apps. Better together. https://zapier.com/.
[17] A. A. Cárdenas, S. Amin, Z.-S. Lin, Y.-L. Huang, C.-Y. Huang, and S. Sastry. Attacks against process control systems: risk assessment, detection, and response. In Proceedings of the 6th ACM symposium on information, computer and communications security, pages 355–366. ACM, 2011.
[18] A. Costin, J. Zaddach, A. Francillon, and D. Balzarotti. A Large-Scale Analysis of the Security of Embedded Firmwares. In Proceedings of USENIX Security, 2014.
[19] R. Dimitrova, B. Finkbeiner, M. Kovács, M. N. Rabe, and H. Seidl. Model checking information flow in reactive systems. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 169–185. Springer, 2012.
[20] E. Fernandes, A. Rahmati, J. Jung, and A. Prakash. Decoupled-ifttt: Constraining privilege in trigger-action platforms for the internet of things. arXiv preprint arXiv:1707.00405, 2017.
[21] G. Ho, D. Leung, P. Mishra, A. Hosseini, D. Song, and D. Wagner. Smart Locks: Lessons for Securing Commodity Internet of Things Devices. In ACM ASIA CCS, 2016.
[22] Y. J. Jia, A. Chen, S. Wang, A. Rahmati, E. Fernandes, Z. M. Mao, and A. Prakash. ContexIoT: Towards Providing Contextual Integrity to Appified IoT Platforms. In NDSS, 2017.
[23] C.-j. M. Liang, L. Bu, Z. Li, and J. Zhang. Systematically Debugging IoT Control System Correctness for Building Automation. In ACM BuildSys, 2016.
[24] C.-j. M. Liang, B. F. Karlsson, N. D. Lane, F. Zhao, J. Zhang, Z. Pan, Z. Li, and Y. Yu. SIFT: Building an Internet of Safe Things. In Proceedings of International Conference on Information Processing in Sensor Networks, 2015.
[25] C. Maternaghan and K. J. Turner. Policy conflicts in home automation. Computer Networks, 57(12):2429–2441, 2013.
[26] S. Resendes, P. Carreira, and A. C. Santos. Conflict detection and resolution in home and building automation systems: a literature review. Journal of Ambient Intelligence and Humanized Computing, 5(5):699–715, 2014.
[27] M. Surbatovich, J. Aljuraidan, L. Bauer, A. Das, and L. Jia. Some Recipes Can Do More Than Spoil Your Appetite: Analyzing the Security and Privacy Risks of IFTTT Recipes. In Proceedings of the 26th International Conference on World Wide Web,2017.
[28] B. Ur, E. McManus, M. Pak Yong Ho, and M. L. Littman. Practical trigger-action programming in the smart home. In Proceedings of the 32nd annual ACM conference on Human factors in computing systems - CHI ’14, 2014.
[29] B. Ur, M. Pak, Y. Ho, S. Brawner, J. Lee, S. Mennicken, N. Picard, D. Schulze, and M. L. Littman. Trigger-Action Programming in the Wild: An Analysis of 200,000 IFTTT Recipes. In Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, 2016.
[30] D. I. Urbina, J. A. Giraldo, A. A. Cardenas, N. O. Tippenhauer, J. Valente, M. Faisal, J. Ruths, R. Candell, and H. Sandberg. Limiting the impact of stealthy attacks on industrial control systems. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pages 1092–1105. ACM, 2016.