ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2020, Vol. 57 ›› Issue (11): 2312-2327.doi: 10.7544/issn1000-1239.2020.20200399

所属专题: 2020密码学与数据隐私保护研究专题

• 信息安全 • 上一篇    下一篇

工业以太网EtherCAT协议形式化安全评估及改进

冯涛,王帅帅,龚翔,方君丽   

  1. (兰州理工大学计算机与通信学院 兰州 730000) (fengt@lut.cn)
  • 出版日期: 2020-11-01
  • 基金资助: 
    国家自然科学基金项目(61462060,61762060)

Formal Security Evaluation and Improvement of Industrial Ethernet EtherCAT Protocol

Feng Tao, Wang Shuaishuai, Gong Xiang, Fang Junli   

  1. (Department of Computer and Communication, Lanzhou University of Technology, Lanzhou 730000)
  • Online: 2020-11-01
  • Supported by: 
    This work was supported by the National Natural Science Foundation of China (61462060, 61762060).

摘要: EtherCAT协议由于具有较高的实时性和较强的性能而被广泛应用,但是随着工业以太网协议的快速发展和开放化,使得工业控制系统承受着巨大的网络攻击风险.目前有许多对工业以太网协议安全和改进的研究,但是这些研究缺乏对协议的形式化建模与安全评估,只注重协议本身安全功能的实现,有一定的局限性.为了解决工业以太网受到攻击的现状,将当前应用较多的EtherCAT协议作为研究对象,提出了一种基于有色Petri网理论和Dolev-Yao攻击方法的模型检测方法,对协议进行了安全性评估与改进.首先基于Petri网理论和CPN Tools模型工具对协议的安全机制FSoE进行了一致性验证;然后引入了Dolev-Yao攻击模型对协议的原始模型进行安全性评估,发现协议存在着篡改、重放和欺骗3类中间人攻击漏洞;最后针对协议存在的漏洞提出了一种新方案,对原协议加入了秘钥分发中心和Hash函数,再次利用CPN模型检测工具对新方案进行了安全性验证.通过验证可以发现新方案能够有效防止3类中间人攻击,提高协议的安全性.

关键词: EtherCAT协议, FSoE, CPN, Dolev-Yao, 安全评估, 安全性验证

Abstract: The EtherCAT protocol is widely used due to its high real-time performance and strong performance. However, with the rapid development and openness of the Industrial Ethernet protocol, industrial control systems are subject to huge network attack risks. There are many studies on the security and improvement of industrial Ethernet protocols, but these studies lack formal modeling and security evaluation of the protocol, and only focus on the realization of the security function of the protocol itself, which has certain limitations. In order to solve the current situation of industrial Ethernet being attacked, we take EtherCAT protocol which is widely used at present as the research object, and propose a model checking method based on colored Petri net theory and Dolev-Yao attack method, and evaluate and improve the security of the protocol. First, we verify the security mechanism of the protocol FSoE based on Petri net theory and CPN Tools model tools; then introduce the Dolev-Yao attack model to evaluate the security of the original model of the protocol. It is found that there are 3 types of man-in-the-middle attack vulnerabilities in the protocol, including tampering, replay, and deception. Finally, a new solution is proposed for the vulnerabilities in the protocol. A key distribution center and a Hash function are added to the original protocol. The security verification of the new scheme is carried out again using the CPN model detection tool. Through verification, it can be found that the new scheme can effectively prevent 3 types of man-in-the-middle attacks and improve the security of the protocol.

Key words: EtherCAT, FSoE, CPN, Dolev-Yao, security evaluation, security verification

中图分类号: