摘要
以IFTTT为代表的事件驱动型物联网系统编程框架为用户构建满足其需求的智能家居物联网系统提供了极大的便利,但也带来了严峻的安全隐患。针对此问题,设计并实现了'门神',这是一个基于模型检验的事件驱动型物联网系统配置、仿真与验证平台。用户可以在门神中自定义其系统,并进行一键式模型驱动的仿真及验证、自动检测并重现错误场景,从而理解系统行为并提升其安全性。通过大量实验可知,门神能在86.7%的案例中发现安全隐患,且平均耗时仅为0.7 s。
The IFTTT style event-driven programming paradigm benefits normal users to build their own customized home automation Internet of things(IoT)system,meanwhile,it also brings serious safety and security risks.To handle this problem,Menshen was designed and implemented,an automated configuration,simulation and verification platform for event-driven home automation IoT system based on model checking.Users can easily set up their own smart home systems in Menshen,and conduct simulation and verification in a push-button style.Menshen could further demonstrate the error trace to help users to understand the behavior of the system and increase the safety and security of the system.An experiment with a large number of cases is carried out,and the results show that 86.7%cases are error-prone,and the verification only took 0.7 seconds in average.
作者
张秋萍
王熙灶
沈思远
张时雨
卜磊
李宣东
ZHANG Qiuping;WANG Xizao;SHEN Siyuan;ZHANG Shiyu;BU Lei;LI Xuandong(State Key Laboratory for Novel Software Technology,Nanjing University,Nanjing 210023,China)
出处
《物联网学报》
2019年第3期90-101,共12页
Chinese Journal on Internet of Things
基金
国家重点研发计划基金资助项目(No.2017YFA0700604)
国家自然科学基金资助项目(No.61632015,No.61572249,No.61561146394)
关键词
物联网
IFTTT框架
系统安全
模型检验
Internet of things
IFTTT framework
system security
model checking
