基于时间自动机的物联网网关安全系统的建模及验证

doi:10.11959/j.issn.1000-436x.2018042

通信学报 ›› 2018, Vol. 39 ›› Issue (3): 63-75.doi: 10.11959/j.issn.1000-436x.2018042

• 论文Ⅰ：物联网与安全 • 上一篇下一篇

基于时间自动机的物联网网关安全系统的建模及验证

王国卿,庄雷(),王瑞民,宋玉,张坤丽

郑州大学信息工程学院，河南郑州 450001

修回日期:2018-02-20 出版日期:2018-03-01 发布日期:2018-04-02
作者简介:王国卿（1989-），男，山东临沂人，郑州大学博士生，主要研究方向为模型检测、形式化分析、物联网安全等。|庄雷（1963-），女，山东日照人，博士，郑州大学教授、博士生导师，主要研究方向为模型检测、未来网络架构、网络虚拟化等。|王瑞民（1974-），男，河南安阳人，博士，郑州大学副教授，主要研究方向为密码学、信息安全、物联网安全等。|宋玉（1969-），男，河南邓州人，郑州大学副教授，主要研究方向为数据挖掘、物联网体系结构、人工智能等。|张坤丽（1977-），女，河南巩义人，郑州大学讲师，主要研究方向为人工智能、自然语言处理等。
基金资助:
国家自然科学基金资助项目(61379079);河南省科技攻关计划基金资助项目(172102210478);河南省国际科技合作计划基金资助项目(152102410021)

Modeling and verifying based on timed automata of Internet of things gateway security system

Guoqing WANG,Lei ZHUANG(),Ruimin WANG,Yu SONG,Kunli ZHANG

School of Information Engineering,Zhengzhou University,Zhengzhou 450001,China

Revised:2018-02-20 Online:2018-03-01 Published:2018-04-02
Supported by:
The National Natural Science Foundation of China(61379079);The Science and Technology Key Project of Henan Province(172102210478);The International Cooperation Program of Henan Province(152102410021)

摘要/Abstract

摘要：

物联网是一个多网异构融合网络，其感知层常面临各类安全威胁。物联网网关作为感知层和网络层的桥梁，应当具备安全管理功能，防止安全问题向上层扩散。针对物联网网关目前安全方面的不足，以物联网网关中间件技术为平台，设计一个通用的物联网网关安全系统。该系统可以嵌入不同的安全协议或算法，然后进行建模与分析，能够辅助安全网关的设计和具体实现。利用时间自动机对系统进行形式化建模与验证，验证结果表明物联网网关安全系统满足机密性、可用性、真实性、顽健性、完整性和新鲜性6项安全需求。

关键词: 物联网网关, 安全系统, 中间件, 时间自动机, 模型检测

Abstract:

The Internet of things (IoT) is a multiple heterogeneous network,and its perception layer is often faced with various security threats.As the bridge between the perception layer and the network layer,the IoT gateway should have the security management function to prevent the security issue from spreading to the upper layer.According to the current security deficiencies in IoT gateway,a universal IoT gateway security system was proposed based on the IoT gateway middleware technology.Various security protocols or algorithms can be embedded in IoT gateway security system,and the modeling and analysis can help the design and implementation of IoT gateway.The formal modeling and verification of the IoT gateway security system was performed by timed automata.The results show that the IoT gateway security system satisfies the security properties of confidentiality,availability,authenticity,robustness,integrity and freshness.

Key words: IoT gateway, security system, middleware, timed automata, model checking

中图分类号:

TP393

王国卿,庄雷,王瑞民,宋玉,张坤丽. 基于时间自动机的物联网网关安全系统的建模及验证[J]. 通信学报, 2018, 39(3): 63-75.

Guoqing WANG,Lei ZHUANG,Ruimin WANG,Yu SONG,Kunli ZHANG. Modeling and verifying based on timed automata of Internet of things gateway security system[J]. Journal on Communications, 2018, 39(3): 63-75.

图/表 16

图1

表1

图2

图3

表2

表3

表4

图4

图5

