耿洋洋，常天佑，魏強 解放軍信息工程大學(xué)

1　引言

工業(yè)控制系統（Industrial control system，ICS）是國家基礎設施的核心并廣泛用于工業(yè)、交通、能源、水利、安防、食品以及大型制造等行業(yè)，工業(yè)控制系統的網(wǎng)絡(luò )安全與國家安全息息相關(guān)[1]。2010年“震網(wǎng)”[2]（stuxnet）病毒造成了伊朗布什爾核電站重大損失，大量離心機報廢，導致伊朗的核計劃推遲，也促使工業(yè)控制系統安全逐漸成為網(wǎng)絡(luò )安全領(lǐng)域的研究熱點(diǎn)。隨著(zhù)工業(yè)控制系統由封閉走向互聯(lián)[3]，大量的控制器配備了以太網(wǎng)通信組件，使得攻擊者可以直接訪(fǎng)問(wèn)PLC硬件及其編程軟件。但PLC邏輯控制層缺少認證和監測等保護措施，PLC代碼的安全缺陷成為工業(yè)控制系統的重要安全威脅之一。

2　工控代碼利用相關(guān)研究

與傳統的編程語(yǔ)言一樣，PLC存在代碼安全缺陷，而這些代碼安全缺陷為攻擊者攻擊工業(yè)控制系統留下了后門(mén)。

2013年South Carolina大學(xué)的Sidney對PLC代碼設計安全缺陷進(jìn)行了深入的研究[4]，并把PLC代碼設計級缺陷主要分為基于硬件缺陷和基于軟件缺陷兩種。攻擊者可以利用PLC代碼缺陷破壞代碼邏輯，進(jìn)行中間代碼插樁，實(shí)現任意代碼執行等。

2014年北京科技大學(xué)李偉澤等[5]提出和分析了一種針對SCADA系統的新型的網(wǎng)絡(luò )物理攻擊——偽邏輯攻擊。

2015年在blackhat-US會(huì )議上Klick等在西門(mén)子S7-300中注入了一種新型的后門(mén)[6]，通過(guò)注入工具實(shí)現了在S7-300上進(jìn)行SNMP掃描及SOCK5代理功能。作者利用PLC程序中存在跳轉指令的安全缺陷，成功在主程序OB1前嵌入惡意指令從而可以控制PLC的啟停以及輸出寄存器。

2016年11月在blackhat歐洲會(huì )議上Ali Abbasi等[7]實(shí)現了對PLC輸入/輸出接口的新攻擊，該攻擊通過(guò)篡改輸出輸入引腳改變系統的運行邏輯。

2017年3月，來(lái)自印度海德拉巴和新加坡的學(xué)者，演示了針對工業(yè)控制系統的PLC梯形圖邏輯炸彈（Ladder Logic Bombs，LLB）[8]。該邏輯炸彈是用梯形圖語(yǔ)言編寫(xiě)的惡意軟件，這種惡意軟件可被攻擊者注入到PLC現有控制邏輯中，通過(guò)改變控制動(dòng)作或者等待特定的觸發(fā)信號來(lái)激活?lèi)阂庑袨?，以?shí)現傳感器數據篡改，系統敏感信息獲取以及PLC拒絕服務(wù)攻擊等。

3　PLC代碼缺陷分類(lèi)

不同于傳統的IT系統，工業(yè)控制系統有其特殊的編程語(yǔ)言，根據國際電工委員會(huì )制定的工業(yè)控制編程語(yǔ)言標準（IEC61131-3）[9]，PLC的編程語(yǔ)言包括以下五種：梯形圖語(yǔ)言（LadderLogic Programming Language，LD）、指令表語(yǔ)言（Instruction List，IL）、功能模塊圖語(yǔ)言（Function Block Diagram，FBD）、順序功能流程圖語(yǔ)言（Sequential function chart，SFC）及結構化文本語(yǔ)言（Structured text，ST）。本文中的代碼缺陷研究也是基于上述編程語(yǔ)言展開(kāi)的。

工業(yè)控制系統的入侵與傳統互聯(lián)網(wǎng)入侵雖然手段上大同小異，但工業(yè)控制系統的部署與其物理工藝流程緊耦合，因此利用工藝流程中的代碼邏輯缺陷成為針對工業(yè)控制系統的有效打擊手段之一，如陷阱門(mén)、邏輯炸彈、特洛伊木馬、蠕蟲(chóng)、Zombie等，且這類(lèi)新的惡意代碼具有更強的傳播能力和破壞性。本文主要研究基于軟件的PLC代碼缺陷，并從代碼邏輯缺陷和違反安全需求規約兩個(gè)方面對PLC代碼缺陷進(jìn)行分類(lèi)研究。

3.1　PLC代碼邏輯缺陷

PLC代碼邏輯缺陷具有隱蔽性強的特性，難以發(fā)現，可以潛伏多年，傳統的安全防御思路無(wú)法解決這方面問(wèn)題。在工業(yè)控制系統中，一次開(kāi)關(guān)動(dòng)作不執行，工藝執行流程的改變以及特定的輸出響應故障都可能造成毀滅性的破壞。

本文以梯形圖語(yǔ)言為例分析PLC代碼邏輯缺陷，梯形圖語(yǔ)言形象直觀(guān)，與繼電器的控制電路的表達方式極為相似[10]。梯形圖由觸點(diǎn)、線(xiàn)圈等圖形符號結合數字指令、算術(shù)運算指令、控制指令等指令符號構成，PLC代碼邏輯缺陷也是由這些元素和組件位置放置不恰當、鏈接和范圍不正確引起的[4]。表1給出了PLC代碼邏輯缺陷分類(lèi)及其相關(guān)描述。

表1 PLC代碼邏輯缺陷分類(lèi)表

通過(guò)利用表1中列舉的PLC代碼邏輯缺陷，可實(shí)現拒絕服務(wù)攻擊，中間人攻擊、改變控制器正常的工作流程等，對工業(yè)控制系統造成難以估量的損失。下面給出幾個(gè)PLC代碼缺陷分析和利用。

（1）計時(shí)器條件競爭缺陷

PLC編程中的計時(shí)器可通過(guò)設置預設時(shí)間觸發(fā)計時(shí)器。定時(shí)器完成位元件的不正確放置可能導致涉及定時(shí)器完成位的過(guò)程和定時(shí)器本身進(jìn)入競爭條件。當定時(shí)器完成位成為激活其自身觸發(fā)機制的必需元素時(shí)，發(fā)生這種競爭條件使得定時(shí)器陷入死循環(huán)并使定時(shí)器復位。

如圖1所示，把計時(shí)器的預設值設為0，使得定時(shí)器觸發(fā)位和定時(shí)器同時(shí)打開(kāi)，造成計時(shí)器持續振蕩，使得輸出O4.1無(wú)法被觸發(fā)，致使程序流程順序錯誤或進(jìn)程無(wú)法關(guān)閉等故障，實(shí)現拒絕服務(wù)攻擊。

圖1 計時(shí)器條件競爭缺陷梯形圖

（2）比較函數硬編碼缺陷

PLC邏輯代碼中的數字指令包含比較指令，該比較指令如果編碼不正確可能會(huì )導致安全隱患，使得惡意用戶(hù)可以通過(guò)比較指令將不正確的數據插入到進(jìn)程中。這些數據可能會(huì )導致進(jìn)程序列發(fā)生變化，或者導致進(jìn)程完全中止。

如圖2所示，假設常開(kāi)觸點(diǎn)I0.1可以觸發(fā)高壓鍋爐的初始化，常開(kāi)觸點(diǎn)后連接一個(gè)比較函數，O4.1控制高壓鍋爐的關(guān)閉進(jìn)程。直到A的值大于等于B的值時(shí)，O4.1被激活，鍋爐停止加熱。如果比較元素B不參考符號表中的數值而是使用定值進(jìn)行硬編碼，B中的數據是不受保護的，我們通過(guò)提高B的溫度值，使得高壓鍋爐不斷加熱直到設備損壞甚至發(fā)生爆炸。

圖2 比較函數缺陷梯形圖

（3）跳轉和鏈接缺陷

跳轉和鏈接缺陷是由一些可影響程序執行順序的跳轉指令和邏輯塊指令的錯誤的跳轉到某個(gè)程序段而引起。這種類(lèi)型的代碼缺陷類(lèi)似于中間人攻擊，攻擊者可以利用錯誤的跳轉指令跳轉到一個(gè)非預期的位置，并且把在非預期的位置插入惡意的程序段，再返回到跳轉之前的位置。

圖3給出了基于跳轉和鏈接缺陷的代碼利用方法，我們可以利用跳轉到子程序JSR函數從File1跳轉到惡意代碼文件File3中，引入惡意的子程序再返回到JSR跳轉之前位置，完成惡意代碼的插入，實(shí)現中間人攻擊。

圖3 跳轉和鏈接缺陷圖

3.2　PLC代碼安全需求規約

除了PLC代碼邏輯缺陷，PLC代碼在物理現場(chǎng)的安全需求屬性也將決定PLC缺陷利用的成功與否。安全需求屬性是由工業(yè)控制現場(chǎng)的安全要求決定，指的是為了保證工業(yè)控制系統的安全，對設備狀態(tài)、時(shí)序、時(shí)間、輸入輸出量等的約束。如一個(gè)電機的額定轉速不超過(guò)2000rpm以及交叉路口的綠燈不能同時(shí)點(diǎn)亮等約束條件。在代碼中可能由于程序員的疏忽導致違反安全需求屬性的情況，就需要對其進(jìn)行檢測?？梢?jiàn)安全需求屬性不是常量，而需要實(shí)際用戶(hù)進(jìn)行描述并輸入到檢測器中。Pavlovic等[11]對PLC的設備狀態(tài)、時(shí)序、時(shí)間、輸入輸出量等安全需求進(jìn)行了約束。本文將安全需求總結為分為以下五類(lèi)，如表2所示。

表2 PLC代碼安全需求規約表

4　PLC代碼形式化分析與驗證

PLC代碼采用“順序掃描，不斷循環(huán)”的工作方式，典型的PLC的工作過(guò)程包括三個(gè)不同階段：把輸入數據讀入存儲器、處理存儲器中的數據和更新輸出數據。PLC程序僅包含有限的狀態(tài)集合和有限的變量，且程序內部不包含循環(huán)，安全需求依賴(lài)于輸出變量等，所以在一定程度上形式化驗證技術(shù)適用于PLC程序安全分析和惡意代碼檢測。

形式化分析分為定理證明和模型檢測兩種方法，定理證明過(guò)程過(guò)于復雜和冗繁，實(shí)際中利用定理證明來(lái)驗證PLC程序正確性的研究并未得到認可。模型檢測是一種廣泛使用的形式化方法，他更適合用于PLC代碼的驗證，相比于傳統的計算機程序，對低級的PLC程序建模會(huì )更容易，因為他的狀態(tài)轉換系統相對簡(jiǎn)單。

4.1　PLC形式化分析中面臨的困難

（1）PLC缺乏高級編程語(yǔ)言

PLC編程屬于低級編程語(yǔ)言且編程語(yǔ)言眾多，語(yǔ)法語(yǔ)義晦澀，采用分層尋址，地址尋址復雜，存在隱式的類(lèi)型數據，建模難度大，語(yǔ)言屬性易丟失。

（2）時(shí)間建模缺失

工業(yè)控制系統的實(shí)時(shí)性要求很高，因此對時(shí)間進(jìn)行建模極為重要，時(shí)間建模的對象應包括定時(shí)器的累積時(shí)間、單條指令的運行時(shí)間和執行周期時(shí)間，由于定時(shí)器是跨循環(huán)周期的全局變量，建模時(shí)將時(shí)間考慮在內會(huì )極大地提高建模的難度并增加檢測的時(shí)間，但不考慮時(shí)間就無(wú)法檢測出與時(shí)間相關(guān)的安全規約。

（3）物理環(huán)境建模缺失

工控系統與物理環(huán)境關(guān)系密切，工業(yè)控制器的輸入一般可以認為是物理環(huán)境的輸出，輸出一般可以認為是物理環(huán)境的輸入，構成一個(gè)閉環(huán)回路，不考慮物理環(huán)境就無(wú)法精確地模擬出工業(yè)控制器的行為。

（4）狀態(tài)空間爆炸

