信息网络安全

信息网络安全 ›› 2019, Vol. 19 ›› Issue (11): 71-81.doi: 10.3969/j.issn.1671-1122.2019.11.010

• 技术研究 • 上一篇    下一篇

基于时间自动机的工业控制系统网络安全风险分析

吕宗平1, 丁磊1,2, 隋翯1,3(), 顾兆军1,2   

  1. 1.中国民航大学信息安全测评中心,天津 300300
    2.中国民航大学计算机科学与技术学院,天津 300300
    3.中国民航大学航空工程学院,天津 300300
  • 收稿日期:2019-08-10 出版日期:2019-11-10 发布日期:2020-05-11
  • 作者简介:

    作者简介：吕宗平（1964—）,男,湖北,研究员,硕士,主要研究方向为网络与信息安全、民航信息系统;丁磊（1995—）,男,天津,硕士研究生,主要研究方向为工业控制系统网络与信息安全;隋翯（1987—）,男,吉林,讲师,博士,主要研究方向为工业控制系统网络与信息安全;顾兆军（1966—）,男,山东,教授,博士,主要研究方向为网络与信息安全、民航信息系统。

  • 基金资助:
    国家自然科学基金[61601467,U1533104];民航科技基金[MHRD20140205,MHRD20150233];民航安全能力建设基金[PESA170003,PESA2018079,PESA2018082,PESA2019073,PESA2019074]

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

Zongping LV1, Lei DING1,2, He SUI1,3(), Zhaojun GU1,2   

  1. 1. Information Security Evaluation Center, Civil Aviation University of China, Tianjin 300300, China
    2. College of Computer Science and Technology, Civil Aviation University of China, Tianjin 300300, China
    3. College of Aeronautical Engineering,Civil Aviation University of China, Tianjin 300300, China
  • Received:2019-08-10 Online:2019-11-10 Published:2020-05-11

RichHTML

6

PDF (PC)

100

摘要：

随着工业控制系统开放性增强,大量工业控制协议漏洞暴露在互联网上,造成了工业控制系统安全风险急剧上升。文章针对工业控制系统中最常用的Modbus协议,以典型灌装环节为例,提出了一种基于时间自动机的工业控制系统网络安全分析方法,并对针对Modbus协议的中间人攻击进行了形式化分析和验证。首先结合灌装生产业务流程,归纳了该控制系统网络结构、安全属性和面临的安全威胁;然后对该控制系统的状态、行为、安全策略和攻击行为进行时间自动机建模,并通过时钟同步将各模型连接成网络;最后利用UPPAAL工具编写安全属性公式,并对有无攻击两种情况下的安全属性进行验证。实验结果表明,针对Modbus协议的中间人攻击成功破坏了该控制系统的完整性和可用性。

关键词: 工业控制系统, 形式化分析, 时间自动机, Modbus协议, UPPAAL

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

中图分类号: