馮 濤 王帥帥 龔 翔 方君麗

(蘭州理工大學(xué)計(jì)算機(jī)與通信學(xué)院 蘭州 730000)(fengt@lut.cn)

傳統(tǒng)的工業(yè)控制系統(tǒng)隨著工業(yè)大數(shù)據(jù)[1]和物聯(lián)網(wǎng)[2]的迅猛發(fā)展，變得更加互聯(lián)互通，大量的以太網(wǎng)協(xié)議被應(yīng)用到工業(yè)控制系統(tǒng)中，工業(yè)以太網(wǎng)協(xié)議在其中扮演著重要角色[3].但是由于工業(yè)控制系統(tǒng)在設(shè)計(jì)之初是封閉隔離的，所以大多協(xié)議未采用加密認(rèn)證等信息安全手段[4]，使得攻擊者能夠很容易對數(shù)據(jù)進(jìn)行監(jiān)聽、篡改和竊取等，從而達(dá)到破壞系統(tǒng)的目的[5-6].隨著控制系統(tǒng)的網(wǎng)絡(luò)化發(fā)展以及工業(yè)協(xié)議的開放化，協(xié)議暴露出許多安全隱患，因此需要重點(diǎn)對協(xié)議的安全性進(jìn)行研究.

本文的主要貢獻(xiàn)包括3個(gè)方面:

1) 提出了一種基于有色Petri網(wǎng)理論和Dolev-Yao攻擊方法的模型檢測方法;

2) 對EtherCAT協(xié)議的安全機(jī)制進(jìn)行了詳細(xì)分析，利用建模工具對協(xié)議進(jìn)行了建模，并且驗(yàn)證了模型一致性.引入Dolev-Yao攻擊者模型對協(xié)議進(jìn)行了安全評估，發(fā)現(xiàn)協(xié)議存在的漏洞;

3) 對協(xié)議存在的漏洞提出了相應(yīng)的新方案，并對新方案進(jìn)行了安全性驗(yàn)證.

1 相關(guān)工作

對協(xié)議進(jìn)行安全評估一般使用的是形式化分析方法，包括模型檢測方法、定理證明方法、類型檢測方法以及模態(tài)邏輯方法等.文獻(xiàn)[7]分析的模態(tài)邏輯方法雖然能夠?qū)Π踩珔f(xié)議進(jìn)行建模和驗(yàn)證，但是該方法抽象度過高，無法對協(xié)議交互的細(xì)節(jié)進(jìn)行描述，無法展現(xiàn)協(xié)議運(yùn)行的整體過程.文獻(xiàn)[8]中分析了定理證明方法能夠不限制協(xié)議的運(yùn)行次數(shù)，但是不能夠?qū)崿F(xiàn)自動化.文獻(xiàn)[9]中指出類型檢測方法能夠得出安全協(xié)議的結(jié)論，但是不能表現(xiàn)出攻擊序列.基于模型檢測的安全評估方法，能夠?qū)f(xié)議的行為進(jìn)行安全建模，但是面臨狀態(tài)爆炸問題.針對于EtherCAT協(xié)議的安全研究，文獻(xiàn)[10]通過基于機(jī)器學(xué)習(xí)的異常檢測方法對EtherCAT進(jìn)行了分析，發(fā)現(xiàn)該方法不僅能夠進(jìn)行異常檢測，還可以標(biāo)記攻擊類型，但是未給出相應(yīng)的改進(jìn)方案；文獻(xiàn)[11]中通過建立面向數(shù)據(jù)流的模型對EtherCAT進(jìn)行分析，發(fā)現(xiàn)該方法能夠?qū)f(xié)議進(jìn)行直觀、準(zhǔn)確的圖形表示，并且能夠驗(yàn)證協(xié)議的正確性，但是建模效率較低，一旦出錯(cuò)就得重新建模.

綜上所述，目前已有的對工業(yè)以太網(wǎng)協(xié)議安全研究的工作大多集中在協(xié)議自身安全功能的實(shí)現(xiàn)，對協(xié)議的安全評估還處于起步階段，針對工業(yè)以太網(wǎng)協(xié)議安全評估模型的建立，以及攻擊者模型的建立，存在一定的問題.本文針對EtherCAT協(xié)議中的安全機(jī)制FSoE進(jìn)行重點(diǎn)研究，以文獻(xiàn)[12]中的有色Petri網(wǎng)理論和Dolev-Yao攻擊方法為指導(dǎo)，利用建模工具CPN Tools對協(xié)議進(jìn)行安全評估，挖掘協(xié)議漏洞，提出新的改進(jìn)方案，并且對新方案進(jìn)行安全性驗(yàn)證.

