?

PLC程序控制流分析方法

2018-01-08 07:33陸余良
計算機應用 2017年12期
關鍵詞:控制流副作用語句

張 曄,陸余良

(合肥電子工程學院 ,合肥 230037)

PLC程序控制流分析方法

張 曄*,陸余良

(合肥電子工程學院 ,合肥 230037)

可編程邏輯控制器(PLC)是工業控制系統的重要組成部分,控制著各類物理設備及工藝流程。無論是攻擊者的惡意篡改還是內部人員的編程錯誤所造成的PLC控制程序錯誤都將嚴重威脅設備及人身安全。為解決該問題,提出了針對PLC程序的控制流分析方法。首先,利用flex和bison分析了源代碼的詞法及語法結構;其次,通過分析抽象語法樹(AST)生成并優化了不含指令副作用的中間表示;最后,在中間表示的基礎上劃分基本塊,并以此為基本單元構建了程序的控制流圖。實驗結果表明,所提方法能夠恢復語句表形式PLC程序的控制流結構,為程序理解和安全性分析提供了基礎。

可編程邏輯控制器;控制流;中間表示;程序理解;安全性

0 引言

自“震網”病毒面世以來,人們對工業控制系統安全的認識達到了前所未有的高度。作為工業控制系統的核心組件,可編程邏輯控制器(Programmable Logic Controller, PLC)關系著整個工業現場的運轉秩序,同時也影響著財產、人身安全,其安全性保障也具有較高需求,因此PLC控制邏輯程序也往往成為攻擊者的惡意篡改對象。與此同時,針對PLC程序的形式化分析、靜態分析等程序分析方法成為了人們廣泛研究的課題。

控制流分析是一類用于分析程序控制流結構的靜態分析技術,目的在于生成程序的控制流圖,在編譯器設計、程序分析、程序理解等領域都有重要應用。針對PLC程序的控制流分析實際上分析的是工業控制系統中離散事件的先后執行順序和狀態的轉換條件,也是各類PLC程序分析方法的基礎。

本文針對西門子S7系列PLC所使用的STL(STatement List)語言展開研究,開發了STL代碼的控制流分析工具。STL也被稱為語句表,衍生于IEC 61131-3[1]標準中的指令表語言,是一種類似于匯編語言的私有結構化語言。

1 相關研究

當前針對PLC程序的分析方法主要有模型檢測[2-4]、靜態分析[5-6]、定理證明[7-8]、符號執行[9]等。

模型檢測主要用于驗證程序有窮狀態是否滿足命題性質,文獻[4]基于抽象解釋理論、反例引導的抽象求精算法設計了具備模型檢測和靜態分析功能的形式化驗證平臺Arcade.PLC,能夠兼容IEC 61131- 3標準中的所有語言以及西門子的STL及ST語言。CERN基于NuSMV和nuXmv模型檢測引擎開發的模型檢測工具PLCverif[2]還支持西門子的SFC、SCL等高級語言,但該工具還處于概念驗證階段。

當前針對PLC程序的靜態分析利用了控制流、數據流分析等技術,主要應用于程序語法規范性的驗證。

文獻[7-8]采用定理證明的方法將PLC程序轉化為數學公式,并用定理證明器進行分析與驗證。

文獻[9]利用符號執行的方法分析程序的路徑約束,通過約束求解計算滿足目標約束的具體值,消除了不可達路徑的訪問,有效解決了PLC程序模型檢測中狀態爆炸的問題。

上述的大部分工作都為PLC程序的驗證與分析奠定了良好的基礎,但仍然存在兩個問題:

1)在程序建模的過程中重點闡述了程序分析后端內容,對代碼解析部分介紹得不夠詳細。

2)分析并未采用中間語言,而是基于源碼進行建模,指令副作用導致了建模規則復雜、狀態空間爆炸等問題。

本文針對這兩個問題,提出了一種消除語義副作用的STL語言中間表示(Simple STL language Intermediate Representation, SSIR),在不改變STL語義的前提下將STL代碼表示成SSIR形式,之后在SSIR的基礎上進行相應的控制流分析,有效實現了程序的控制流恢復,使后端工作僅需要在控制流圖的基礎上進行即可。