PLC代碼包含的變量多，狀態(tài)空間大，對PLC代碼進(jìn)行建模分析是建立在狀態(tài)轉化基礎上的，如果直接進(jìn)行模型檢測會(huì )造成狀態(tài)空間爆炸的問(wèn)題。

4.2　PLC代碼形式化分析

PLC代碼形式化驗證旨在檢測出PLC代碼缺陷，防止惡意代碼的入侵。目前通過(guò)形式化驗證方式發(fā)現PLC代碼缺陷的研究主要集中于對PLC代碼形式化模型構建、PLC代碼缺陷及安全需求規約描述以及PLC代碼模型檢測技術(shù)的研究，如圖4所示。

圖4 PLC控制代碼檢測的技術(shù)路線(xiàn)

4.2.1　中間語(yǔ)言翻譯

由于工業(yè)控制器支持多種標準編程語(yǔ)言，且語(yǔ)法語(yǔ)義上都有較大差異，現有的模型檢測技術(shù)大都基于特定的編程語(yǔ)言，為了降低建模的復雜性，我們需要把PLC編程語(yǔ)言轉化成模型檢測器可以處理的中間語(yǔ)言。

Darvas等[12～15]提出了將PLC程序的SCL語(yǔ)言轉化為基于NuSMV的中間模型方法，它是一種接近于自動(dòng)機模型的中間模型。McLaughlin等[16]給出了將PLC的指令表IL語(yǔ)言代碼翻譯為基于Vine的中間語(yǔ)言ILIL的方法。Zonouz等[17]通過(guò)反編譯的方法將MC7code轉化為中間語(yǔ)言ILIL，該中間語(yǔ)言ILIL同樣使用BitBlaze[18]二進(jìn)制分析工具Vine插件來(lái)描述。

4.2.2　時(shí)間模型構建

工業(yè)控制系統的實(shí)時(shí)性要求很高，因此時(shí)間是很重要的建模對象。延時(shí)寄存器（On-Delay Timer，TON）用于確保PLC中實(shí)時(shí)性屬性，TON指令為PLC的輸入信號提供延遲機制。對TON計時(shí)器建模會(huì )極大地提高建模的難度并增加檢測的時(shí)間，但不考慮時(shí)間就無(wú)法檢測出與時(shí)間相關(guān)的安全規約。因此對TON計時(shí)器的形式化驗證成為PLC代碼形式化驗證的瓶頸之一。

近年來(lái)也有一些對T ON 計時(shí)器的建模研究，Masder等[19～20]最早開(kāi)始這方面的研究，他們將IL程序轉換為時(shí)間自動(dòng)機模型并使用自動(dòng)機和Prometa模型兩種方式對計時(shí)器建模。Willems[21]使用時(shí)間自動(dòng)機對TON模型建模計來(lái)解決關(guān)于TON的問(wèn)題。Wan等[22～23]在定理證明器Coq中針對梯形圖語(yǔ)言對TON計時(shí)器進(jìn)行形式化驗證，但沒(méi)有給出通用模塊的PLC程序形式化描述。Sidi[24]在定理證明器Coq中針對指令表語(yǔ)言對TON計時(shí)器進(jìn)行形式化驗證。

4.2.3　模型檢測技術(shù)

模型檢測是一種廣泛使用的自動(dòng)化驗證技術(shù)，選擇合適的模型來(lái)驗證系統，并且通過(guò)系統地探測建模來(lái)檢查所要驗證的所需屬性。由于模型檢測可以自動(dòng)執行，并能在系統不滿(mǎn)足性質(zhì)時(shí)提供反例路徑，因此在工業(yè)界比演繹證明更受推崇。模型檢測在PLC系統安全的驗證方面特別有用，因為與傳統的計算機編程相比，可以更容易地將低級PLC代碼建模為狀態(tài)轉換系統。