相比已有的研究工作，本文提出了基于有色Petri網(wǎng)理論和Dolev-Yao攻擊方法的模型檢測方法對協(xié)議進(jìn)行安全分析；對協(xié)議的模型進(jìn)行一致性驗(yàn)證，并且引入攻擊者模型對協(xié)議進(jìn)行安全評估；對協(xié)議安全評估的結(jié)果，提出針對性的新方案，并對新方案進(jìn)行安全性驗(yàn)證.

2 相關(guān)理論

2.1 EtherCAT及其運(yùn)行原理

EtherCAT協(xié)議是由EtherCAT技術(shù)集團(tuán)(ETG)支持[13]的一種流行的實(shí)時(shí)工業(yè)以太網(wǎng)，該協(xié)議使用了以太網(wǎng)標(biāo)準(zhǔn)IEEE802.3的物理層和鏈路層，并且由Beckhoff定義.它是一種開放的實(shí)時(shí)以太網(wǎng)通信技術(shù)協(xié)議，具有高速低延時(shí)、適用性強(qiáng)、符合以太網(wǎng)標(biāo)準(zhǔn)、刷新周期短、同步性能好等特點(diǎn)，支持多種網(wǎng)絡(luò)連接拓?fù)浣Y(jié)構(gòu).

EtherCAT協(xié)議的工作原理如圖1所示,Ether-CAT主從站之間的交互行為是由主站主動發(fā)起的，主站通過標(biāo)準(zhǔn)的以太網(wǎng)數(shù)據(jù)幀的形式將EtherCAT數(shù)據(jù)幀發(fā)送給從站，報(bào)文在經(jīng)過每個(gè)從站時(shí)，從站對報(bào)文中與自己相關(guān)的數(shù)據(jù)信息進(jìn)行相應(yīng)處理，在報(bào)文的指定位置進(jìn)行數(shù)據(jù)的讀寫，并且對計(jì)數(shù)器信息WKC(working counter)進(jìn)行加1操作來表示從站對報(bào)文進(jìn)行了處理，然后將數(shù)據(jù)幀傳輸?shù)较乱粋€(gè)從站節(jié)點(diǎn)，經(jīng)過最后一個(gè)從站節(jié)點(diǎn)的處理后進(jìn)行返回，最終通過第1個(gè)節(jié)點(diǎn)返回到主站[14-16].

Fig. 1 The operation principle of EtherCAT protocol

2.2 安全機(jī)制FSoE簡介

現(xiàn)代通信系統(tǒng)不僅要實(shí)現(xiàn)控制數(shù)據(jù)的確定傳輸，還要在相同的介質(zhì)中進(jìn)行安全關(guān)鍵控制數(shù)據(jù)的傳輸.

EtherCAT使用FSoE(fail safe over EtherCAT)機(jī)制來實(shí)現(xiàn)該目的.EtherCAT安全技術(shù)是基于IEC 61508開發(fā)的，由TüV認(rèn)證，并符合IEC 61784-3標(biāo)準(zhǔn).該協(xié)議可支持功能安全等級SIL 3的安全應(yīng)用場合.安全數(shù)據(jù)幀可被看作一個(gè)“安全容器”，其中包含了安全關(guān)鍵過程數(shù)據(jù)以及一些用于保證數(shù)據(jù)安全性的額外信息[17].

安全數(shù)據(jù)幀如圖2所示，其至少可以傳輸1B的安全數(shù)據(jù)(Safedata)，也可以傳輸1 B或2 B倍數(shù)的Safedata，每2 B的Safedata被2 B的CRC校驗(yàn).Safedata的長度在FSoE從屬安全設(shè)備描述中定義，其最大數(shù)量不受協(xié)議的限制；CRC校驗(yàn)結(jié)果包括4種因素，分別為最后接收到的FSoE幀的CRC、傳輸數(shù)據(jù)(ConnlD,CMD,Data)、CRC的索引以及會話ID；其中的連接ID指示FSoE主節(jié)點(diǎn)和FSoE從節(jié)點(diǎn)之間的連接，它應(yīng)該是系統(tǒng)中唯一的連接ID，必須在配置中進(jìn)行檢查.

Fig. 2 Data frame structure of FSoE

2.3 CPN及建模工具

Petri網(wǎng)的概念是由德國科學(xué)家Carl Adam Petri最早提出的，后來出現(xiàn)了許多擴(kuò)展的概念，例如時(shí)間Petri網(wǎng)、隨機(jī)Petri網(wǎng)、CPN等[18-20].形式化建模工具CPN Tools具有編輯、模擬、狀態(tài)空間分析和性能分析等特性，而且能夠通過回饋機(jī)制對產(chǎn)生的錯(cuò)誤進(jìn)行精準(zhǔn)定位.CPN建模能夠進(jìn)行增量語法檢查及代碼生成，在一定程度上保證了模型的正確性.該工具是由丹麥奧胡斯大學(xué)基于Design/CPN開發(fā)的，使用良好的人機(jī)界面技術(shù)對用戶圖形界面(GUI)進(jìn)行了設(shè)計(jì)，不僅能夠?qū)τ猩玃etri網(wǎng)進(jìn)行編輯、模擬和分析，而且支持時(shí)間CPN和分層CPN，借助CPN工具，用戶不僅可以輕松建模，還可以仿真和分析并行系統(tǒng)[21-22].

3 EtherCAT協(xié)議建模

在創(chuàng)建大型的、比較復(fù)雜的Petri網(wǎng)時(shí)，用傳統(tǒng)的CPN模型是比較麻煩的，我們基于模塊編程化思想，利用CPN建模工具內(nèi)的替代變遷的概念可以將CPN網(wǎng)絡(luò)結(jié)構(gòu)拆分成多個(gè)小塊.具有替代變遷的網(wǎng)絡(luò)是多層次的網(wǎng)絡(luò)，我們可以先從廣義上建立一個(gè)簡化的網(wǎng)絡(luò)模型，然后再利用高層次中的替代變遷關(guān)聯(lián)到更為詳細(xì)的子頁面中去，這樣可以逐步細(xì)化自己的模型.

工業(yè)以太網(wǎng)的協(xié)議模型一般由3個(gè)部分組成，分別為發(fā)送端、接收端和中間的通信網(wǎng)絡(luò)，但是一般用于工業(yè)上的協(xié)議通信都比較復(fù)雜，建立傳統(tǒng)的模型可重用性較低，而且不能很好地表現(xiàn)其功能，利用分層建模的方法可以降低復(fù)雜度，本文將協(xié)議建模劃分為頂層、中層和底層3個(gè)層次.

3.1 EtherCAT協(xié)議消息流模型

EtherCAT主從站之間存在2種通信模式，分別為過程數(shù)據(jù)通信和郵箱數(shù)據(jù)通信.EtherCAT使用安全機(jī)制FSoE來保證協(xié)議的安全性，該安全機(jī)制使用了過程數(shù)據(jù)通信模式，如圖3所示為其信息的傳輸過程.

1) 主站發(fā)起會話連接請求，請求信息包括主站地址、從站地址以及會話連接ID.

2) 從站處理接收到的信息，如果連接成功，則回復(fù)連接成功消息和連接ID，如果失敗，則進(jìn)行重置操作.

3) 主從站成功建立連接后，進(jìn)行安全數(shù)據(jù)傳輸，主站將安全數(shù)據(jù)進(jìn)行分段處理，拆分為多個(gè)字節(jié)，然后對拆分后的安全數(shù)據(jù)分別進(jìn)行本地CRC校驗(yàn)，最后將安全數(shù)據(jù)、CRC校驗(yàn)數(shù)據(jù)、命令信息、連接ID和計(jì)數(shù)器信息一并發(fā)給從站.

4) 從站接收到數(shù)據(jù)后，會將安全數(shù)據(jù)在本地進(jìn)行CRC校驗(yàn)，然后與接收到的校驗(yàn)數(shù)據(jù)進(jìn)行對比，如果相同則進(jìn)行相應(yīng)的命令操作，然后將計(jì)數(shù)器信息加1后，回復(fù)主站計(jì)數(shù)信息；如果不同，則進(jìn)行重置操作.

Fig. 3 Message flow model of EtherCAT protocol

3.2 EtherCAT協(xié)議的CPN模型建立

本文將Ethernet協(xié)議的安全機(jī)制FSoE的主從站交互過程進(jìn)行具體建模，該安全機(jī)制使用的是過程數(shù)據(jù)通信模式.

EtherCAT協(xié)議的頂層CPN模型如圖4所示，頂層模型從整體上模擬了協(xié)議的會話過程，包括協(xié)議的通信雙方、通信網(wǎng)絡(luò)以及傳輸信息.圖4中雙線矩形代表替代變遷，橢圓代表消息庫所，通信的主站用替代變遷Master表示，通信從站用替代變遷Slave表示，通信網(wǎng)絡(luò)用替代變遷NET表示.

協(xié)議的中層模型由5個(gè)替代變遷和9個(gè)庫所組成，如圖5所示.主站向從站發(fā)起建立連接信息的過程由替代變遷Connection表示；從站對主站的連接信息進(jìn)行處理和回復(fù)的過程由替代變遷Connection′表示；主站向從站發(fā)送安全數(shù)據(jù)的過程由替代變遷Safedata表示；從站對安全數(shù)據(jù)處理和回復(fù)的過程由Safedata′表示.

Fig. 4 Top level model of EtherCAT protocol

Fig. 5 Middle level model of EtherCAT protocol

Fig. 6 Internal model of alternative transition Connection

EtherCAT協(xié)議的底層模型包括5個(gè)部分，我們按照協(xié)議主從站整體的交互順序，依次對會話連接過程和安全數(shù)據(jù)傳輸過程做詳細(xì)介紹.圖6對替代變遷Connection的內(nèi)部模型進(jìn)行了詳細(xì)描述.變遷Conn_MAC將主站地址信息Mac_M和從站地址信息Mac_S合并成地址信息，變遷Combination將地址信息和連接ID合并為連接請求信息，通過庫所Send_conn發(fā)送到從站；從站回復(fù)的確認(rèn)信息由庫所Rec_ConnID進(jìn)行接收，確認(rèn)信息通過變遷R_ConnID進(jìn)行處理，然后將連接ID通過庫所ConnID發(fā)送給安全數(shù)據(jù).

圖7對替代變遷NET的內(nèi)部模型進(jìn)行了詳細(xì)描述.變遷Transmit_conn和Transmit ConnID分別模擬了在建立連接過程中，主站向從站發(fā)起連接請求信息的傳輸路徑以及從站向主站回復(fù)信息的傳輸路徑；同樣在安全數(shù)據(jù)傳輸過程中，主站向從站發(fā)送安全數(shù)據(jù)的傳輸路徑和從站向主站回復(fù)計(jì)數(shù)信息的傳輸路徑由變遷Transmit Safedata和Transmit WKC表示.

圖8對替代變遷Connection′的內(nèi)部模型進(jìn)行了詳細(xì)描述.庫所Rec_conn用來接收主站發(fā)送的連接信息，變遷R_conn message對接收到的信息進(jìn)行處理，然后將接收到的消息存儲到庫所ReceiveMAC中，變遷Reply將連接ID信息和確認(rèn)信息進(jìn)行整合，通過庫所Send_ConnID發(fā)送給主站，如果連接失敗則從站會進(jìn)行重置操作.

Fig. 7 Internal model of alternative transition NET

Fig. 8 Internal model of alternative transition Connection′

Fig. 9 Internal model of alternative transition Safedata

Fig. 10 Internal model of alternative transition Safedata′

圖9對替代變遷Safedata的內(nèi)部模型進(jìn)行了詳細(xì)描述.變遷CRCdata首先對安全數(shù)據(jù)進(jìn)行本地的CRC校驗(yàn)，然后將安全數(shù)據(jù)和CRC檢驗(yàn)數(shù)據(jù)進(jìn)行合并；變遷Combination′將接收到的確認(rèn)連接ID信息、CMD命令信息和計(jì)數(shù)信息WKC進(jìn)行合并；最后這些數(shù)據(jù)由庫所Safeoutput一并發(fā)送給從站；計(jì)數(shù)器WKC的更新信息由庫所Rec_WKC進(jìn)行接收.

圖10對替代變遷Safedata′的內(nèi)部模型進(jìn)行了詳細(xì)描述.庫所Safeinput用來接收主站發(fā)送的安全數(shù)據(jù)信息，變遷Safe_Message將接收的安全數(shù)據(jù)信息進(jìn)行分解，從站對安全數(shù)據(jù)進(jìn)行本地的CRC校驗(yàn)，然后與接收到的CRC校驗(yàn)數(shù)據(jù)進(jìn)行對比，如果相同則按照接收到的命令信息進(jìn)行操作，并將接收到的計(jì)數(shù)信息加1，由庫所Send_WKC返回給主站.如果本地生成的CRC檢驗(yàn)值與接收到的校驗(yàn)數(shù)據(jù)不同，則進(jìn)行重置操作.

3.3 EtherCAT模型一致性驗(yàn)證

我們將對建議的原始EtherCAT協(xié)議的CPN模型進(jìn)行一致性驗(yàn)證，使用了狀態(tài)空間[23]分析工具.首先我們對所建立的模型給出了預(yù)期結(jié)果，模型會成功進(jìn)行會話連接和安全數(shù)據(jù)傳輸，整個(gè)交互過程中不會產(chǎn)生重置操作.通過對表1的狀態(tài)空間結(jié)果分析，可以發(fā)現(xiàn)狀態(tài)空間節(jié)點(diǎn)、有向弧與強(qiáng)連通節(jié)點(diǎn)、強(qiáng)連通弧的數(shù)目相同，說明我們建立的原始模型不存在導(dǎo)致狀態(tài)無限循環(huán)和迭代行為，所有狀態(tài)節(jié)點(diǎn)都是可達(dá)的；主狀態(tài)節(jié)點(diǎn)和活變遷為0，說明原始模型沒有始終處于激活狀態(tài)的活變遷，同時(shí)也不存在任意可達(dá)的狀態(tài)；死節(jié)點(diǎn)為1，表示全部請求都被從站執(zhí)行；存在2個(gè)死變遷Reset和Reset1，變遷Reset是用來表示連接失敗后的重置操作，變遷Reset1是表示數(shù)據(jù)傳輸過程中CRC校驗(yàn)失敗后的重置操作，這2個(gè)變遷均為死變遷說明模型不存在連接失敗和數(shù)據(jù)傳輸失敗的情況，與預(yù)期結(jié)果一致.

Table 1 State Space Analysis of the Original Model of EtherCAT Protocol

4 基于攻擊者安全評估模型

Dolev和Yao發(fā)表了一篇重要論文，其對協(xié)議安全研究發(fā)展產(chǎn)生了深刻的影響[24].該論文的主要觀點(diǎn)就是在假設(shè)密碼系統(tǒng)是“完美”的基礎(chǔ)上只討論協(xié)議本身的安全屬性，這樣能夠不去討論密碼算法的安全性而是專心研究協(xié)議的內(nèi)在安全性質(zhì);而且Dolev和Yao提出了攻擊者模型，攻擊者具體強(qiáng)大的計(jì)算能力，不僅能夠?qū)f(xié)議運(yùn)行過程中真實(shí)實(shí)體間交換的信息進(jìn)行竊聽、截獲、篡改、重放操作，還可以對這些信息進(jìn)行加密、解密、拆分和組合[25-26].

由于EtherCAT協(xié)議具有高度的實(shí)時(shí)性，數(shù)據(jù)幀經(jīng)過每個(gè)從站的時(shí)間極小，在從站中數(shù)據(jù)幀的接收與解碼、數(shù)據(jù)的提取與插入、數(shù)據(jù)幀的轉(zhuǎn)發(fā)都是由硬件來實(shí)現(xiàn)的，因此本文將嘗試對主從站之間的網(wǎng)絡(luò)通道引入攻擊模型.

4.1 引入攻擊者模型

根據(jù)Dolev-Yao攻擊者模型中，攻擊者所具備的對網(wǎng)絡(luò)信道發(fā)起各類中間人攻擊的強(qiáng)大能力，對原始模型的網(wǎng)絡(luò)傳輸層引入重放、欺騙和篡改的中間人攻擊.

如圖11所示，我們對原始模型的網(wǎng)絡(luò)傳輸層面引入中間人攻擊包括重放、欺騙和篡改攻擊，圖11中藍(lán)色部分標(biāo)注的庫所和變遷模擬了重放攻擊，變遷TA截獲協(xié)議第一次傳輸時(shí)的信息，庫所distri能夠存儲分解和待分解的信息，庫所P2和P3存儲原子信息.變遷TC采用攻擊者的分解規(guī)則后將形成的原子消息保存到庫所P3中，變遷TH采用攻擊者的過度規(guī)則將無法解密的信息采用過度規(guī)則保存到庫所P4中.變遷TD將采用攻擊者的合成規(guī)則將原子消息合成后保存到庫所P5中.使用并發(fā)控制庫所SP對合成規(guī)則對應(yīng)的變遷TD加以限制，初始狀態(tài)可使能之外，每當(dāng)有分解的信息產(chǎn)生后再進(jìn)行點(diǎn)火合成.變遷TF將攻擊者的信息合成發(fā)送到信道端口庫所.圖11中的紅色標(biāo)注的弧上的表達(dá)式和變遷庫模擬了篡改攻擊，表達(dá)式中引入的攻擊者attack，通過變遷ATTACK發(fā)起攻擊.圖11中的紫色部分模擬了欺騙攻擊，包括了原始網(wǎng)絡(luò)傳輸過程中的全部變遷Transmit conn,Transmit ConnID,Transmit,SafeData,Transmit WKC.

Fig. 11 Attacker model

4.2 EtherCAT模型安全性評估

由表2所示的攻擊者模型的狀態(tài)空間報(bào)告可知狀態(tài)空間節(jié)點(diǎn)、有向弧與強(qiáng)連通節(jié)點(diǎn)、強(qiáng)連通弧的數(shù)目相同，說明該協(xié)議的攻擊者模型所有狀態(tài)節(jié)點(diǎn)都是可達(dá)的，引入攻擊者模型后，其狀態(tài)空間節(jié)點(diǎn)和弧的數(shù)量相對于原始模型來說增加不是太多，說明引入攻擊者模型后不會出現(xiàn)狀態(tài)空間過大或者爆炸的情況，降低了狀態(tài)空間節(jié)點(diǎn)規(guī)模，減少了不被接受者認(rèn)可的消息，在保證攻擊能力的基礎(chǔ)上提高了攻擊模型效率.說明我們引入的攻擊者模型是有效的.

Table 2 State Space Comparison of Models

