1　引言

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

　　2　工控代碼利用相關研究

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

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

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

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

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

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

　　3　PLC代碼缺陷分類

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

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

　　3.1　PLC代碼邏輯缺陷

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

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

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

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

　?。?）計時器條件競爭缺陷

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

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

　　圖1 計時器條件競爭缺陷梯形圖

　?。?）比較函數硬編碼缺陷

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

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

　　圖2 比較函數缺陷梯形圖

　?。?）跳轉和鏈接缺陷

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

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

　　圖3 跳轉和鏈接缺陷圖

　　3.2　PLC代碼安全需求規約

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

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

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

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

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

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

　?。?）PLC缺乏高級編程語言

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

　?。?）時間建模缺失

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

　?。?）物理環境建模缺失

　　工控系統與物理環境關系密切，工業控制器的輸入一般可以認為是物理環境的輸出，輸出一般可以認為是物理環境的輸入，構成一個閉環回路，不考慮物理環境就無法精確地模擬出工業控制器的行為。

　?。?）狀態空間爆炸

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

　　4.2　PLC代碼形式化分析

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

　　圖4 PLC控制代碼檢測的技術路線

　　4.2.1　中間語言翻譯

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

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

　　4.2.2　時間模型構建

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

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

　　4.2.3　模型檢測技術

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

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

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

　　5　結語

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