2 控制流分析框架

控制流分析框架如圖1所示,主要分為以下幾個步驟:

1)利用詞法分析生成器flex對STL程序進行詞法分析,生成相應的token序列。

2)基于bison對token序列進行語法分析,構造程序的抽象語法樹(Abstract Syntax Tree, AST)。

3)遍歷抽象語法樹生成中間表示SSIR。

4)在中間表示的基礎上劃分基本塊,構建程序控制流圖用于過程內分析。

圖1 控制流分析框架Fig. 1 Framework of control flow analysis

由于前兩步的工作已公開發表不再贅述,本文主要介紹中間表示的生成與優化以及所面臨的主要困難,并給出了程序的控制流圖生成算法。

3 中間表示生成與優化

STL源代碼不適合直接用于控制流分析,主要因為源代碼的指令副作用使得程序控制流不夠清晰[9],因此,在完成語法分析后,通過遍歷抽象語法樹生成無指令副作用的中間表示SSIR。本章首先介紹了STL程序基本單元,隨即舉例介紹了源代碼中存在的指令副作用,之后介紹了中間表示的語法格式,最后列舉了中間表示生成過程中STL特有元素的翻譯規則。

3.1 STL程序基本單元

3.1.1 邏輯塊

邏輯塊是STL程序的基本單元,不僅包含用戶編寫的程序,而且包含程序操作所需的數據。用戶可編輯的部分主要有組織塊(OB)、功能(FC)、功能塊(FB)、數據塊(DB)等,具體功能如下:

1)組織塊相當于用戶程序中的主程序,可以調用其他塊,是操作系統與用戶的接口,用于控制掃描循環、中斷程序、PLC的啟動和錯誤處理等,決定了用戶程序的結構。

2)功能和功能塊類似于函數,通過其輸入、輸出參數實現與過程控制的傳感器、執行器、用戶程序中的其他塊交換數據,主要區別在于功能塊有獨立的背景數據塊。

3)數據塊是用于存放用戶數據的數據區域。

3.1.2 程序狀態字與累加器

STL程序主要依賴于程序狀態字寄存器、累加器兩類寄存器執行指令操作。

狀態字是一個16位的寄存器,實際上僅使用了其中的9位,用于存儲CPU執行指令后的狀態、結果以及錯誤,幾乎所有位邏輯運算指令在執行過程中都要與程序狀態字進行交互。用戶一般不直接使用狀態位,但是PLC在解釋執行代碼時會對狀態字進行隱式的寫操作,從而影響了后續指令的執行結果。狀態字的具體描述如表1所示。

表1 程序狀態字Tab. 1 Program status word

累加器(ACCUx)是執行STL指令操作的關鍵部件。除位邏輯運算以外,大部分語句表操作都是在累加器中進行[10]。不同PLC型號的累加器數目不同,本文以兩個累加器的為例介紹STL指令的副作用。

3.2 指令副作用

STL語言的指令副作用主要源于狀態字,對狀態位的隱式讀寫操作由PLC解釋執行,其增加了程序的條件分支,但并未顯式地表現在代碼中。

例如圖2所示,雙斜杠后的內容表示指令的隱式操作。與操作“A”將操作數的布爾值賦予狀態寄存器STA,第3行根據該指令是否是邏輯串的首指令來決定后續的指令流向,這就是指令副作用產生的額外控制流。為了減少副作用引起的額外控制流,需要對部分指令進行預處理及優化,最為主要的有FC狀態位和OR狀態位。

3.2.1 FC狀態位

FC狀態位為0表示該行指令是邏輯串的首指令,與RLO相關的操作將STA狀態值直接賦予RLO;否則,RLO則需要與STA位進行相應的邏輯操作后再將值賦予RLO。輸出指令或與RLO有關的跳轉指令將其置位為0,表示邏輯串結束。