將原始模型和加入攻擊模型后的狀態(tài)空間進(jìn)行對比，我們發(fā)現(xiàn)死節(jié)點(diǎn)變成6個(gè)，死變遷變成8個(gè).通過對死節(jié)點(diǎn)進(jìn)一步的查詢分析，發(fā)現(xiàn)有2個(gè)死節(jié)點(diǎn)是由于引入重放攻擊和篡改攻擊導(dǎo)致從站進(jìn)行了重置操作而產(chǎn)生的，剩下的4個(gè)死變遷是因?yàn)橐肫垓_攻擊致使協(xié)議產(chǎn)生不可預(yù)期的終態(tài)而導(dǎo)致的；通過對死變遷進(jìn)行分析，發(fā)現(xiàn)有2個(gè)死變遷是由于引入重放攻擊使得會話連接在從站無法使能，另外2個(gè)死變遷是由于引入欺騙攻擊導(dǎo)致從站沒有接收到從站的返回信息，其余4個(gè)死變遷則是因?yàn)橐氪鄹墓魧?dǎo)致在安全數(shù)據(jù)傳輸過程中CRC校驗(yàn)錯(cuò)誤而未使能.通過狀態(tài)空間的對比分析，可以發(fā)現(xiàn)攻擊者模型對原始模型的會話連接和安全數(shù)據(jù)傳輸過程發(fā)起了有效攻擊，側(cè)面反映出原始協(xié)議存在中間人進(jìn)行重放、欺騙和篡改的漏洞.

5 EtherCAT協(xié)議新方案

5.1 新方案加固方法

通過引入攻擊者模型對協(xié)議進(jìn)行安全評估，發(fā)現(xiàn)協(xié)議存在中間人進(jìn)行重放、欺騙和篡改的漏洞，針對安全評估結(jié)果，我們在協(xié)議的會話連接過程中引入秘鑰分發(fā)中心進(jìn)行認(rèn)證加固，為了確保安全數(shù)據(jù)的安全傳輸，我們在安全數(shù)據(jù)傳輸過程中加入Hash值.

如圖12所示為改進(jìn)后的消息流圖，改進(jìn)后的消息傳輸過程為：

1) 主站向秘鑰中心發(fā)生請求，包括主站地址、從站地址和連接ID.

2) 秘鑰分發(fā)中心對接收到的數(shù)據(jù)進(jìn)行處理，將地址信息和公鑰Ks用從站的私鑰Kb進(jìn)行加密，與公鑰Ks和接收到的其他信息，一起用主站的私鑰Ka進(jìn)行加密，然后回復(fù)給主站.

3) 主站用自己的私鑰對從站回復(fù)的消息進(jìn)行解密，得到公鑰Ks后，將其余需要發(fā)送給從站的消息發(fā)送給從站.

4) 從站用自己的私鑰Kb將收到的消息進(jìn)行解密，獲得公鑰Ks，利用公鑰將新產(chǎn)生的會話連接ID進(jìn)行加密，然后回復(fù)給主站.

5) 主站用公鑰將從站回復(fù)的消息進(jìn)行解密，獲得會話ID后，在本地對會話ID進(jìn)行函數(shù)運(yùn)行，最后用公鑰加密函數(shù)運(yùn)算的結(jié)果，發(fā)送給從站進(jìn)行認(rèn)證.

6) 從站用公鑰進(jìn)行解密接收到的消息，并且對解密后的會話ID 進(jìn)行認(rèn)證.

7) 建立會話連接之后，主站發(fā)起安全數(shù)據(jù)傳輸，首先將安全數(shù)據(jù)進(jìn)行本地Hash，然后將安全數(shù)據(jù)、Hash值、命令信息、計(jì)數(shù)信息和連接ID一并發(fā)送給從站.

8) 從站首先對接收到的信息進(jìn)行拆分，然后對安全數(shù)據(jù)進(jìn)行本地Hash,用本地生成的Hash值與接收到的Hash值進(jìn)行比對，如果相同則進(jìn)行相應(yīng)的命令操作，并且將技術(shù)信息加1，回復(fù)給主站.

Fig. 12 Message flow model of the new scheme

Fig. 13 Middle level model of new scheme model

5.2 EtherCAT協(xié)議新方案模型

我們將原始協(xié)議進(jìn)行加固，并且進(jìn)行CPN建模.改進(jìn)后的中層模型加入了秘鑰分發(fā)中心，由6個(gè)替代變遷和13個(gè)庫所組成，如圖13所示.其中，秘鑰分發(fā)過程由替代變遷Key Distribution表示，主從站連接建立以及認(rèn)證的過程由替代變遷Connection和Connection′來表示，安全數(shù)據(jù)的傳輸過程由替代變遷Safedata和Safedata′表示.改進(jìn)后的中層模型整體上描述了秘鑰分發(fā)、連接認(rèn)證和安全數(shù)據(jù)傳輸?shù)倪^程.

圖14對新方案替代變遷Connection的內(nèi)部模型進(jìn)行了詳細(xì)描述.主從站的地址信息和連接ID由變遷Combination進(jìn)行合并，然后通過庫所SendMAC發(fā)送到秘鑰分發(fā)中心；秘鑰分發(fā)中心返回的消息由庫所RecKs進(jìn)行接收；主站利用自己的私鑰Ka對收到的消息進(jìn)行解密，同時(shí)對收到的消息進(jìn)行確認(rèn)；將解密后需要發(fā)送給從站的消息通過庫所SendKb發(fā)送給從站；利用解密后的公鑰Ks對庫所RecSid′接收到的從站返回信息進(jìn)行解密，對解密后獲得的連接ID通過變遷Function進(jìn)行函數(shù)運(yùn)算；利用公鑰Ks對函數(shù)運(yùn)算的結(jié)果通過變遷變遷EncFID進(jìn)行加密，最后由通過庫所SendfSid發(fā)送給從站.

