MDSSED: A safety and security enhanced model-driven development approach for smart home apps

被引:1
作者
Ye, Tong [1 ]
Zhuang, Yi [1 ]
Qiao, Gongzhe [1 ]
机构
[1] Nanjing Univ Aeronaut & Astronaut, 29 Jiangjun Ave, Nanjing 211100, Jiangsu, Peoples R China
基金
中国国家自然科学基金;
关键词
Security; Safety; Smart home apps; Model-driven software development; Formal method; REQUIREMENTS;
D O I
10.1016/j.infsof.2023.107287
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Context: With the popularization of smart home devices, people rely more on automation functions provided by smart home apps. This increases the attack surface for safety and security threats. Many of these threats are at the interaction level, caused by unintended or malicious interactions between apps.Objective: Most of the current studies focus on identifying unsafe interactions between smart home apps by code analysis. To the best of our knowledge, none of the existing studies focuses on enhancing the safety and security of smart home apps under interaction threats in the design phase. To fill this gap, this paper presents MDSSED, a safety and security enhanced model-driven development approach for smart home apps.Method: First, this paper identifies eleven types of interaction threats faced by smart home apps. Second, the MDSSED profile is proposed to support modeling smart home apps using UML. Third, the MDSSED prototype tool is developed to generate threat models and corresponding safety and security properties automatically. Then, the safety and security properties are automatically verified by model checking. Finally, the MDSSED tool automatically converts the UML models to the Samsung SmartThings apps.Results: To evaluate the accuracy and effectiveness of MDSSED, this paper uses the benchmarks in existing state-of-the-art studies. The results show that MDSSED not only identified the safety and security problems in the existing benchmarks but also pointed out vulnerabilities of apps under other interaction threats identified in this paper.Conclusion: To the best of our knowledge, MDSSED is the first model-driven development approach that supports the automatic verification of the safety and security properties of smart home apps under interaction threats. The accuracy, practicality, and efficiency of MDSSED are corroborated by experiments. The source code of the MDSSED tool and the experimental data are available online.1
引用
收藏
页数:18
相关论文
共 42 条
  • [1] Alhanahnah M, 2020, PROCEEDINGS OF THE 29TH ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS, ISSTA 2020, P272, DOI 10.1145/3395363.3397347
  • [2] [Anonymous], 2021, SMARTTHINGS DEV DOCU
  • [3] [Anonymous], 2021, ECLIPSE PAPYRUS
  • [4] [Anonymous], 2021, SMARTTHINGS GROOVY I
  • [5] Hardening machine learning denial of service (DoS) defences against adversarial attacks in IoT smart home networks
    Anthi, Eirini
    Williams, Lowri
    Laved, Amir
    Burnap, Pete
    [J]. COMPUTERS & SECURITY, 2021, 108
  • [6] Basin D., 2003, 8 ACM S ACC CONTR MO
  • [7] Security modelling and formal verification of survivability properties: Application to cyber-physical systems
    Bernardi, S.
    Gentile, U.
    Marrone, S.
    Merseguer, J.
    Nardone, R.
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 2021, 171
  • [8] Bright P., 2021, SAMSUNGS TIZEN IS RI
  • [9] IoTGUARD: Dynamic Enforcement of Security and Safety Policy in Commodity IoT
    Celik, Z. Berkay
    Tan, Gang
    McDaniel, Patrick
    [J]. 26TH ANNUAL NETWORK AND DISTRIBUTED SYSTEM SECURITY SYMPOSIUM (NDSS 2019), 2019,
  • [10] Celik ZB, 2018, PROCEEDINGS OF THE 2018 USENIX ANNUAL TECHNICAL CONFERENCE, P147