目前研究中用到的模型檢測工具有很多， 如SMV、UPPAAL、SPIN等。Yoo等[25]使用Verilog模型和CadenceSMV模型對核電站控制系統的PLC代碼進(jìn)行模型檢查。McLaughlin等[16]開(kāi)發(fā)了一個(gè)TSV（Trusted Safety Verifier）工具，該工具是利用TEG（Temporal Execution Graph）圖來(lái)進(jìn)行模型檢測，在原始的IL代碼對輸出變量賦值再轉換到ILII中間語(yǔ)言，依據被給的安全需求，TSV使用生成的TEG圖來(lái)決定具體的原子命題值。Zonouz等[26]同樣利用TEG圖的方法進(jìn)行模型檢測，先對線(xiàn)性時(shí)序邏輯規范公式進(jìn)行取反接著(zhù)得到TEG-UR圖模型P，然后在模型M中搜尋滿(mǎn)足的路徑，最后，如果在第三步中不存在任何路徑，則可認為原始代碼滿(mǎn)足安全需求，能夠安全地執行。如果存在路徑，則可以通過(guò)違反約束的路徑條件得到相應的反例。

實(shí)際開(kāi)發(fā)的PLC程序包含的多個(gè)變量和狀態(tài)空間，執行路徑較復雜。會(huì )遇到狀態(tài)空間爆炸的問(wèn)題。解決狀態(tài)空間爆炸問(wèn)題最有效的方法是符號執行，McLaughlin等[16]提出一種合并具有相同輸出的輸入來(lái)避免等價(jià)狀態(tài)生成的狀態(tài)聚合方法。Guo等[27]提出了一種用于自動(dòng)測試PLC編程語(yǔ)言符號執行工具SymPLC。SymPLC將PLC源代碼作為輸入，并在應用符號執行之前將其轉換為C語(yǔ)言，以系統的生成測試輸入來(lái)覆蓋每個(gè)周期任務(wù)中的所有路徑。為此，他們提出了一些PLC特定縮減技術(shù)，用于識別和消除冗余。

5　結語(yǔ)

在工業(yè)控制系統中，一個(gè)微小的代碼缺陷可能影響到整個(gè)工業(yè)流程遭受破壞甚至威脅到生命財產(chǎn)安全。本文圍繞著(zhù)工業(yè)控制系統控制代碼安全展開(kāi)研究，從PLC代碼邏輯缺陷、代碼安全需求規約兩個(gè)方面對工控代碼缺陷進(jìn)行分類(lèi)，并結合了現實(shí)中常見(jiàn)的梯形圖邏輯缺陷構造了代碼利用場(chǎng)景，基于這些代碼邏輯缺陷實(shí)現了對工業(yè)控制系統的拒絕服務(wù)攻擊，中間人攻擊等。PLC代碼形式化驗證是發(fā)現PLC代碼缺陷的一種重要且有效的方法，文章最后圍繞著(zhù)如何實(shí)現，簡(jiǎn)要從中間語(yǔ)言翻譯，時(shí)間模型構建和模型檢測技術(shù)三個(gè)方面闡述了PLC代碼形式化驗證的技術(shù)路線(xiàn)及研究進(jìn)展。

作者簡(jiǎn)介

耿洋洋（1994-）男，河南太康人，研究生在讀，現就讀于解放軍信息工程大學(xué)，主要研究方向為工控安全。

常天佑（1992-）男，河南駐馬店人，研究生在讀，現就讀于解放軍信息工程大學(xué)，主要研究方向為工控安全。

魏強（1979-）男，江西南昌人，副教授，博導，現就職于解放軍信息工程大學(xué)，主要研究方向為軟件脆弱性分析、工控安全。

參考文獻：

[1] 陳冬青, 彭勇, 謝豐. 我國工業(yè)控制系統信息安全現狀及風(fēng)險[J]. 中國信息安全, 2012 (10) : 64 - 70.

[2] James P. Farwell, Rafal Rohozinski. Stuxnet and the Future of Cyber War[J]. Survival, 2011, 53 (1) : 23 - 40.

[3] 王繼業(yè). 工業(yè)控制系統的信息安全[J]. 電力信息與通信技術(shù), 2012, 10 (7) : 7 - 7.

[4] Valentine S E. PLC code vulnerabilities through SCADA systems [C] . University of South Carolina, 2013.

[5] Li W, Xie L, Liu D, et al. False Logic Attacks on SCADA Control System [C] . Services Computing Conference. 2014:136 - 140.