Fig. 14 Internal model of alternative transition Connection of new scheme model

圖15對新方案替代變遷Key Distribution的內(nèi)部模型進(jìn)行了詳細(xì)描述.秘鑰分發(fā)中心將主站的請求信息和要分發(fā)的公鑰Ks通過變遷Ks-Msg1進(jìn)行整合；將收到的地址信息和公鑰Ks通過變遷Kb-Msg進(jìn)行整合；將要回復(fù)主站的消息通過變遷ComMsg進(jìn)行打包；利用主站私鑰Ka對打包消息通過變遷KComMsg進(jìn)行加密，最后由庫所RecKs發(fā)送給主站.

圖16對新方案替代變遷Combination′的內(nèi)部模型進(jìn)行了詳細(xì)描述，從站利用自身私鑰Kb對接收到的消息通過變遷DecMsg進(jìn)行解密；利用解密后獲得的公鑰Ks對新產(chǎn)生的連接ID通過變遷EncID進(jìn)行加密，加密后的消息由庫所RecSid發(fā)送給主站；利用公鑰對主站發(fā)送的認(rèn)證消息通過變遷DecFID進(jìn)行解密，通過解密后獲得的連接ID進(jìn)行連接認(rèn)證.

Fig. 15 Internal model of alternative transition Key Distribution of new scheme model

Fig. 16 Internal model of alternative transition Connection′ of new scheme model

圖17對新方案替代變遷Safedata的內(nèi)部模型進(jìn)行了詳細(xì)描述，新方案主要改進(jìn)在于，通過變遷HashSafedata對安全數(shù)據(jù)進(jìn)行本地Hash處理，最后將Hash值與安全數(shù)據(jù)一并發(fā)送給從站.

圖18對新方案替代變遷Safedata′的內(nèi)部模型進(jìn)行了詳細(xì)描述，新方案的主要改進(jìn)在于，將接收到的安全數(shù)據(jù)通過變遷HashSafedata進(jìn)行本地Hash處理，通過變遷Comparison對新產(chǎn)生的Hash值Hdata′和接收到的Hash值Hdata進(jìn)行對比處理，相同則證明數(shù)據(jù)沒有被篡改，然后進(jìn)行相關(guān)命令的操作，并且將計(jì)數(shù)器加1返回給主站.如果不同則進(jìn)行重置操作.

Fig. 17 Internal model of alternative transition Safedata of new scheme model

Fig. 18 Internal model of alternative transition Safedata′ of new scheme model

5.3 新方案安全評估模型

我們利用相同的方式，引入Dolev-Yao攻擊模型，對新方案模型的網(wǎng)絡(luò)層面進(jìn)行中間人攻擊，包括篡改、欺騙和重放攻擊.如圖19所示，藍(lán)色部分模擬重放攻擊，紅色部分模擬篡改攻擊，紫色部分模擬欺騙攻擊.

Fig.19 Security evaluation model of new scheme

5.4 新方案模型安全性驗(yàn)證

我們將新方案模型安全評估的狀態(tài)空間與改進(jìn)前進(jìn)行對比，如表3所示.我們可以發(fā)現(xiàn)由于引入了秘鑰分發(fā)中心進(jìn)行認(rèn)證以及對數(shù)據(jù)加入了Hash值，增加了許多庫所和變遷，使得新方案的的狀態(tài)空間節(jié)點(diǎn)和弧數(shù)目有所增加.利用改進(jìn)前協(xié)議存在的3類中間人攻擊對新方案進(jìn)行安全性驗(yàn)證.由表3 的狀態(tài)空間對比結(jié)果可以發(fā)現(xiàn)，新方案模型的狀態(tài)空間死節(jié)點(diǎn)減少成一個(gè)，通過進(jìn)一步查詢得知，這個(gè)死節(jié)點(diǎn)表示協(xié)議運(yùn)行后的終態(tài)，而改進(jìn)前的多個(gè)死節(jié)點(diǎn)是由于攻擊狀態(tài)而造成的，說明新方案未遭受攻擊.新方案的死變遷相較于改進(jìn)前的死變遷數(shù)目有所變化，進(jìn)一步分析發(fā)現(xiàn)這些死變遷均發(fā)生在網(wǎng)絡(luò)層面，是由于攻擊者無法發(fā)起有效攻擊而造成的.攻擊者無法獲取協(xié)議連接過程的會話秘鑰，而無法對獲取的信息進(jìn)行解密分解，從而無法發(fā)起重放攻擊；在數(shù)據(jù)傳輸層面，新方案對協(xié)議的傳輸消息進(jìn)行了Hash處理，由于Hash值的不可逆性，所以攻擊者無法對消息發(fā)起篡改攻擊；由于新方案對協(xié)議加入了認(rèn)證，所以攻擊者無法對協(xié)議進(jìn)行欺騙攻擊.

