Network Security Risk Analysis of Industrial Control System Based on Time Automata

doi:10.3969/j.issn.1671-1122.2019.11.010

Abstract

Abstract:

With the increasing openness of industrial control system, a large number of industrial control protocol vulnerabilities are exposed on the Internet, causing a sharp rise in industrial control system security risks. In this paper, a network security analysis method of industrial control system based on time automata is proposed based on the Modbus protocol, which is the most commonly used Modbus protocol in industrial control system. Firstly, the network structure, safety attributes and security threats of the control system are summarized according to the filling production process. Then, the state, behavior, security policy and attack behavior of the control system are modeled by time automata, and the models are connected into a network by clock synchronization. Finally, the UPPAAL tool is used to write the security attribute formula, and the security attribute is verified in two cases with or without attack. The comparison of experimental results shows that the man-in-the-middle attack against Modbus protocol successfully destroys the integrity and availability of the control system.

Key words: industrial control system, formal analysis, time automaton, Modbus protocol, UPPAAL

CLC Number:

TP309

Zongping LV, Lei DING, He SUI, Zhaojun GU. Network Security Risk Analysis of Industrial Control System Based on Time Automata[J]. Netinfo Security, 2019, 19(11): 71-81.

Figures/Tables 22

References 23

[1]	PENG Yong, JIANG Changqing, XIE Feng, et al.Research Progress on Information Security of Industrial Control System[J]. Journal of Tsinghua University(Natural Science Edition), 2012, 52(10): 1396-1408.
	彭勇,江常青,谢丰,等.工业控制系统信息安全研究进展[J].清华大学学报:自然科学版,2012,52(10):1396-1408.
[2]	ERIC D K.Industrial Network Security: Securing Critical Infrastructure Networks for Smart Grid, SCADA, and Other Industrial Control Systems[M]. ZHOU Qin, GUO Bingyi, HE Huimin, et al. Beijing: National Defense Industry Press, 2014.
	Eric D K. 工业网络安全——智能电网,SCADA和其他工业控制系统等关键基础设施的安全[M].周秦,郭冰逸,贺惠民,等,译.北京:国防工业出版社,2014.
[3]	CHEMINOD M, DURANTE L, VALENZANO A.Review of Security Issues in Industrial Networks[J]. IEEE Transactions on Industrial Informatics, 2013, 9(1): 277-293.
[4]	YANG An, SUN Limin, WANG Xiaoshan, et al.Overview of Intrusion Detection Technologies for Industrial Control Systems[J]. Computer Research and Development, 2016, 53(9): 2039-2054.
	杨安,孙利民,王小山,等.工业控制系统入侵检测技术综述[J].计算机研究与发展,2016,53(9):2039-2054.
[5]	ZHOU Jian, CHEN Jie.Construction of Integration Evaluation Index System for Manufacturing Enterprises[J]. Computer Integrated Manufacturing System, 2013, 19(9): 2251-2263.
	周剑,陈杰.制造业企业两化融合评估指标体系构建[J].计算机集成制造系统,2013,19(9):2251-2263.
[6]	The State Council. Made in China 2025[EB/OL]. .
	国务院.中国制造2025[EB/OL]. .
[7]	LIANG Xiujing.TSMC Virus Event: Information Security of Manufacturing Industry is Urgent[J]. Automation Expo, 2008, 35(8): 5.
	梁秀璟. 台积电病毒事件:制造业信息安全刻不容缓[J].自动化博览,2018,35(8):5.
[8]	WANG Huanhuan.Research on Vulnerability Scanning Technology of Industrial Control System[D]. Beijing: Beijing University of Posts and Telecommunications, 2015.
	王欢欢. 工控系统漏洞扫描技术的研究[D].北京:北京邮电大学,2015.
[9]	GA/T 1390A/T 1390.5-2017. Basic Requirements for Network Security Level Protection of Information Security Technology-part 5: Safety Extension Requirements for Industrial Control Systems[S]. Beijing: Standards Press of China, 2018.
	GA/T 1390A/T 1390.5-2017.信息安全技术网络安全等级保护基本要求第5部分:工业控制系统安全扩展要求[S].北京:中国标准出版社,2018.
[10]	WANG Ji, ZHAN Naijun, FENG Xinyu, et al.Overview of Formal Methods[J]. Journal of Software, 2019, 30(1): 33-61.
	王戟,詹乃军,冯新宇,等.形式化方法概貌[J].软件学报,2019,30(1):33-61.