除狀態字傳送指令、O先“與”后“或”指令[10]、調用背景塊指令以外,FC狀態位值均取決于操作符而非操作值。因此,在源代碼翻譯為中間表示之前,僅需要對源代碼進行一次遍歷,標記執行前FC位為0的指令行號,之后行號已被標記的指令便可直接采用相應的翻譯規則,從而省略多余的條件分支語句。預處理規則如下:

1)首行指令執行前FC位為0。

2)賦值、置位、復位指令下一條指令若非跳轉目標,則執行前FC位為0。

3)與RLO相關的跳轉指令的下一條指令若非跳轉目標,則執行前FC位為0。

4)除裝載指令以外的計數器指令的下一條指令非跳轉目標,則執行前FC位為0。

圖2 STL指令副作用Fig. 2 Instruction side effects of STL

3.2.2 OR狀態位

OR位主要功能是在O先“與”后“或”指令中保存之前“與”操作的運算結果,若運算結果為1,則OR位值為1,后續若無將OR位復位的指令,RLO值一直為1。

因此,需要在每條對RLO賦值的指令后添加“RLO=RLO or OR”指令,以此替代冗余的條件判斷。實際上,OR位在多數情況下為常量0,也意味著該指令無效,所以可以在中間表示的優化過程中檢測同一基本塊中該條指令前OR是否為0,若為0則刪除該條指令。

3.3 SSIR語法規則

中間表示SSIR抽象語法規則用巴科斯范式表示如圖3所示。

圖3 SSIR語法規則Fig. 3 Syntax rules of SSIR

prog表示構成程序的邏輯塊結構,ins代表指令,包括跳轉指令jmp id、條件跳轉指令cjmp id,exp、功能調用指令call id、功能塊調用指令call id,id、塊結束指令BE、帶有標簽的指令label: 、賦值指令:=。exp為表達式,包含了變量、變量的二元運算、變量的一元運算。條件調用指令用于實現組織塊對功能、功能塊的條件調用。pop和push指令用于嵌套指令的堆棧操作,在3.4.5節詳細介紹。

實際上,SSIR僅對STL源代碼進行了局部優化,并且以四元式作為存儲結構。STL源代碼的指令結構包括了標簽、操作符、至多一個操作數、注釋。SSIR在STL的基礎上消除了注釋信息,為了消除指令副作用,SSIR增加至三個操作數,包括一個目的操作數和至多兩個源操作數。

3.4 特有元素的翻譯規則

與一般程序相比,STL具備一些特有的元素,在生成中間表示時需要得到相應的處理。下面介紹STL特有元素的翻譯規則。

3.4.1 定時器

不同類型的定時器具備不同功能,西門子S7系列PLC為每個定時器都分配一個16位字和一個二進制位。定時器的16位字用于存放剩余時間值,二進制位表示定時器輸出觸點狀態,根據定時器的類型在滿足相應條件時發生跳變。 SSIR根據操作符類型判定程序訪問的是邏輯值還是具體數值。

3.4.2 計數器

計數器的主要功能是在滿足預置的指定數目脈沖后進行某種操作。西門子S7系列PLC為每個計數器都分配一個16位字和一個二進制位。計數器的16位字用于存放當前數值。計數器值大于0時,二進制位為1;反之為0。因此,SSIR對計數器的處理與定時器相同。

3.4.3 邊沿檢測指令

某些指令在特定的內存單元值發生高低位變化時才會執行,邊沿檢測指令就是通過檢測單個地址位信號的上升或下降來決定后續指令的執行與否。緊跟在“FN”算符或“FP”算符后的邊沿存儲位用于存儲之前的邏輯運算結果,程序執行到該條指令,通過判斷邊沿存儲位和指令執行前RLO值決定指令執行后RLO的取值。SSIR將邊沿檢測指令轉換為RLO位與邊沿存儲位的比較指令和邊沿存儲位的再賦值。

例如,“FN M 0.2”被轉換為“RLO=RLO

3.4.4 主控繼電器指令