Table 3 Comparison of the State Space of the Safety Assessment Model

通過分析表明，由于攻擊者無法獲得消息的會話秘鑰、認(rèn)證秘鑰以及無法篡改數(shù)據(jù)的Hash值，使得攻擊者無法發(fā)起攻擊，從而證明了新方案能夠防御之前的3種中間人攻擊，滿足協(xié)議安全機(jī)制需求.

5.5 新方案性能分析和分析方法對比

本節(jié)我們對新方案進(jìn)行性能分析，新方案通過引入秘鑰分發(fā)中心對協(xié)議主從站建立連接的過程進(jìn)行認(rèn)證加固，秘鑰靠秘鑰分發(fā)中心分發(fā)，不需要主從站生成，因此對協(xié)議通信的整體時(shí)間消耗較小.新方案在安全數(shù)據(jù)傳輸中加入了Hash值，不需要對安全數(shù)據(jù)進(jìn)行過多的加密操作，因此不需要對平臺進(jìn)行過大的升級，只是對整個(gè)通信來說，增加了計(jì)算、通信和存儲數(shù)據(jù)的開銷.所以改進(jìn)方案對協(xié)議運(yùn)行的開銷不大，僅僅增加了計(jì)算和存儲成本.本文在對協(xié)議進(jìn)行引入秘鑰分發(fā)中心和Hash函數(shù)改進(jìn)時(shí)，增加了協(xié)議消息交互的步驟，在增強(qiáng)協(xié)議安全性的同時(shí)會對協(xié)議的實(shí)時(shí)性有所影響.

我們將本文用到的形式化分析方案與其他分析方法做比較，文獻(xiàn)[10]中通過基于機(jī)器學(xué)習(xí)的異常檢測方法對EtherCAT進(jìn)行了分析，發(fā)現(xiàn)該方法不僅能夠進(jìn)行異常檢測，還可以標(biāo)記攻擊類型；文獻(xiàn)[11]中通過建立面向數(shù)據(jù)流的模型對EtherCAT進(jìn)行分析，發(fā)現(xiàn)該方法能夠?qū)f(xié)議進(jìn)行直觀、準(zhǔn)確的圖形表示，并且能夠驗(yàn)證協(xié)議的正確性.通過表4的對比分析，我們可以看出本文的基于有色Petri網(wǎng)理論和Dolev-Yao攻擊方法為指導(dǎo)模型檢測方法不僅能夠進(jìn)行直觀、準(zhǔn)確的圖形化描述和驗(yàn)證協(xié)議功能的正確性，還可以發(fā)現(xiàn)協(xié)議的攻擊類型，對協(xié)議通過引入攻擊者進(jìn)行異常檢測.同時(shí)方案對引入的攻擊模型進(jìn)行了改進(jìn)，解決了傳統(tǒng)模型檢測方法的狀態(tài)空間爆炸的問題，可以用該分析方案對其他工業(yè)以太網(wǎng)協(xié)議進(jìn)行安全分析與研究.

Table 4 Comparison of Protocol Formal Analysis Methods

6 總結(jié)與展望

本文將研究的重點(diǎn)放在工業(yè)以太網(wǎng)應(yīng)用熱門的EtherCAT協(xié)議的安全機(jī)制FSoE上，首先通過對協(xié)議安全機(jī)制消息流的分析，利用建模工具CPN Tools對協(xié)議進(jìn)行HCPN建模；然后在原始模型的基礎(chǔ)上加入攻擊者模型，并且通過對原始模型和攻擊模型狀態(tài)空間表進(jìn)行對比，對模型進(jìn)行安全性評估發(fā)現(xiàn)協(xié)議存在重放、竊聽和篡改3類中間人攻擊；最后針對協(xié)議所存在的3類攻擊提出了新的方案，并且對新方案進(jìn)行再次建模，引入攻擊者模型進(jìn)行再次攻擊，通過分析改進(jìn)前和新方案的狀態(tài)空間表，得出新方案可以有效防御重放、竊聽和篡改3類中間人攻擊.但是本文研究目的是為了改進(jìn)協(xié)議的安全性，對協(xié)議的實(shí)時(shí)性考慮不足，而且只對協(xié)議進(jìn)行了中間人攻擊，并未考慮協(xié)議是否存在其他形式的攻擊.下一步將考慮協(xié)議在保證安全的情況下是否滿足實(shí)時(shí)性要求，還有在其他攻擊形式下是否還存在安全的不足.