[11]	WANG Yongjie, XIAN Ming, LIU Jin, et al.Research on Network Security Evaluation Based on Attack Graph Model[J]. Journal of Communications, 2007(3): 29-34.
	王永杰,鲜明,刘进,等.基于攻击图模型的网络安全评估研究[J].通信学报,2007(3):29-34.
[12]	WAN Danmei.Random Model Method and Evaluation Technology of Network Security[J]. Journal of Science and Technology Innovation, 2008, 15(30): 85-87.
	万丹梅. 网络安全的随机模型方法与评价技术[J].科技创新导报,2018,15(30):85-87.
[13]	HAN Deshuai, YANG Qiliang, XING Jianchun.A Software Adaptive UML Modeling and Its Formal Verification Method[J]. Journal of Software, 2015, 26(4): 730-746.
	韩德帅,杨启亮,邢建春.一种软件自适应UML建模及其形式化验证方法[J].软件学报,2015,26(4):730-746.
[14]	GAO Mengzhou, FENG Dongqin, LING Congli, et al.Vulnerability Analysis of Industrial Control System Based on Attack Graph[J]. Journal of ZheJiang University(Engineering Edition), 2014, 48(12): 2123-2131.
	高梦州,冯冬芹,凌从礼,等.基于攻击图的工业控制系统脆弱性分析[J].浙江大学学报:工学版,2014,48(12):2123-2131.
[15]	WANG Dejin, JIANG Changqing, PENG Yong.Security Domain based Attack Graph Generation on Industrial Control System[J]. Journal of Tsinghua University(Natural Science Edition), 2014, 54(1): 44-52.
	王得金,江常青,彭勇.工业控制系统上基于安全域的攻击图生成[J].清华大学学报:自然科学版,2014,54(1):44-52.
[16]	HUANG Jiahui, FENG Dongqin, WANG Hongjian.Vulnerability Quantification Method of Industrial Control System Based on Attack Graph[J]. Journal of Automation, 2016, 42(5): 792-798.
	黄家辉,冯冬芹,王虹鉴.基于攻击图的工控系统脆弱性量化方法[J].自动化学报,2016,42(5):792-798.
[17]	HUANG Huiping, XIAO Shide, MENG Xiangyin.Information Security Risk Assessment of Industrial Control System Based on Attack Tree[J]. Computer Application Research, 2015, 32(10): 3022-3025.
	黄慧萍,肖世德,孟祥印.基于攻击树的工业控制系统信息安全风险评估[J].计算机应用研究,2015,32(10):3022-3025.
[18]	KUMAR R, MARIELLE S. QuantitativeSecurity and Safety Analysis with Attack-Fault Trees[EB/OL]. , 2019-2-11.
[19]	PUYS M, POTET M L, KHALED A.Generation of Applicative Attacks Scenarios Against Industrial Systems[C]//Springer. International Symposium on Foundations and Practice of Security, October 23-25, 2017, Nancy, France. Heidelberg: Springer, 2017: 127-143.
[20]	SU Qi, WANG Ting, CHEN Tieming, et al. CPS Security Modeling and Verification Based on Time Automata[EB/OL]. , 2019-2-11.
	苏琪,王婷,陈铁明,等.基于时间自动机的CPS安全建模和验证[EB/OL]. , 2019-2-11.
[21]	LI Lixing, JIN Zhi, LI Ge.Modeling and Validation of Internet of Things Service Based on Time Automata[J]. Journal of Computer Science, 2011, 34(8): 1365-1377.
	李力行,金芝,李戈.基于时间自动机的物联网服务建模和验证[J].计算机学报,2011,34(8):1365-1377.
[22]	WANG Guoqing, ZHUANG Lei, WANG Ruimin, et al.Modeling and Verification of Internet of Things Gateway Security System Based on Time Automata[J]. Journal of Communications, 2018, 39(3): 63-75.
	王国卿,庄雷,王瑞民,等.基于时间自动机的物联网网关安全系统的建模及验证[J].通信学报,2018,39(3):63-75.
[23]	PENG Dayan, BU Bing.Modeling and Verification of Typical Operation Scenarios of FAO System Based on UPPAAL[J]. Journal of Railway Science, 2013, 35(6): 65-71.
	彭大天,步兵.基于UPPAAL的FAO系统典型运营场景建模与验证[J].铁道学报,2013,35(6):65-71.

安全属性	安全条件	说明
完整性	1）	确保控制策略和链路完整,任何情况下都有可执行的控制命令,不产生控制死锁
可用性	2）、3）、4）	确保整个控制命令符合实际生产逻辑,可执行
保密性	5）、6）	确保可同步验证数据来源节点的密钥,认证身份具有合法性