主控繼電器(Master Control Relay, MCR)指令控制著一片區域的指令是否被正常執行,自“MCR(”指令開始,以“MCR)”指令結束?!癕CR(”指令將RLO存放在一個8位深、1位寬MCR堆棧中?!?MCR”刪除MCR的棧頂項。

若進入MCR區域前,堆棧內所有RLO值為1,則MCR激活,該區中與MCR相關的指令正常執行;否則,MCR去活,賦值指令與傳送指令均向尋址位寫入“0”,復位和置位指令對尋址位不產生影響。因此,SSIR為MCR區域內指令設立MCR標識,并且在MCR區域內這4類寫操作指令執行前都要進行條件判斷。

3.4.5 嵌套指令

除主控繼電器指令以外,STL語言中允許嵌套的指令只有“A(”“AN(”“O(”“ON(”“X(”“XN(”六類位邏輯運算指令。這六類嵌套指令將RLO和OR位以及指令操作數保存在嵌套堆棧中,當遇到“)”指令時,堆棧中彈出輸入項,恢復OR位,根據指令代碼完成與RLO的運算。

SSIR為位邏輯指令和MCR指令分別設立了位堆棧和MCR堆棧,根據指令操作數來判別具體使用的堆棧類型。

4 基于SSIR的控制流圖生成算法

控制流分析分為過程內的控制流分析和過程間的控制流分析。因為組織塊相當于PLC程序的主函數,所以在中間語言生成過程中將組織塊所調用的功能塊及功能代碼內聯至組織塊程序中,針對STL程序的控制流分析便由此轉化為針對STL程序組織塊的過程內控制流分析。介紹控制流圖生成算法前,首先介紹幾個基本定義。

4.1 基本定義

定義1 基本塊?;緣K是最大化的連續指令序列,控制流只能從第一條指令進入,從最后一條指令退出,基本塊內部不存在分支。

基本塊劃分規則是:

1)第一條指令是入口語句。

2)條件跳轉或無條件跳轉的目標語句是入口語句。

3)條件跳轉或無條件跳轉指令的后一條指令是入口語句。

4)每條入口語句到下一個入后語句前的所有語句為一個基本塊。

根據基本塊的最后一條指令,可以分為四種類型:

1)單出口基本塊:末指令是無條件跳轉指令,或者該指令的下一條指令是分支轉移的目標地址。

2)雙出口基本塊:末指令是條件跳轉指令。

3)多出口基本塊:末指令是多分支跳轉指令,根據累加器的低字決定跳轉目標。

4)返回基本塊:末指令是功能、功能塊返回指令或者塊結束指令。

實際上,多分支跳轉指令很少應用于PLC程序中[11],所以在概念驗證時不考慮多分支跳轉。

定義2 控制流圖??刂屏鲌DG=(N,E)是一個以基本塊為節點的有向圖。N={B1,B2,…,Bn}是程序的基本塊集合,E?N×N表示邊的集合,如果存在(Bi,B,Bj)∈E,則從Bi到Bj存在一條有向邊,且Bi稱為Bj的前驅節點,Bj稱為Bi的后繼節點。

4.2 算法步驟

控制流圖生成算法描述如下。

輸入 SSIR指令表;

輸出 控制流圖。

//若指令表為空,返回

if (List_Instruction==null) return;

//遍歷指令表,將入口語句序號添加至入口語句序號表

for (Instruction ins: List_Instruction)

{

//程序的第一條指令為基本塊入口語句

if (ins.Id == 0)

List_Entry.add(ins.Id);

//跳轉指令的下一條指令及目標指令是入口語句

if (ins.Op == "jmp"|"cjmp")

List_Entry.add(ins.Id+1);

List_Exit.add(ins.Id);

List_Entry.add(LineOfLabel(ins.Label));

//標簽語句是入口語句

if (ins.Label != null)

List_Entry.add(ins.Id);

}

//將指令集大小加入入口語句表用于判定循環結束。

List_Entry.add(List_Instruction.size());

//遍歷入口語句序號表,構建基本塊,bc_i表示指令序號,bb_i

//表示基本塊號,n_bb表示基本塊總數

int n_bb=List_Entry.size()+1;

int[] n_pred=new int[n_bb];