图6

图7

图8

图9

图10

图11

表5

参考文献 21

[1]	王良民, 熊书明 . 物联网工程概论[M]. 北京: 清华大学出版社, 2011: 45-52.
	WANG L M , XIONG S M . The introduction of IoT engineering[M]. Beijing: Tsinghua University PressPress, 2011: 45-52.
[2]	钱志鸿, 王义君 . 物联网技术与应用研究[J]. 电子学报, 2012,40(5): 1023-1029.
	QIAN Z H , WANG Y J . IoT technology and application[J]. Acta Electronica Sinica, 2012,40(5): 1023-1029.
[3]	MORABITO R , BEIJAR N . A framework based on SDN and containers for dynamic service chains on IoT gateways[C]// The Workshop on Hot Topics in Container Networking and Networked Systems. 2017: 42-47.
[4]	SATHYADEVAN S , VEJESH V , DOSS R ,et al. Portguard an authentication tool for securing ports in an IoT gateway[C]// IEEE International Conference on Pervasive Computing and Communications Workshops. 2017: 624-629.
[5]	SCHRICKTE L F , MONTEZ C B , OLIVEIRA R S D ,et al. Design and implementation of a 6LoWPAN gateway for wireless sensor networks integration with the internet of things[J]. International Journal of Embedded Systems, 2016,8(5/6): 380-390.
[6]	陈琦, 韩冰, 秦伟俊 ,等. 基于 Zigbee/GPRS 物联网网关系统的设计与实现[J]. 计算机研究与发展, 2011,48(s2): 367-372.
	CHEN Q , HAN B , QIN W J ,et al. Design and implementation of the IoT gateway based on Zigbee/GPRS protocol[J]. Journal of Computer Research and Development, 2011,48(s2): 367-372.
[7]	ZHANG L , ALHARBE N R , ATKINS A S . A self-adaptive distributed decision support model for Internet of things applications[J]. Transactions of the Institute of Measurement and Control, 2017,39(4): 404-419.
[8]	罗俊海, 周应宾, 邓霄博 . 物联网网关系统设计[J]. 电信科学, 2011,27(2): 105-110.
	LUO J H , ZHOU Y B , DENG X B . Design for gateway system in Internet of things[J]. Telecommunications Science, 2011,27(2): 105-110.
[9]	CHEN H C , YOU I , WENG C E ,et al. A security gateway application for end-to-end M2M communications[J]. Computer Standards ＆ Interfaces, 2016,44(C): 85-93.
[10]	MIN D , XIAO Z , SHENG B ,et al. Design and implementation of heterogeneous IoT gateway based on dynamic priority scheduling algorithm[J]. Transactions of the Institute of Measurement and Control, 2014,36(7): 924-931.
[11]	CONDRY M W , NELSON C B . Using smart edge IoT devices for safer,rapid response with industry IoT control operations[J]. Proceedings of the IEEE, 2016,104(5): 938-946.
[12]	LI F , WAN Z , XIONG X ,et al. Research on sensor-gateway-terminal security mechanism of smart home based on IoT[C]// IoT Workshop 2012,CCIS 312. 2012: 415-422.
[13]	石希, 陈震, 汪东升 ,等. 物联网汇聚安全网关关键技术研究[J]. 信息网络安全, 2012(6): 85-89.
	SHI X , CHEN Z , WANG D S ,et al. A research of the key technology of the aggregative security gateway of Internet of things[J]. Netinfo Security, 2012(6): 85-89.
[14]	SERDAROGLU K C , BAYDERE S . WiSEGATE:wireless sensor network gateway framework for Internet of things[J]. Wireless Networks, 2015,22(5): 1-17.
[15]	罗娟, 顾传力, 李仁发 . 基于角色的无线传感网络中间件研究[J]. 通信学报, 2011,32(1): 79-86.
	LUO J , GU C L , LI R F . Researches on role-based middleware in wireless sensor networks[J]. Journal on Communications, 2011,32(1): 79-86.
