基于分布式物聯(lián)網(wǎng)的工業(yè)自動化安全性分析

汪建春，胡曉進

（江蘇農(nóng)林職業(yè)技術(shù)學(xué)院，江蘇 句容 212400）

智能物聯(lián)網(wǎng)（IoT）設(shè)備的先進功能已使其在工業(yè)自動化系統(tǒng)中得到廣泛應(yīng)用，從而迅速推進了可重構(gòu)制造系統(tǒng)（Reconfigurable manufacturing systems，RMS）的發(fā)展［1，2］。第四次工業(yè)革命的興起，開啟了高度定制制造的新時代。制造資源高度模塊化，為適應(yīng)動態(tài)市場需求提供了必要的靈活性［3］，可重構(gòu)制造系統(tǒng)支持有效的結(jié)構(gòu)和功能更改，可以在停機時間很短的情況下進行個性化配置。RMS的基礎(chǔ)是由智能工業(yè)物聯(lián)網(wǎng)（IoT）控制器控制的模塊［4］。IoT端點是異構(gòu)的，其部署環(huán)境根據(jù)流程需求和RMS的當前配置而動態(tài)變化。RMS的無縫重新配置、集成和可靠功能要求組件高度自治，必須能夠使用兼容協(xié)議（可集成性）彼此無障礙通信、交換與底層控制相關(guān)的信息，并以不同方式交互。

分布式控制體系結(jié)構(gòu)支持可重構(gòu)性，新一代的智能制造資源不僅必須利用功能所需的組件（如傳感器和執(zhí)行器）［5］，而且還須利用具有IoT功能控制器的固有計算和通信功能，以實現(xiàn)更高水平的自動化。通過控制分配，可將對特定物理資源進行控制的細粒度細節(jié)與資源協(xié)調(diào)問題解耦［6］，而資源協(xié)調(diào)問題只需要關(guān)心制造資源的性能即可。Rashid等［7］提出了一種基于模型的CPS攻擊仿真方法，但是不支持正式驗證，并根據(jù)具體攻擊實現(xiàn)得到了試驗結(jié)果。李慶鑫等［8］對工業(yè)CPS控制器進行了正式安全評估，但分析仍然局限于功能模型級別的高級漏洞。金志剛等［9］提出了在特定攻擊模型下的無線物聯(lián)網(wǎng)通信的全面正式安全分析，但未考慮對底層物理過程控制質(zhì)量的影響。

為了能夠建立安全的RMS，本研究引入了有效的技術(shù)，用于對部署在支持IoT的本地控制器（LC）上的分布式控制應(yīng)用程序進行系統(tǒng)安全分析，并且通過添加適當?shù)陌踩珯C制來解決檢測到的漏洞，利用安全分析的結(jié)果來改善存在攻擊時的自動化性能和安全保證。

1 方法

新一代分布式自動化系統(tǒng)的網(wǎng)絡(luò)性質(zhì)使它們?nèi)菀资艿骄W(wǎng)絡(luò)的攻擊，類似于其他網(wǎng)絡(luò)物理系統(tǒng)領(lǐng)域中報告的安全漏洞。例如，一個對手可能會注入錯誤事件，延遲或拒絕對合法控制器的網(wǎng)絡(luò)訪問，或操縱通過不安全的通信通道發(fā)送的控制命令［10］。在分布式順序控制系統(tǒng)中，提供安全保證至關(guān)重要，在該系統(tǒng)中，其進度直接受到通信不可用性的影響。本研究提出的靈活分布式自動化方法如圖1所示。在大部分物聯(lián)網(wǎng)系統(tǒng)中，組件之間的協(xié)調(diào)是基于離散事件的。雖然在物聯(lián)網(wǎng)框架下使用了大量的正式建模框架，但工業(yè)自動化系統(tǒng)通常基于GRAFCET（IEC 60848）/SFC（IEC 61131-3）控制設(shè)計。本研究聚焦使用CIPN（Control Interpreted Petri Nets）描述的IoT控制器的安全分析，該控制器可以直接開發(fā)或者使用現(xiàn)有的集中式順序自動化設(shè)計的分發(fā)方法自動派生［11］，允許在IoT支持的智能控制器上部署遺留控制應(yīng)用程序。

圖1 基于彈性IoT的靈活分布式自動化方法

2 基于TPN的自動化建模

TPN通過引入定時轉(zhuǎn)換來擴展PN。在TPN中，每個轉(zhuǎn)換的特征都是間隔或，其中t f和是轉(zhuǎn)換觸發(fā)時間的下限和上限，可以為零或無窮大，TPN支持不確定性，有助于使用確定性或隨機模型無法準確完成的攻擊建模。