[6] Klick J, Lau S, Marzin D, et al. Internet-facing PLCs a new back orifice [J] . Blackhat USA, 2015.

[7] Ali Abbasi，Majid Hashemi.Ghost in the PLC Designing an Undetectable Programmable Logic Controller Rootkit via Pin Control Attack [C] .blackhat,2016.

[8] Govil N, Agrawal A, Tippenhauer N O. On Ladder Logic Bombs in Industrial Control Systems [J] . 2017.

[9] John K H, Tiegelkamp M. IEC 61131-3: Programming Industrial Automation Systems [M] . Springer Berlin Heidelberg, 2010.

[10] 陳輝, 李堅強, 裴海龍,等. 基于梯形圖語(yǔ)言的軟PLC技術(shù)研究與實(shí)現[J]. 微計算機信息, 2006, 22 (25) : 266 - 268.

[11] O Pavlovic，R Pinger，M Kollmann.Automated Formal Verification of PLC Programs Written in IL [J] .Conference on Automated Deduction，2007.

[12] Darvas D, Adiego B F, Vi uela E B. Transforming PLC programs into formal models for verification purposes [J] . 2013.

[13] Darvas D, Adiego B F, V r s A, et al. Formal verification of complex properties on PLC programs[M]. Formal Techniques for Distributed Objects, Components,and Systems. 2014: 284 - 299.

[14] Adiego B F, Darvas D, Tournier J C, et al. Bringing Automated Model Checking to PLC Program Development — A CERN Case Study [J]. IFAC Proceedings Volumes, 2014, 47(2): 394 - 399.

[15] Darvas D, Majzik I, Vi uela E B. Formal Verification of Safety PLC Based Control Software[M]. Integrated Formal Methods. Springer International Publishing, 2016.

[16] Mclaughlin S. A Trusted Safety Verifier for Process Controller Code[C]. Network and Distributed System Security Symposium, 2014.

[17] Zonouz S, Rrushi J, Mclaughlin S. Detecting Industrial Control Malware Using Automated PLC Code Analytics[J]. IEEE Security & Privacy, 2014, 12 (6) : 40 - 47.

[18] Song D, Brumley D, Yin H, et al. BitBlaze: A New Approach to Computer Security via Binary Analysis[C]. Information Systems Security, International Conference, Iciss 2008, Hyderabad, India, December 16 - 20, 2008. Proceedings. DBLP, 2008 : 1 - 25.

[19] Mader A, Wupper H. Timed Automaton Models for Simple Programmable Logic Controllers[C]. Real-Time Systems, 1999. Proceedings of the, Euromicro Conference on. CiteSeer, 2017 : 106 - 113.

[20] Mader A, Brinksma E, Wupper H, et al. Design of a PLC Control Program for a Batch Plant VHS Case Study 1[J]. European Journal of Control, 2001, 7 (4) : 416 - 439.

[21] Willems H X. Compact Timed Automata for PLC Programs[J]. 1999.

[22] Wan H, Chen G, Song X, et al. Formalization and Verification of PLC Timers in Coq[C]. IEEE International Computer Software and Applications Conference.IEEE Computer Society, 2009 : 315 - 323.

[23] Wan H, Song X, Gu M. Parameterized Specification and Verification of PLC Systems in Coq[C]. International Symposium on Theoretical Aspects of Software Engineering. IEEE, 2010 : 179 - 182.

[24] Biha S O. A Formal Semantics of PLC Programs in Coq[C]. IEEE, Computer Software and Applications Conference. IEEE Computer Society, 2011 : 118 - 127.

[25] Yoo J, Cha S, Jee E. A Verification Framework for FBD Based Software in Nuclear Power Plants[C]. Software Engineering Conference, 2008. APSEC '08. Asia-Pacific. IEEE, 2008 : 385 - 392.

[26] Zonouz S, Rrushi J, Mclaughlin S. Detecting Industrial Control Malware Using Automated PLC Code Analytics[J]. IEEE Security & Privacy, 2014, 12 (6) : 40 - 47.

[27] Guo S, Wu M, Wang C. Symbolic execution of programmable logic controller code[C]. Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering. ACM, 2017 : 326 - 336.

摘自《工業(yè)控制系統信息安全》專(zhuān)刊第四輯