基于分布式物聯網的工業自動化安全性分析

汪建春，胡曉進

（江蘇農林職業技術學院，江蘇 句容 212400）

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

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

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

1 方法

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

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

2 基于TPN的自動化建模

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

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

通過發出I/O API調用來處理驅動和轉換處理感知；

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

調用其他平臺相關API的位置，如請求執行延遲。

這些轉換直接依賴于實現控制器底層平臺的CIPN結構，必須為捕獲以下內容的網絡顯式地建模［12］：①與工廠之間的交互；②與通信信道之間的交互；③基于已發布命令（如變量更新、執行延遲）更改運行時環境。

2.1 工廠間控制器交互建模

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

圖2 物理設置

2.2 CIPN和TPN控制器等效

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

3 彈性分析與漏洞修復

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

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

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

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

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

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

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

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

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

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

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

4 實證分析

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

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

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

圖3 氣動機械手配置

初始狀態下，氣缸A和B完全收回，并且氣動夾爪C松開。在這種狀態下，機械手已準備好開始其工作周期。通過按下啟動開關（s t=1）啟動機械手的初始工作周期，完成后為全自動操作。首先，氣缸B朝著工件pick位置延伸（驅動命令bp=1），一旦氣缸B到達其末端位置（b1=1），則氣動夾爪C抓取（cp=1）。控制器B等待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）。機械手返回初始狀態，并自動執行下一個循環。

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

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

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

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

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

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

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

圖5 驅動信號

5 小結

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