顧兆軍，孫浩然
(1.中國民航大學信息安全評測中心，天津300300；
2.中國民航大學中歐航空工程師學院，天津300300)
工業控制系統(Industrial Control System，ICS)是由各種自動化控制組件以及實時數據采集組件和監控控制組件共同構成的信息系統[1]。一般來說，工業控制系統的核心組件包括數據采集與監控系統(Supervisory Control And Data Acquisition，SCADA)、分布式控制系統(Distributed Control System，DCS)、可編程邏輯控制器(Programmable Logic Controller，PLC)、遠程終端(Remote Terminal Unit，RTU)、智能電子設備(Intelligent Electronic Device，IED)和確保各組件通信的接口等技術系統[2]。
SCADA系統是一個典型的工業控制系統[3]。SCADA系統優點在于邏輯范圍廣，系統應用軟件多，但系統內硬件結構復雜，系統所處環境多樣，一旦遭到攻擊，將會對現實物理世界造成巨大危害。2007年，加拿大的水利SCADA控制系統遭到黑客入侵，攻擊者利用惡意軟件破壞供水控制計算機，致使水利系統一度陷入癱瘓。2010年，震網病毒(Stuxnet)[4]攻擊伊朗濃縮鈾工廠，超過1000臺離心機遭到攻擊而癱瘓，伊朗核工業發展遭受重創。2011年，黑客入侵美國伊利諾伊水廠SCADA系統，導致水泵被破壞，污水泄漏。2017年，Wannacry[5]勒索病毒爆發，數以萬計加油站因遭受攻擊而無法為用戶提供正常服務。
SCADA系統是工業控制系統的核心，是國家關鍵基礎設施的重要組成部分，加強對SCADA系統的安全防護，是我國信息安全保障建設的重大課題[6]。從“兩化融合[7]”到“中國制造2025計劃[8]”的推廣，我國對于工控網絡安全保護策略的制定和相關技術的研發處于起步階段。隨著兩化融合，工業控制網絡安全形勢也變得越來越嚴峻[9]，工控網絡安全逐漸成為產業界和學術界共同關注的焦點，對于工控網絡安全評估研究成為熱門研究領域。
Ralston[10]等人給出了SCADA和DCS系統風險評估概要，提出基于妥協表的分析方法。Byres[11]等人對SCADA系統通信協議進行安全評估，指出SCADA系統中Profibus協議脆弱性。白佳林[12]等人總結了人為干預、通信、內部元器件等因素是導致電力系統安全性降低的原因。Nie L[13]等人提出使用貝葉斯加權攻擊路徑建模技術模擬攻擊過程。
工業安全領域中常用形式化分析方法對系統安全性進行評估，形式化分析方法包括攻擊樹[14]、攻擊圖[15]、時間自動機[16]等。其中時間自動機是自動機的理論擴展模型，其優點在于有一些有效軟件工具幫助構建時間自動機模型并完成模型驗證，因此利用時間自動機對工業控制系統安全性驗證在近些年得到了廣泛應用。
本文提出一種基于時間自動機的形式化驗證方法，對SCADA系統安全屬性變化進行分析與驗證。首先以機場供油自控系統為例，將系統分為監視層、控制層、現場設備層，對每個層級進行時間自動機建模，三個層級的時間自動機一同構成了時間自動機網絡。其次根據常見的網絡攻擊方式，建立針對工控系統的攻擊模型，分析工控網絡攻擊對機場供油自控系統造成的影響。針對工控網絡攻擊提出防御手段，構建防御模型并分析驗證在引入防護措施后航油自控系統安全屬性。最后利用UPPAAL工具驗證該工控系統在正常環境下、遭受攻擊條件下以及引入防御措施條件下的安全屬性變化。
2.1 時間自動機
時間自動機是由ALUR和ADIL提出的一種基于自動機理論的自然擴展，用于構建實時系統模型[17]。
設X是一個時鐘變量集，x表示X當中的一個時鐘值，c表示有理數集Q中的常量，φ1，φ2表示時鐘約束。時鐘約束集合Φ(x)的約束公式如下：
δ∶=x≤c|c≤x|x (1) 時鐘變量集X上的一個時鐘解釋v表示為從X到R+的一個映射，如果對于v所提供的任意的時鐘賦值，時鐘約束δ布爾值為真，則稱v是X上的一個時鐘約束。 時間自動機是一個六元組：A= Φ(A)∶=a≤c|c≤a|a (2) UPPAAL[18]是基于時間自動機理論的模型形式化驗證工具，主要包括編輯器、模擬器和驗證器。首先利用指令和共享變量將基于時間自動機建立的設備模型連接在一個網絡中。其次，通過窮舉法驗證系統模型的邏輯性和安全性。同時UPPAAL工具利用了CTL語法，具體如表1所示。 表1 CTL屬性說明表 機場供油過程一般由機場油庫、輸送管網、輸送裝置和過濾裝置構成[19]，如圖1所示。 中轉油庫接收貨輪來油和鐵路來油，煤油進入中轉油庫后在儲油罐內沉降，經化驗合格后通過送油泵和長運輸管道輸送至使用油庫。使用油庫繼續對煤油進行沉降，直到油庫內煤油檢驗合格后，煤油才可以通過送油泵輸送到停機坪供油系統向飛機加油。由于飛機用油對煤油清潔度要求較高，利用過濾裝置對煤油進行過濾除雜質，保證煤油含雜質量降低到要求水平之下。 圖1 機場供油流程圖 機場供油自控系統網絡拓撲簡如圖2所示，自控系統由監控管理層、直接控制層和現場設備層組成。監控管理層能夠監視生產過程，通過訪問服務器獲取生產數據，可以迅速地掌握現場設備的工作狀態以及儲油庫內煤油的情況。直接控制層完成信號的分配、控制運算和執行控制命令等。現場設備層包括了儲油罐內智能溫度傳感器、流量傳感器、溫度傳感器、壓力傳感器和泵。通過傳感器完成信息量的采集，通過閥門開啟或關閉泵。 機場供油自控系統采用了冗余網絡結構，其中以太網網絡帶寬為100M，利用Modbus協議進行網絡通信，航油自控系統數據傳輸過程如下： 圖2 供油系統網絡拓撲簡圖 1)儲油罐內智能傳感器將測得航油參數上傳至Modbus服務器中。 2)工程師站從Modbus服務器獲取儲油罐內航油參數。 為保證機場供油自控系統能夠完成正常的生產流程，從完整性、可用性兩個方面對系統安全屬性進行描述，結合正常的工藝流程，控制系統應滿足以下安全條件： 1)機場供油自控系統應嚴格按照正常生產流程進行操作； 2)進油泵和送油泵開啟前，傳感器應處于工作狀態； 3)儲油罐內智能傳感器損壞，自控系統關閉油泵； 4)儲油罐內航油參數超過危險值時，自控系統關閉油泵； 根據歸納總結，系統安全屬性如表2所示。 表2 系統安全屬性 網絡攻擊分為主動攻擊與被動攻擊，主動攻擊通常帶有惡意的攻擊目的，破壞系統正常運行，造成巨大安全隱患[20]，主動攻擊通常可以分為以下四類：拒絕服務、消息篡改、偽裝、重放。 拒絕服務攻擊影響系統或通訊設備正常工作，讓目標計算機或網絡無法提供正常的服務或資源訪問，使目標系統服務系統停止響應甚至崩潰。消息篡改指對傳輸數據修改或者改變數據傳輸順序來進行攻擊。偽裝是一個實體冒充另一個實體，通常偽裝攻擊不會單獨出現，一般伴有其它類型的攻擊，例如偽裝成服務器截取傳輸數據，冒充合法服務器進行攻擊[21]。重放是攻擊人通過重新發送已經被認證過的消息來欺騙系統，從而完成身份認證。主動攻擊的攻擊方式以及攻擊結果如表3所示 表3 主動攻擊攻擊方式及結果 為了描述機場供油自控系統的工作流程，建立了多個時間自動機模型，每個時間自動機模型功能不同，各個時間自動機共同模擬供油自控系統。時間自動機由內部狀態節點和信號指令組成，自動機內部節點通過函數以及信號指令會自發的發生狀態之間的轉移。 機場供油自控系統共分為三個層次，分別是監控層，直接控制層，現場設備層，利用時間自動機理論分別對上述三個層次進行建模。 1)監控層模型 監控層模型當中包含了工程師站模型與Modbus服務器模型，工程師站對生產過程監控，Modbus服務器通過以太網將其它設備連接到計算機以及保存傳感器測得的數據。 ①工程師站時間自動機 工程師站可以創建、發送和接收響應，與Modbus服務器建立通信，工程師站時間自動機模型見圖3。 從Start開始，設置時鐘變量t=0，發送modbus＿c2s請求與Modbus服務器建立單向連狀態，如果等待時間超過20s，則判定為連接超時，進入Restart狀態準備重新開始。如果在20s內收到服務器發送的modbus＿s2c請求時，進入Connected狀態，說明此時已與Modbus服務器建立雙向通信，工程師站向服務器發送控制指令msg。 圖3 工程師站時間自動機 當工程師站接收數據時，首先向服務器發送data＿c2s請求進入Wait＿data狀態等待數據包，如果在30s內收到data＿s2c請求，完成一次建立通信的過程，工程師站通過Download指令從服務器下載數據； ②Modbus服務器時間自動機 Modbus服務器與接收到直接控制層傳輸來的數據信息，并由工程師站完成數據的下載，其時間自動機模型如圖4所示。 服務器接收工程師站發送的modbus＿c2s請求并向工程師站發送mobus＿s2c請求，完成一次與工程師站建立雙向通信，并接收控制指令msg。服務器接收控制器發送signal＿control請求并向其發送signal＿controlback請求，完成一次與直接控制層的雙向通信，利用update指令將數據從控制器上傳至服務器當中。通過data＿s2c請求、data＿c2s請求和download指令完成工程師站從服務期內獲取數據的過程。 2)直接控制層模型 圖4 Modbus服務器時間自動機 直接控制層作為機場供油自控系統的大腦，對生產過程完成自動控制。其行為過程見圖5。當控制器收到智能傳感器傳來的數據之后，有以下幾種自動控制行為。 如果儲油內傳感器所測得的參數正常，則不改變泵的工作狀態，通過向服務器發送signal＿control請求、接收signal＿control＿back請求，完成控制器與Modbus服務器的雙向通信，之后將傳感器測量到的煤油數據上傳到服務器當中。 如果儲油罐內傳感器所測的參數超過危險值，控制器向進油泵或送油泵發送signal＿stop＿pump＿in指令或者signal＿stop＿pump＿out指令，關閉油泵并通知工程師站。 如果沒有收到傳感器傳送的測量數據，表明傳感器損壞，控制器向進油泵和送油泵發送signal＿stop＿pump＿in指令以及signal＿stop＿pump＿out指令，關閉油泵并通過通知工程師站。 3)現場設備層模型 圖5 控制器時間自動機 現場設備層由儲油罐內的智能傳感器以及現場控制設備組成。智能傳感器是具有信息處理功能的傳感器，相對于僅提電壓信號的傳統傳感器，智能傳感器充分利用當代集成技術、微處理器技術，將感知、信息處理融為一體，能提供具有一定知識級別的信息[21]。 智能傳感器包括了智能溫度傳感器、智能壓力傳感器、智能流量傳感器、智能液位傳感器器。智能傳感器系統時間自動機模型如圖6所示，傳感器工作原理如圖5所示。 傳感器每10s鐘對油庫內煤油進行一次測量并進入Wait狀態，如果在10s內傳感器沒有測量到值，說明此時傳感器損壞，智能傳感器系統發送fault指令，控制器關閉油泵； 圖6 智能傳感器模型 如果智能傳感器系統在十秒內所測得數據超過危險值，智能傳感器系統向控制器發送back指令，控制器關閉油泵； 如果傳感器在10s內測的數據符合規定值，智能傳感器系統向控制器發送show＿level指令告知系統處于正常工作情況，并將測得的數據傳輸至控制器中。 現場控制設備由進油泵和送油泵組成，進油泵收到signal＿start＿pump＿in指令，進油泵閥門由Close狀態轉換到Open狀態，送油泵開啟； 圖7 控制設備模型 1) Synflood攻擊建模 Synflood攻擊屬于拒絕服務(Denial of Service，Dos)的一種，攻擊者利用Modbus/TCP傳輸協議當中TCP“三次握手”機制漏洞，對服務器進行攻擊。Synflood攻擊模型如圖8所示。 2) 篡改攻擊建模 圖8 Synflood攻擊模型 篡改攻擊模型見圖9，當攻擊者與控制器建立雙向通信之后，攻擊者通過向控制器發送控制指令，對原有的控制指令的進行篡改，影響控制器正常的控制行為。 3) 重放攻擊建模 圖9 篡改攻擊模型 重放攻擊是指攻擊者收集有效數據包并重新發送或延遲發送，從而欺騙系統，并通過網絡監聽來破壞身份認證過程，重放攻擊模型見圖10。 圖10 重放攻擊模型 1)防Synflood模塊 防Synflood攻擊措施見圖11，通過設立CloudFlare模塊代替服務器完成“三次握手”，保證服務器內沒有“半連接”消耗服務器網絡資源，從而避免服務器遭受到synflood攻擊。 2)防篡改模塊 圖11 防Synflood模型 防篡改模塊見圖12，通過過設置白名單機制，完成對篡改攻擊的防御。如果IP不是白名單內的IP，說明遭受到篡改攻擊，當對消息進行舍棄； 4) 防重放模塊 圖12 防篡改模型 針對重放攻擊，利用加隨機數的方法防重。服務器和控制器都定義一個初始序列號i，傳輸數據結束后，如果服務器接收到的i沒有變化，拋棄該請求； 圖13 防重放模型 實驗使用因特爾酷睿i5 5257U處理器CPU 2.70GHz，在Java13.0.1環境下安裝UPPAAL4.1.9，根據機場供油自控系統工作原理在UPPAAL建立時間自動機模型并驗證。 利用UPPAAL檢查器對系統進行安全性驗證，其中機場供油自控系統要滿足可用性、完整性、保密性。機場供油自控系統安全屬性結果如表4所示。 表4 系統驗證結果 從表7可以看出，系統在正常工作時，完整性、可用性滿足性質，供油自控系統運轉正常。但是Modbus協議在網絡上以明文方式傳輸，不存在加密以及身份認證的措施，不能夠通過UPPAAL驗證器對機場供油自控系統保密性進行驗證。 進而在航油自控系統中引入攻擊者模型，用Dos-Synflood攻擊、篡改攻擊、重放攻擊對系統進行破壞，并對其安全屬性進行驗證，驗證結果如表5所示。 表5 攻擊驗證結果 從表8可以看出，攻擊導致機場供油自控系統安全屬性變化：其中Dos-Synflood攻擊導致網絡無法提供正常的服務及資源訪問，傳感器測量數據無法傳遞，破壞系統完整性，但是沒有破壞系統的自控功能，可用性沒有遭到破壞； 在對機場自控系統設置一系列防御措施后，重新對系統的安全屬性進行驗證，驗證結果如表6所示。 表6 防御措施驗證結果 在引入以上三種防御措施后，自控系統的安全屬性恢復，具體來說：防Dos-Synflood攻擊措施恢復了系統的完整性，防篡改措施恢復了系統的完整性和可用性，防重放措施保證了自控系統數據不被泄露，保證了數據的完整性。 通過對比實驗可知，常見的網絡攻擊手段對系統的安全屬性均有影響：Dos-Synflood攻擊會導致系統內存耗盡，發生死鎖現象，對系統的完整性均造成影響。篡改攻擊導致工程師站發送給現場設備的命令被篡改，系統進入不可控狀態從而導致引發危險事件，破壞了系統的可用性。重放攻擊導致了系統數據包泄露，威脅到信息完整性。但是由于機場自控系統采用Modbus協議，該協議本身不具備身份認證與加密功能，系統的保密性不能夠被驗證。 針對以上三種攻擊方式，分別建立了防Dos-Synflood攻擊模塊、防火墻防篡改攻擊模塊、防重放攻擊模塊。驗證結果表明在引入防御措施后，系統已滿足的完整性、可用性的要求，系統的安全屬性恢復。對于保密性而言，防重放措施可以保護數據的可用性，增強系統的完整性。 本文基于時間自動機理論對機場供油自控系統建模，針對常見的網絡攻擊手段，構建Synflood攻擊模型、篡改攻擊模型和重放攻擊模型并對機場供油自控系統進行攻擊，在此基礎上建立相應的防御措施，利用UPPAAL軟件驗證機場供油自控系統在正常生產、遭受攻擊和引入防御措施后安全屬性的變化，發現Synflood攻擊影響系統完整性，篡改攻擊影響系統的完整性和可用性，重放攻擊影響系統的完整性。在引入防御措施后，機場供油自控系統的安全屬性恢復，在構建的防御措施下可以完成正常的工作，可見所構建的防御措施可以加強機場供油自控系統的安全性。但由機場供油自控系統采用Modbus明文傳輸協議，所以無法驗證系統保密性的變化，后續將對更為復雜的工控系統進行安全性分析與研究。
E是邊界的規則轉換集合。式(2)是時間自動機的Φ(A)是時鐘約束集合，其中c是有理數集合Q當中的任意元素，對A當中任意的元素a都有2.2 UPPAAL工具介紹
3.1 機場供油自控系統介紹
3.2 安全屬性
3.3 攻擊方式
4.1 時間自動機模型
4.2 機場供油自控系統建模
如果超過30s仍沒收到data＿s2c請求，則回到Restart狀態準備重新開始。
當接收到signal＿stop＿pump＿in指令，進油泵閥門由Open狀態轉換到Close狀態，進油泵關閉。進油泵和送油泵的時間自動機模型見圖7。
4.3 攻擊建模
4.4 防御措施建模
當IP地址是白名單內的IP地址，說明消息來自工程師站，對該信息保留。防篡改模型時間自動機見圖12。
如果服務器接收到的i滿足i=i+1，說明此時沒有遭到重放攻擊，重放防御模型時間自動機見圖13。
5.1 安全屬性驗證
5.2 存在攻擊者的模型驗證結果
篡改攻擊導致自控系統與現場設備通信受阻，攻擊者對設備進行自由控制，例如攻擊者篡改指令泵的閥門一直處于開啟狀態，導致正常指令無法傳遞，系統不能夠按照正常的業務邏輯進行控制，破壞了自控系統的完整性和可用性。重放攻擊通過將已發送的數據包進行重新發送，導致數據的泄露，破壞了系統的數據完整性，進而破壞了系統的完整性。5.3 防御措施下的模型驗證結果