將CIPNi（i=1,…,N）表示的形式化分布式控制規(guī)范轉(zhuǎn)換為TPN兼容模型使用工廠模型和安全感知通信信道模型，能夠在建模對抗性的影響下對系統(tǒng)級的安全特性進行推理。由于CIPN和TPN都起源于PNS，從CIPNi（i=1,…,N）控制器模型到的轉(zhuǎn)換，所有轉(zhuǎn)換都是直接的，即：

通過發(fā)出I/O API調(diào)用來處理驅(qū)動和轉(zhuǎn)換處理感知；

通過共享信道處理傳輸，并使用API調(diào)用處理通信信號的接收［分別為send（destination，signal）和signal=value］；

調(diào)用其他平臺相關(guān)API的位置，如請求執(zhí)行延遲。

這些轉(zhuǎn)換直接依賴于實現(xiàn)控制器底層平臺的CIPN結(jié)構(gòu)，必須為捕獲以下內(nèi)容的網(wǎng)絡(luò)顯式地建模［12］：①與工廠之間的交互；②與通信信道之間的交互；③基于已發(fā)布命令（如變量更新、執(zhí)行延遲）更改運行時環(huán)境。

2.1 工廠間控制器交互建模

由于CIPN的形式已被自動化設(shè)計普遍采用，因此假設(shè)可以使用基于PN的（即CIPN或TPN）工廠模型，pick&place站的位置如圖2所示。在到達時間上有一個下限，位置p＆p_Init表示站點的初始狀態(tài)，來自該位置的令牌流受控制器模型的LC1對應(yīng)命令限制。在TPN形式上，標記相關(guān)的保護函數(shù)可用于限制工廠模型中的狀態(tài)變化（即令牌流），即用標記相關(guān)的函數(shù)評估控制器的狀態(tài)，并返回參數(shù)位置內(nèi)的當前令牌數(shù)量［13］。一旦LC2的模型將其令牌觸發(fā)了pick&place過程，即LC2從特定的傳送帶啟動它，則站的令牌將轉(zhuǎn)換為傳送帶1（或2）有待處理的工件。

圖2 物理設(shè)置

2.2 CIPN和TPN控制器等效

CIPN的執(zhí)行路徑可以定義為標記序列，其中由于觸發(fā)轉(zhuǎn)換而導(dǎo)致標記發(fā)生變化，每個標記都與一組動作相關(guān)聯(lián)，每個轉(zhuǎn)換的觸發(fā)都受一組條件限制。在TPN模型中，路徑的特征是具有相似的序列加上轉(zhuǎn)換時序。在TPN模型中維持CIPN控制器執(zhí)行路徑即可，目標是源（集中）和目標（分布式）控制模型的操作等價性［14］。

3 彈性分析與漏洞修復(fù)

通過對已開發(fā)的安全感知TPN模型的組合，得到一個安全感知閉環(huán)系統(tǒng)模型，用于驗證系統(tǒng)級安全性和攻擊時的QoC特性。TPN分析工具允許驗證形式屬性，這些形式屬性指定為線性時序邏輯（LTL）、計算樹邏輯（CTL）或定時CTL（TCTL）公式。使用工具Romeo來驗證基于TCTL，如傳統(tǒng)安全性和活動性。此外，由于包含了工廠模型，可以指定與領(lǐng)域相關(guān)的工廠狀態(tài)屬性，這些屬性對于功能安全性和QoC評估至關(guān)重要。本研究考慮的屬性包括：

屬性1：傳送帶1上的工件永遠不會觸發(fā)傳送帶2的pick操作；

屬性2：在任何傳送帶上檢測到的工件最終都被拾??；

屬性3：在輸送機監(jiān)視器等待進來的工件（即在Pcm_Init處）時，pick&place沒有開始循環(huán)。

在存在攻擊的情況下，使用Romeo工具驗證這些屬性，因為攻擊者能夠在任意時間改變LC之間的預(yù)期交互。從試驗測量或直接從網(wǎng)絡(luò)規(guī)格中獲得傳輸時間和時間的界限。此外，從所使用收發(fā)器的規(guī)格中獲得與收發(fā)器有關(guān)的時間，如在空閑信道評估期間的退避時間。

關(guān)于驗證的可伸縮性，在系統(tǒng)模型中，一個正常的pick&place循環(huán)［15，16］（所有攻擊都被禁用）包含了約35個轉(zhuǎn)換，數(shù)量約為模型中狀態(tài)數(shù)的數(shù)量。除了在工廠模型中時間誘發(fā)的不確定性外，模型的復(fù)雜性還會隨著不確定性攻擊選擇的增加而增加。然而，在所有情況下，Romeo工具在具有Inteli7-8086K CPU和64 GB內(nèi)存的工作站上，只需不到1 s的時間就可以找到違反屬性的執(zhí)行路徑。

