1　引言

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

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

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

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

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

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

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

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

　　3　PLC代碼缺陷分類

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

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

　　3.1　PLC代碼邏輯缺陷

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

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

　　表1 PLC代碼邏輯缺陷分類表

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

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

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

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

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

　　（2）比較函數(shù)硬編碼缺陷

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

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

　　圖2 比較函數(shù)缺陷梯形圖

　?。?）跳轉(zhuǎn)和鏈接缺陷

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

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

　　圖3 跳轉(zhuǎn)和鏈接缺陷圖

　　3.2　PLC代碼安全需求規(guī)約

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

　　表2 PLC代碼安全需求規(guī)約表

　　4　PLC代碼形式化分析與驗(yàn)證

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

　　形式化分析分為定理證明和模型檢測兩種方法,，定理證明過程過于復(fù)雜和冗繁,，實(shí)際中利用定理證明來驗(yàn)證PLC程序正確性的研究并未得到認(rèn)可。模型檢測是一種廣泛使用的形式化方法,，他更適合用于PLC代碼的驗(yàn)證,，相比于傳統(tǒng)的計(jì)算機(jī)程序，對(duì)低級(jí)的PLC程序建模會(huì)更容易,，因?yàn)樗臓顟B(tài)轉(zhuǎn)換系統(tǒng)相對(duì)簡單,。

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

　　（1）PLC缺乏高級(jí)編程語言

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

　?。?）時(shí)間建模缺失

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

　?。?）物理環(huán)境建模缺失

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

　?。?）狀態(tài)空間爆炸

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

　　4.2　PLC代碼形式化分析

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

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

　　4.2.1　中間語言翻譯

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

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

　　4.2.2　時(shí)間模型構(gòu)建

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

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

　　4.2.3　模型檢測技術(shù)

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

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

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

　　5　結(jié)語

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