ControlFlowGraph cfg=new ControlFlowGraph(n_bb);

//基本塊0和1分別為程序的入口節點和出口節點。

cfg.basic_blocks[0]=new BasicBlock(0,-1);

cfg.basic_blocks[1]=new BasicBlock(1,-1);

int bb_i=2; BasicBlock bb=null;

Iterator it=List_Entry.iterator();

for (;;)

{

int bc_i=it.next ();

if (bc_i == bc.length) break;

bb=cfg.basic_blocks[bb_i]=new BasicBlock(bb_i, bc_i);

++bb_i;

}

//為每個基本塊添加后繼節點信息

cfg.basic_blocks[0].successors=new BasicBlock[1];

cfg.basic_blocks[0].successors[0]=cfg.basic_blocks[2];

cfg.basic_blocks[1].successors=new BasicBlock[0];

Iterator it=List_Exit.iterator();

bb_i=2;

while (it.hasNext())

{

int bc_i=it.next ();

bb=cfg.basic_blocks[bb_i];

//該基本塊中沒有出口語句

while (bc_i > bb.end)

{

bb.successors=new BasicBlock[1];

bb.successors[0]=cfg.basic_blocks[bb_i+1];

BasicBlock next_bb=bb.successors[0];

bb=next_bb;

}

//出口語句為非條件跳轉指令

if(ins[bc_i].op=="jmp")

{

BasicBlock target_bb=cfg.getBasicBlockByIndex

(ins[bc_i].oprand1);

bb.successors=new BasicBlock[1];

bb.successors[0]=target_bb;

}

//出口語句為條件跳轉指令

if(ins[bc_i].op=="cjmp")

{

int bb_i=bb.id;

BasicBlock next_bb=cfg.basic_blocks[bb_i+1];

BasicBlock target_bb=cfg.getBasicBlockByIndex

(ins[bc_i].oprand2);

bb.successors=new BasicBlock[2];

bb.successors[0]=next_bb;

bb.successors[1]=target_bb;

}

}

算法中:List_Entry為入口節點表;List_Exit為出口節點表;List_Instruction為指令表;ControlFlowGraph為控制流圖類;BasicBlock為基本塊類;LogicBlock表示邏輯塊類。

4.3 實例分析

因為本文主要針對PLC程序的控制流進行分析,所以采用一個控制分支較多的實例程序進行實驗驗證。圖4所示的的STL程序包含了常用的跳轉語句及循環語句,將圖中的指令轉化為SSIR后分析其控制流,輸出的控制流圖如圖5所示。程序分為9個基本塊,其中,BB0 、BB1分別是整個控制流圖的入口塊和出口塊,二者均不含指令。

圖4 控制流分析實例代碼Fig. 4 Example code of control flow analysis

圖5 控制流圖示例Fig. 5 Example of control flow graph

圖6 控制流圖的圖形化表示Fig. 6 Graphical representation of control flow graph

將圖5中字符串形式的控制流圖轉換為圖形化表示如圖6所示。BB5是一個循環體,因此存在一條指向自身的回邊。由于BB6中最后一條指令是無條件跳轉指令,因此不存在指向BB7的邊。

5 結語

本文提出了PLC程序控制流分析方法,在對源程序進行語法分析的基礎上,利用中間表示有效解決了指令副作用的問題,生成的控制流圖為后續研究奠定了良好的基礎。未來工作主要集中于以下三方面:1)浮點數指令的中間表示轉換;2)SSIR中間表示的靜態單賦值形式轉化;3)PLC程序的數據流分析方法研究。

References)

[1] International Electrotechnical Commission. IEC 61131-3: programmable controllers — Part 3: programming languages [S]. Geneva: IEC, 2003.

[2] DARVAS D, ADIEGO B F, VINUELA E B. PLCverif: a tool to verify PLC programs based on model checking techniques [C]// Proceedings of the 15th International Conference on Accelerator and Large Experimental Physics Control Systems. Melbourne, Australia: JACoW, 2015: 911-914.