在系統(tǒng)漏洞修復(fù)方向，攻擊行為可能會嚴重影響基于IoT的分布式工業(yè)自動化系統(tǒng)的性能。為了解決這些問題，有必要添加某些安全機制，討論安全機制對系統(tǒng)模型和相關(guān)屬性可驗證性的影響。

1）檢測拒絕服務(wù)攻擊：分組和確認（ACK）丟失在無線通信中很常見，因此通常在此類設(shè)置中使用ACK和重傳機制。例如，在收發(fā)器設(shè)置中禁用ACK請求，不會在數(shù)據(jù)鏈路層上嘗試重傳。對于兩個隔離的收發(fā)器，相當于約99%的單向數(shù)據(jù)包成功率。因此，當啟用ACK請求時，最多執(zhí)行3次數(shù)據(jù)鏈路層重傳，在單個工業(yè)機器運行的情況下，除了3個低層協(xié)議提供的重傳外，不需要應(yīng)用層重傳。為了提高網(wǎng)絡(luò)利用率，模擬了通過同一無線信道通信的其他機器數(shù)目；單向數(shù)據(jù)包的成功率約為98%。因此，兩次應(yīng)用層重傳足以實現(xiàn)可靠的事件交換，從而確保正確的操作。協(xié)議提供的重試是在短時間內(nèi)進行的，而應(yīng)用層重傳則會產(chǎn)生較大的延遲，通道很可能在短時間內(nèi)持續(xù)忙碌，如被其他合法的傳輸占用。然而，對手可能會反復(fù)拒絕對合法控制器的網(wǎng)絡(luò)訪問，從而阻止系統(tǒng)運行。因此，除非使用單獨的安全通道檢測到DoS攻擊并停止系統(tǒng)（或采取其他預(yù)防措施），否則建模的系統(tǒng)不滿足屬性2。

從操作角度來看，每個LC都可以在聲明受到攻擊之前實施有限數(shù)量的連續(xù)應(yīng)用層重傳。為了從建模角度解決這個問題，當應(yīng)用層重傳用盡時，添加了發(fā)射器模型轉(zhuǎn)換到其他位置。如果將DoS攻擊限制為4個連續(xù)的通道訪問拒絕，則可以滿足屬性2。如果沒有安全的通信通道或無法將DoS攻擊與網(wǎng)絡(luò)隔離，則可能無法立即緊急停止機器。

2）網(wǎng)絡(luò)流認證：確保網(wǎng)絡(luò)流完整性的傳統(tǒng)加密技術(shù)依賴于使用消息認證碼（Message Authentication Codes，MAC）對數(shù)據(jù)包進行簽名，并可用于防御欺騙攻擊。在這種設(shè)置下，LC之間的每一次傳輸都由發(fā)送方使用密鑰簽名，并且簽名由接收方驗證。因此，攻擊者無法篡改消息有效負載，否則會被檢測到。

從建模的角度來看，可將引入身份驗證建模為在控制器模型中接收轉(zhuǎn)換的附加條件，在該轉(zhuǎn)換中，將接收到的有效負載與所需值進行比較，即將有效負載的MAC部分與攻擊者無法更改（在修改的情況下）或生成（在欺騙攻擊的情況下）的秘鑰值進行比較。驗證傳輸不會影響ACK，因為在將MAC添加到數(shù)據(jù)包有效負載的同時，數(shù)據(jù)鏈路層負責ACK數(shù)據(jù)包。此外，攻擊者可能會竊聽未加密的序列號，該序列號是數(shù)據(jù)包幀的一部分，因此，可以代表不活動的LC生成有效的ACK。同時，即使使用認證，也可能錯誤地確認了未送達的傳輸，這是數(shù)據(jù)鏈路層ACK已知的缺點，可以通過應(yīng)用層ACK來緩解，所提出的建模技術(shù)可以用于對附加的已實現(xiàn)協(xié)議進行建模。

4 實證分析

考慮重構(gòu)工業(yè)氣動機械手的完整物理實現(xiàn)，該機械手具有以分布式方式控制的可變數(shù)量的模塊，每個模塊有一個本地控制器，本節(jié)展示了提出的框架在多種模塊配置（即2-DOF、3-DOF）上的有效性。

4.1 自由度（2-DOF）工業(yè)氣動機械手

2自由度配置的氣動工業(yè)機械手如圖3a所示。兩個雙作用氣缸（A和B）提供了平移自由度，而氣動夾爪（C）提供工件的操作方式。所有的驅(qū)動命令都是通過更新電子信號x p,x∈{a,b,c}發(fā)出的，該信號可以激活單穩(wěn)雙控氣動閥門，信號用x表示，而氣缸用X表示。氣缸A和氣缸B有兩個接近開關(guān)，可以感應(yīng)位置（即完全收回、完全伸出）。對應(yīng)于完全收回（原始）位置的信號表示為x0，而完全伸出（結(jié)束）位置的信號表示為x1。此外，系統(tǒng)還包含一個啟動開關(guān)，其相應(yīng)信號由s t表示。