[16]	杨光, 耿贵宁, 都婧 ,等. 物联网安全威胁与措施[J]. 清华大学学报(自然科学版), 2011,51(10): 1335-1340.
	YANG G , GENG G N , DU J ,et al. Security threats and measures for the Internet of things[J]. Journal of Tsinghua University (Science and Technology), 2011,51(10): 1335-1340.
[17]	王浩, 郑武, 谢昊飞 ,等. 物联网安全技术[M]. 北京: 人民邮电出版社, 2016: 5-17.
	WANG H , ZHENG W , XIE H F ,et al. IoT security technology[M]. Beijing: Posts ＆ Telecom PressPress, 2016: 5-17.
[18]	ALUR R , DILL D L . A theory of timed automata[J]. Theoretical Computer Science, 1994,126(2): 183-235.
[19]	DAVID A , OLIVER M M . From HUPPAAL to UPPAAL:a translation from hierarchical timed automata to flat timed automata[R]. BRICS Report Series RS-01-11,Department of Computer Science,University of Aarhus, 2001.
[20]	YIN A , WANG S . A novel encryption scheme based on timestamp in gigabit ethernet passive optical network using AES-128[J]. Optik, 2014,125(3): 1361-1365.
[21]	BEHRMANN G , DAVID A , LARSEN K G . A tutorial on UPPAAL[M]// Formal Methods for the Design of Real-Time Systems. Springer Berlin Heidelberg, 2004: 200-236.

名称	说明
通信信道攻击	消息的截取、篡改、重放及注入，攻击者通过长时间占据信道导致合法通信无法传输
拒绝服务攻击	污水池（sinkhole）攻击、虫洞（wormhole）攻击、洪泛攻击等，DoS攻击会耗尽节点资源，使节点丧失运行能力
节点捕获	网关等关键节点被攻击者控制，可能导致通信密钥、广播密钥、配对密钥等被泄露，进而威胁网络的通信安全
假冒攻击	恶意节点假冒合法节点发起女巫（sybil）攻击，利用多身份与其他节点通信，并配合其他攻击手段达到攻击目的
路由协议攻击	通过欺骗、篡改或重发路由信息，攻击者可创建路由循环，形成虚假错误消息，增加端到端时延，耗尽关键节点能源等

状态位置	含义	状态位置	含义
Start	启动安全系统	CheckCategory	检查终端类别
Configuration	读取网关配置信息	Connect	连接感知汇聚节点
Authentication	统一身份认证	ReadCache	解析汇聚节点缓存信息
WaitAC	等待认证信息返回	CheckAP	检查轮询周期完成标识
CheckGS	检查网关状态	UpdateKey	密钥更新
CheckTS	检查终端状态	WaitKMS	等待密钥管理系统工作
IntrusionDetection	入侵检测	SelfMonitoring	发出自组织监控命令
WaitIDS	等待入侵检测系统处理完成	WaitNode	等待节点数据返回
Idle	空闲状态	CheckRF	检查返回标识
Restart	网关重新启动	Clear	清除控制状态
EnterMiddle	进入中间层轮询模块	MonitoringInfo	准备提交监控信息至顶层主模块
WaitData	等待中间层返回监控信息	ReadConInfo	读取执行设备配置信息
CheckData	检查是否有监控信息返回	DeviceControl	发出设备控制命令
Verify	数据是否异常	WaitDevice	等待设备状态返回
WaitHE	等待异常处理	Keep	令设备在合法时间内运行一段时间
DataAnalysis	解析监控信息	RetrieveData	发出取回监控信息命令
Record	记录监控信息或轮询失败的信息	Failure	轮询失败
CheckPolling	当前轮询周期是否完成	End	该逻辑流程结束

同步通道	含义
StartIDS	开始进行入侵检测
FinishIDS	入侵检测完成
StartAC	开始进行身份认证
FinishAC	身份认证完成
StartMiddle	开始执行中间层轮询模块
FinishMiddle	中间层轮询模块执行完成
StartKMS	开始进行密钥管理
FinishKMS	密钥管理完成
HandlingException	开始进行异常处理
Return	异常处理完毕返回
Decryption	解密
DReturn	解密完成
Encryption	加密
EReturn	加密完成