[3] ADIEGO B F, DARVAS D, VINUELA E B, et al. Applying model checking to industrial-sized PLC programs [J]. IEEE Transactions on Industrial Informatics, 2015, 11(6): 1400-1410.

[4] BIALLAS S, BRAUER J, KOWALEWSKI S. Arcade.PLC: a verification platform for programmable logic controllers [C]// Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering. New York: ACM, 2012: 338-341.

[5] STATTELMANN S, BIALLAS S, SCHLICH B, et al. Applying static code analysis on industrial controller code [C]// Proceedings of the 2014 IEEE Conference on Emerging Technology and Factory Automation.Piscataway, NJ: IEEE, 2014: 1-4.

[7] HUUCK R. Semantics and analysis of instruction list programs [J]. Electronic Notes in Theoretical Computer Science, 2005, 115: 3-18.

[8] BIHA S O. A formal semantics of PLC programs in Coq [C]// Proceedings of the 2011 IEEE 35th Computer Software and Applications Conference. Washington, DC: IEEE Computer Society, 2011: 118-127.

[9] MCLAUGHLIN S, POHLY D, MCDANIEL P, et al. A trusted safety verifier for process controller code [EB/OL]. [2017- 04- 20]. http://pdfs.semanticscholar.org/3f5e/13e951b58c1725250cb60af

c27f08d8bf02c.pdf.

[10] 西門子股份有限公司.SIMATIC S7- 300和S7- 400語句表(STL) 編程:參考手冊[M].慕尼黑:西門子公司,2002:24.(Siemens LTD. STatement List (STL) for SIMATIC S7- 300 and S7- 400 Programming, Reference Manual [M]. Munich: Siemens, 2002: 24.)

[11] 廖常初.S7- 300/400 PLC應用技術[M].北京:機械工業出版社,2005:120.(LIAO C C. Application Technology of S7- 300/400 PLC [M] Beijing: China Machine Press, 2005: 120.)

ZHANGYe, born in 1993, M. S. candidate. His research interests include information security.

LUYuliang, born in 1964, Ph. D., professor. His research interests include information security.

ControlflowanalysismethodofPLCprogram

ZHANG Ye*, LU Yuliang

(HefeiElectronicEngineeringInstitute,HefeiAnhui230037,China)

Programmable Logic Controller (PLC) is one of the most important components of industrial control system, which controls varieties of physical equipments and production processes. The faults of PLC control program caused by malicious tempering of attacker and programming errors of internal personnel will seriously threaten equipment safety and personal safety in industrial field. In order to solve this problem, a control flow analysis method of PLC program was proposed. Firstly, the lexical and syntactic structure of source code were analyzed by using flex and bison. Then, the intermediate representation without instruction side effects was generated and optimized by analyzing the Abstract Syntax Tree (AST). Finally, the basic blocks were divided on the basis of intermediate representation, and the control flow graph of the program was constructed by taking basic block as the basic unit. The experimental results show that, the proposed method can restore the control flow structure of PLC program in the form of statement table, and provide the basis for program understanding and security analysis.

Programmable Logic Controller (PLC); control flow; intermediate representation; program understanding; security

2017- 05- 09;

2017- 07- 04。

張曄(1993—),男,江西九江人,碩士研究生,主要研究方向:信息安全; 陸余良(1964—),男,江蘇宜興人,教授,博士,主要研究方向:信息安全。

1001- 9081(2017)12- 3581- 05

10.11772/j.issn.1001- 9081.2017.12.3581

(*通信作者電子郵箱zhangye_only@foxmail.com)

TP393.08;TP312

A

猜你喜歡
控制流副作用語句
徐長風:核苷酸類似物的副作用
抵御控制流分析的Python 程序混淆算法
基于返回地址簽名的控制流攻擊檢測方法
重點:語句銜接
基于控制流的盒圖動態建模與測試
基于Petri網數據流約束下的業務流程變化域分析
藥物副作用,到底怎么解?
安眠藥可以這樣吃
我喜歡
作文語句實錄
91香蕉高清国产线观看免费-97夜夜澡人人爽人人喊a-99久久久无码国产精品9-国产亚洲日韩欧美综合