名称	说明
复制	允许攻击者将指令存储到其本身的内存中
拦截	允许攻击者拦截工程师站与服务器在信道上发送的指令
伪造	允许攻击者创建新指令
篡改	允许攻击者篡改被截获的指令
重放	允许攻击者将指令重放到网络中
解密	允许攻击者从内存中检索解密密钥

名称	时间自动机模型	作用
Client-Communication	工程师站通信模型	描述工程师站与Modbus服务器交互通信的状态迁移
Client-Behavior	工程师站行为模型	描述Modbus行为服务器状态迁移
Modbus_Server-Communication	Modbus服务器通信模型	描述Modbus服务器与上位机和下位机交互通信状态迁移
Modbus_Server- Behavior	Modbus服务器行为模型	描述Modbus服务器接收、下发指令行为状态迁移
OPC_Server-Communication	OPC服务器通信模型	描述OPC服务器与上位机和下位机交互通信状态迁移
OPC_Server- Behavior	OPC服务器行为模型	描述OPC服务器接收、下发指令行为状态迁移
Conveyor	传送带模型	描述传送带工作状态迁移
Nozzle	灌装喷嘴模型	描述灌装喷嘴工作状态迁移
Arm_One	机械臂1模型	描述机械臂1工作状态迁移
Arm_Two	机械臂2模型	描述机械臂2工作状态迁移
PositionSensor_One	位置传感器1模型	描述位置传感器1状态迁移
PositionSensor_Two	位置传感器2模型	描述位置传感器2状态迁移
Level	液位监测器模型	描述液位检测器工作状态迁移
Security	安全策略模型	描述系统安全状态迁移
Attack	攻击模型	描述攻击行为状态迁移

指令	作用
Begin_or_Stop	打开/关闭Client-Behavior
Modbus_CtoS/Modbus_StoC	Client-Communication与Modbus_Server-Communication交互通信
OPC_CtoS/OPC_StoC	Client-Communication与OPC_Server-Communication互相通信
Modbus_On/ Modbus_Off	打开/关闭Modbus_Server- Behavior
OPC_On/OPC_Off	打开/关闭OPC_Server- Behavior
Conveyor_On/Conveyor_Off	打开/关闭Conveyor
Nozzle_On/ Nozzle_Off	打开/关闭Nozzle
Arm_One_On/ Arm_One_Off	打开/关闭机械臂1
Arm_Two_On/ Arm_Two_Off	打开/关闭机械臂2
Sign	数字签名
Check_Sign	检查数字签名
Sign_Crypt	数字签名加密
Decrypt	解密
Signal_1	设备交互通信
Signal_2	设备交互通信

状态	含义
idle	起始状态
client_behavior_on_off	Client-Behavior开启/关闭状态
modbus_ctos	Client-Communication与Modbus_Server-Communication建立通信状态
modbus_stoc	Modbus_Server-Communication与Client-Communication建立通信状态
opc_ctos	Client-Communication与OPC_Server-Communication建立通信状态
opc_stoc	OPC_Server-Communication与Client-Communication建立通信状态
sign	执行数字签名完毕状态
check_sign	完成检查签名操作状态
check_false/ check_true	签名错误/签名正确
on/ off	Client-Behavior开启/关闭状态
check_msg	检查读/写操作状态
read/ write	检查读/写操作完毕状态
modbus_server	Modbus_Server状态
nozzle	罐装喷嘴状态
sensor_1	位置传感器1工作/未工作状态
sensor _2	位置传感器2工作/未工作状态
level	液位监测器罐装完成/罐装未完成状态
conveyor	传送带工作/未工作状态
arm_1	机械臂1状态
arm_2	机械臂2状态
modbus_server_on	Modbus服务器启动状态
modbus_server_off	Modbus服务器关闭状态
opc_run	OPC服务器状态
opc_server_on/opc_server_off	OPC服务开启/关闭器状态
decrypt	解密完毕状态
sign_crypt	数字签名加密完毕状态
out/in	瓶子处于/未处于位置传感器状态
full/filling	监测液体灌满/未灌满状态
Arm_stop/Arm_work	机械臂工作/未作状态
conveyor_on/ conveyor_off	传送带工作/未工作状态
arm_1_on/arm_1_off	机械臂1工作/未工作状态
nozzle_on/nozzle_off	罐装喷嘴工作/未工作状态