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

Formal Security Evaluation and Improvement of Industrial Ethernet EtherCAT Protocol

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

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.