工業是一個國家的根本的經濟命脈，工業控制系統（Industrial Control Systems，ICS）是工業自動化體系結構的重要組成部分。隨著工業4.0時代的到來，工業網絡的安全性日益重要。工業以太網EtherNet/IP協議使用原有的基于標準的以太網技術，已經被大量使用在工業網絡控制系統中，其安全性一直備受關注，國內對工業網絡協議安全性的研究很少。使用形式化分析工具Scyther在Delov-Yao模型和強安全模型下對EtherNet/IP協議核心成員通用工業協議（Control and Information Protocol，CIP）所采用的加密認證TLS協議進行形式化分析。對下一代CIP協議嵌入TLS1.3具有實踐價值，該方法對其他工業網絡協議進行有效的安全分析有理論指導意義。
EtherNet/IP協議簡介和CIP介紹
EtherNet/IP協議結構和性能
EtherNet/IP（EtherNet/IP Industry Protocol）是由兩大組織ODVA（Open DeviceNet Vendors Association）和ControlNet International于2001年正式推出的新的協議成員。使用通用工業協議（CIP）作為上層協議，結合傳統的以太網協議技術和標準的TCP/IP（Transmission Control Protocol/Internet Protocol）協議共同構成EtherNet/IP協議的體系結構，該協議是基于CIP協議的工業網絡協議。EtherNet/IP協議有較好的互操作性能，而且數據傳輸距離長，傳輸速率高。CIP協議獨立于物理層和數據鏈路層之上，與設備介質無關，可以將其移植到高性能的網絡設施上。CIP封裝協議的主要任務是定義和規范了如何封裝和傳輸上層協議的報文，以及如何管理和利用下層TCP/IP鏈接，起到承上啟下的作用。EtherNet/IP協議網絡遵循開放的OSI模型。圖1是EtherNet/IP協議結構圖。
由于以太網數據傳輸速度的大幅度提升和工業網絡交換機技術的快速發展，在網絡高負載通信時EtherNet/IP協議也能夠滿足工業網絡對實時性和確定性的要求。EtherNet/IP協議使用高效的數據傳輸模式——生產者/消費者模式（Producer/Consummer）。端點之間的聯系不是通過具體的源和目的地址關聯起來，而是一個生產者可以對應多個消費者，使數據的傳輸達到了最優化。網絡源節點按照內容將數據進行標識，采用組播的方式同時發送到多個節點，網絡上其他節點按照自己的需要通過標識符來確定要接收的數據。避免了帶寬浪費，節省了網絡資源，同時提高了系統的通信效率。能夠很好地支持系統的控制、組態和數據采集，并且非實時性通信和實時性通信可以在同一子網中實現。但工業控制系統遭受越來越多的威脅，主要是網絡協議自身的缺陷引起的，EtherNet/IP協議也存在安全問題，需要進一步提高安全防護能力。
CIP報文傳輸方式
CIP協議報文傳輸方式有顯式報文和隱式報文傳輸兩種方式。當CIP協議嵌入UDP協議用于發送隱式報文（Implicit（I/O）Message）。而CIP協議嵌入TCP協議用于發送顯式報文（Explicit Message）。兩種報文使用的封裝協議不同，傳輸的消息類型也不同。CIP將應用對象之間的通信關系抽象為連接，并與之相應制定了對象邏輯規范，使CIP協議可以不依賴于某一具體的網路硬件技術，用邏輯來定義連接的關系，在通信之前先建立連接獲取唯一的標識符（Connection ID，CID），如果連接涉及雙向的數據傳輸，就要分配兩個CID。
顯式報文針對組態信息、設備配置、故障診斷等非實時性信息，其優先級較低（包含解讀該報文所需要的信息），通過點對點的報文在兩個對象之間以交互的方式進行傳輸。報文本身攜帶有關地址、數據類型和功能描述等相關內容，接收設備根據內容做出相應的處理，采用源/目的地址傳送方式。在通信之前通過TCP協議獲得標識符CID，之后進行數據報文傳輸。使用通信端口0XAF12f。圖2是CIP顯示報文連接。
隱式報文用于節點之間傳輸實時I/O數據、實時互鎖，優先級較高（隱式報文中不包含傳送地址、數據類型標識和功能描述內容），全部作為有效數據，傳輸效率高，在報文頭部有數據標識符，消費者根據標識符選擇自己需要的內容，通過UDP協議將實時I/O消息傳送到總線上。圖3是CIP隱式報文連接。
CIP通信安全
目前CIP協議仍然使用IETF標準TLS1.2（Transport Layer Security:RFC 5246）和DTLS1.2（Datagram Transport Layer Security:RFC 6347）協議版本保證顯示報文和隱式報文數據傳輸的安全性。TLS協議安承擔著Internet上通信的安全，造成越來越多的威脅，目前TLS1.2存在很多已被證明的安全隱患，TLS1.3（Transport Layer Security:RFC:8846）協議是2018年3月更新的最新版本，較之前的TLS1.2版本有較大的改變，修改了部分內容，其安全性更高，這為EtherNet/IP協議的安全帶來新的挑戰和利益，因為其應用層CIP協議的安全性取決于TLS和DTLS協議安全保障能力。為了最大程度提高EtherNet/IP協議的安全性能，必須保證其應用層協議CIP的安全性，所以最終在CIP協議中必須支持TLS1.3版本。TLS1.3在CIP協議中的支持預計要3~6年才能實現，TLS協議在握手期間實現秘鑰建立和認證，身份驗證和秘鑰的建立很大程度上來說對CIP層和EtherNet/IP是透明的。TLS協議保證在不安全的傳輸通道上使用加密確保數據的安全傳輸。而DTLS協議是TLS轉換而來的，采用同TLS相同的設計方法，所以本文只對TLS協議進行形式化分析。
TLS協議保障在TCP傳輸安全性，客戶端和服務端建立TCP連接之后，建立TLS會話，實現TLS握手和TLS記錄協議。TLS協議由很多子協議組成，其中核心協議是記錄協議和握手協議，TLS握手協議負責身份驗證和秘鑰建立（包括TLS版本確定和秘鑰交換以及后續使用的秘鑰算法），記錄協議通過使用客戶端和服務器協商后的秘鑰進行數據加密，TLS記錄協議主要用來識別TLS中的消息類型（通過“Content Type”字段的數據來識別握手、警告或數據），以及每個消息的完整性保護和驗證。圖4是TLS協議實現客戶端和服務端建立會話的初始配置過程。
CIP報文傳輸分為隱式報文傳輸和顯式報文傳輸，顯式報文使用TCP傳輸，在TCP之上的應用可以使用TLS來保證傳輸信息的安全性。但是TLS并不能保證UDP的傳輸安全，DTLS是在TLS協議框架上擴展出來的。其協議結構基本上同TLS相同，在隱式報文傳輸中使用UDP協議，對使用UDP協議通信的傳輸使用DTLS協議進行加密處理。TLS和DTLS層次結構如圖5所示。
TLS協議形式化分析及實驗結果
Scyther性能簡介
Scyther軟件是由牛津大學教授CAS CREMERS使用Python語言開發的一款功能很強的用于驗證和表征安全協議的自動化協議形式化分析工具，由于Python語言可以快速生成用戶界面，使用Python語言開發的軟件具有良好的人機交互界面，因此Scyther軟件具有可以對協議分析攻擊軌跡的輸出功能，便于理解協議存在的漏洞。Scyther軟件的協議分析采用Athena算法，使用該算法使得Scyther軟件可以支持多協議并行分析，該工具是安全協議形式化分析的最新技術，支持分析與時序相關的協議，同時可以尋找協議的多種攻擊，輸出協議角色執行軌跡和攻擊圖。除此之外，Scyther軟件對無限會話和無限狀態集合的協議給出明確的終止，其中實現多協議的并行分析解決了傳統分析工具的狀態空間爆炸問題，Scyther形式化分析工具內置了Delov-Yao模型和強安全模型，所以敵手的攻擊模式設置簡單。并且在攻擊漏洞和攻擊誤報等性能方面也表現較好。
Scyther敵手模型和語義操作
強安全模型是通過敵手定義更強的攻擊能力，決定了敵手能力在完全掌握了通信網絡的基礎上，具備腐蝕化長期私鑰和臨時秘鑰等能力，Scythe可以通過敵手詢問組合的方式選擇安全模型，設置方便，并且有明確的終止。在強安全模型下可以同時添加會話秘鑰泄露、隨機數泄露、狀態泄露等。圖6是Scyther軟件敵手模型設置界面。
Scyther定義安全協議結構模型如圖7所示。
Scyther使用SPDL語言規定了一系列的操作語義和操作原語，基本的操作語義如表1所示。
對TLS協議形式化安全分析
對TLS1.2協議進行形式化分析，本文采用Scyther- Compromise-0.9.2版本，運行在Intel（R） Core（TM） i5-7400 CPU@ 3.00 GHz、操作系統是Linux kali 4.19.0-kali3-amd64、8 GB RAM的電腦上（賦予至少4 GB以上的內存），具體的使用軟件及工具參見表2。
TLS協議會話形式化分析過程
首先使用Scyther工具的SPDL語言對TLS握手協議交互的過程進行形式化的描述，分別在Delov-Yao模型和強安全模型下對該協議進行形式化分析。SPDL語言對協議的描述是基于角色的，在定義了協議交互使用的變量之后，整個協議的交互過程通過參與協議每個主體發生的事件集合表示。其中send和recv事件表示該主體發送和接收消息的事件，目標屬性的描述通過claim事件完成，利用claim事件可以對角色的認證性、變量的機密性等進行描述。Scyther-Compromise工具可以方便地更改協議分析的安全模型，該工具的敵手的攻擊分析能力可以通過選項的形式供用戶選擇。
CIP協議嵌入到TCP報文傳輸的時候，在實現客戶端和服務端身份認證的時候，首先建立TLS會話，通過對協議版本、密碼算法和認證方式以及公鑰加密技術的協商，進入協議握手階段，圖8是TLS握手協議流程圖。
?。?）客戶端首先發起請求，交換hello協商算法、
隨機數、協議版本等信息。
（2）交換必要的密碼學參數，客戶端和服務器生成預主秘鑰。
（3）雙方交換數字證書，客戶端驗證服務端證書通過后取出證書中的公鑰。
?。?）通過預主秘鑰和交換的隨機數生成主秘鑰。
?。?）為之后的記錄層提供安全參數。
?。?）秘鑰確認，進行通信。
根據TLS握手協議分析涉及的2個實體（Client、Server），協議形式化定義2個角色a和b分別表示客戶端和服務器。
實驗結果
Scyther采用黑盒驗證思想，每個角色從自身的角度判斷是否滿足安全目標或者安全屬性，工業網絡最初與用戶應用網絡Internet是分開的，像CIP、EtherNet/IP沒有考慮傳輸安全類問題，缺乏固有的安全機制。近些年研究人員公開報告了CIP和EtherNet/IP中許多漏洞，因為EtherNet/IP協議使用基于CIP的以太網協議，固然也存在安全隱患，圖9是Scyther-Compromise工具在Delov-Yao模型下對TLS握手協議的形式化分析輸出的攻擊路徑圖，圖10是在該模型下驗證TLS握手協議秘鑰協商的機密性，結果顯示在該模型下不存在攻擊威脅。
圖11是在Scyther-Compromise工具中通過添加選項長期私鑰泄露、會話秘鑰泄露、隨機數泄露以及狀態泄露的強安全模式設置參數界面。圖12是在強安全模型下對TLS握手協議機密性驗證，結果顯示存在至少4個攻擊，證明在強安全模型下，TLS握手協議不能保證秘鑰的機密性。
結論
本文分析了EtherNet/IP協議的結構和性能，其核心組成成員應用層CIP協議的安全性取決于加密認證協議TLS的安全保證能力，使用Scyther工具對TLS協議進行形式化分析，設置敵手模型分別為Delov-Yao模型和強安全模型下進行驗證，從輸出的攻擊軌跡圖，證明在強安全模型下TLS協議存在長期秘鑰泄露導致主體的長期私鑰泄露的危險。由于秘鑰傳輸過程中傳輸的機密性取決于長期私鑰的安全性。實驗證明TLS握手協議在強安全模型下傳輸秘鑰不安全，TLS協議無法保證CIP協議通信的安全，導致了使用CIP作為EtherNet/IP協議的核心協議在應用層的傳輸不夠安全。未來在EtherNet/IP協議嵌入TLS1.3版本的時候不得不重新考慮整體安全性。
內容節選自《信息技術與網絡安全》2019年第七期《工業以太網EtherNet/IP協議安全分析》一文，作者田學成，徐英會）