变量	含义
c	全局时钟
x,y,z	KMS时钟，中间层时钟，IDS时钟
Category	类别标识：1-网关，2-感知终端，3-执行终端
GatewayStatus	网关认证合法状态
TerminalStatus	终端认证合法状态
SubmitData	监控信息提交至顶层标识位
AlreadyPolling	轮询周期完成标识位
PollingSuccess	轮询成功标识位
AuthenticationFlag	认证标识
KMSType	密钥管理功能类别：1-更新密钥，2-验证密钥
KeyUpdateFlag	密钥更新标识
KeyVerificationFlag	密钥验证标识
ReturnFlag	返回标识
ExceptionLevel	数据异常等级：0-无异常，1-容错机制，2-人工干预

性质	验证时间/s	内存消耗/KB	验证结果
机密性	0.034	9 096	满足该性质
可用性	0.001	9 116	满足该性质
真实性	0.001	9 116	满足该性质
顽健性	0.060	9 508	满足该性质
完整性	0.034	9 504	满足该性质
新鲜性	0.062	9 516	满足该性质

基于时间自动机的物联网网关安全系统的建模及验证

Modeling and verifying based on timed automata of Internet of things gateway security system

在线阅读

PDF下载

可视化

摘要/Abstract

引用本文

使用本文

图/表 16

参考文献 21

相关文章 15

Metrics

推荐阅读 0

[1]	谭国真,韩国栋,张福新,丁男,刘明剑. 基于网络效用最大化理论的分布式车联网拥塞控制策略[J]. 通信学报, 2019, 40(2): 82-91.
[2]	王舜,杜晔,韩臻,刘吉强. 基于程序局部性引导的有界模型检测优化方法[J]. 通信学报, 2018, 39(3): 181-190.
[3]	杨京,范丹,张玉清. 改进的安全协议自适应分析算法[J]. 通信学报, 2015, 36(Z1): 266-276.
[4]	习宁，马建峰，孙聪，卢笛，张涛. 基于模型检测的服务链信息流安全可组合验证方法[J]. 通信学报, 2014, 35(11): 3-22.
[5]	习宁,马建峰,孙聪,卢笛,张涛. 基于模型检测的服务链信息流安全可组合验证方法[J]. 通信学报, 2014, 35(11): 23-31.
[6]	常德显1,2,3，冯登国1，秦宇1，张倩颖1,2. 基于扩展LS的可信虚拟平台信任链分析[J]. 通信学报, 2013, 34(5): 4-41.
[7]	常德显,冯登国,秦宇,张倩颖. 基于扩展LS²的可信虚拟平台信任链分析[J]. 通信学报, 2013, 34(5): 31-41.
[8]	罗娟,顾传力,李仁发. 基于角色的无线传感网络中间件研究[J]. 通信学报, 2011, 32(1): 79-86.
[9]	陈小峰,冯登国. 可信密码模块的模型检测分析[J]. 通信学报, 2010, 31(1): 59-64.
[10]	郭渊博,刘伟,袁顺,周睿鹏. 容忍入侵的应用服务器结构设计与实现[J]. 通信学报, 2009, 30(10A): 97-102.
[11]	孙纪敏,沈玉龙,孙玉,张思东. 传感器网络接入Internet体系结构和服务提供方法[J]. 通信学报, 2008, 29(4): 85-89.
[12]	晏立,鞠时光,王昌达. 安全信息流的实时监控机制[J]. 通信学报, 2008, 29(10): 51-57.
[13]	黄河,姚淑珍. 基于动态规则的访问控制模型[J]. 通信学报, 2007, 28(11A): 14-17.
[14]	李英壮,张建华,肖永平. Bluetooth-UPnP软件桥的设计[J]. 通信学报, 2006, 27(11A): 273-276.
[15]	苗春雨,史美林,姜进磊. MOM-S：基于Web服务的消息中间件系统[J]. 通信学报, 2006, 27(11): 96-100.