圖3 氣動機械手配置

初始狀態(tài)下，氣缸A和B完全收回，并且氣動夾爪C松開。在這種狀態(tài)下，機械手已準備好開始其工作周期。通過按下啟動開關(guān)（s t=1）啟動機械手的初始工作周期，完成后為全自動操作。首先，氣缸B朝著工件pick位置延伸（驅(qū)動命令bp=1），一旦氣缸B到達其末端位置（b1=1），則氣動夾爪C抓取（cp=1）?？刂破鰾等待500 ms抓緊零件，然后氣缸B縮回（命令bp=0所致），一旦到達原始位置（b0=1），氣缸A伸出（命令ap=1），到達終點位置（a1=1）后，氣缸B向放置位置延伸（命令bp=1）。一旦到達其最終位置（b1=1），抓爪C釋放工件（命令cp=0）。500 ms后，氣缸B收回（bp=0，然后b0=1），之后氣缸A收回（ap=0，然后a0=1）。機械手返回初始狀態(tài)，并自動執(zhí)行下一個循環(huán)。

氣缸被建模為兩個狀態(tài)工廠模型，伸出和收回時間從試驗測量獲得。圖4為所使用低成本ARM Cortex-M3控制器配備符合IEEE802.15.4標準收發(fā)器的10 000條消息的Tx-Rx和Rx-Ack時間延遲。

圖4 在支持IEEE 802.15.4的LC平臺上測量Tx-Rx和Rx-Ack時間

4.2 自由度（3-DOF）工業(yè)氣動機械手

3自由度（3-DOF）工業(yè)氣動機械手配置如圖3b所示。氣缸C提供的附加旋轉(zhuǎn)自由度會引入附加LC，并增加LC協(xié)調(diào)的復(fù)雜性。將工件浸入帶有清潔液的水池中，然后將其返回到pick位置，以供另一臺機器進行進一步處理，可以使用該配置來處理噴涂的工件。

圖3c顯示了該配置的物理設(shè)置以及具有相應(yīng)IEEE 802.15.4收發(fā)器的低成本基于ARM Cortex-M3的LC。盡管這些模型比2-DOF情況更復(fù)雜，但它們在語義上相似的。圖5a所示為事件時間，即對于一個樣本在“拾取-浸泡-搖動-返回”運行過程中，所有感測和驅(qū)動信號的狀態(tài)。

攻擊者可以在工件返回到返回位置之前發(fā)送釋放工件的命令。圖5b顯示了在一個采樣周期運行中獲取的信號時序，在該采樣周期中，會存惡意注入釋放夾爪的命令而釋放夾具，從而使工件掉落，這可能會對工件或機械手造成損壞。如果對傳輸進行了驗證，并相應(yīng)地調(diào)整了模型，則可以緩解此漏洞。通過包括IoT控制器完全兼容的mbed TLS（安全套接層）來應(yīng)用軟件安全補丁，在一個傳輸信號上簽署128位消息驗證代碼，在使用的低成本基于ARM Cortex-M3的LC計算開銷為100μs，在提供安全保證的同時，相對于機械手的工作周期幾乎可以忽略。

從模型的角度來看，DoS攻擊不會造成死鎖，在物理過程停滯的同時，網(wǎng)絡(luò)過程實際上是動態(tài)鎖定的。圖5c顯示在一個示例運行中獲取的信號定時，通過在攻擊者的收發(fā)器上啟用載波傳輸來啟動DoS，以便從浸泡池中拾取工件后阻塞消息。無線控制節(jié)點可以跟蹤不成功的介質(zhì)訪問嘗試，并在檢測到DoS攻擊時立即停止操作。

圖5 驅(qū)動信號

5 小結(jié)

本研究開發(fā)了一個框架來分析基于CIPN的分布式順序控制系統(tǒng)的安全性。由于在存在攻擊時CIPN不支持對形式安全屬性的驗證，因此將控制器模型轉(zhuǎn)換為TPN，從而通過支持不確定的定時轉(zhuǎn)換以及轉(zhuǎn)換之間的不確定性選擇來固有地支持此驗證，討論了如何將基于網(wǎng)絡(luò)的攻擊者的模型集成到非確定性的通信渠道模型中，并驗證了存在攻擊時違反安全性的行為。此外，運用驗證結(jié)果來查明控制軟件實施中的漏洞，并提出安全補丁以減輕這些漏洞對控制性能的影響。