基于狀態轉換的PLC程序模型構建方法

常天佑，魏 強，耿洋洋

(1.信息工程大學，鄭州 450001； 2.數學工程與先進計算國家重點實驗室，鄭州 450001)

基于狀態轉換的PLC程序模型構建方法

常天佑1,2*，魏 強1,2，耿洋洋1,2

(1.信息工程大學，鄭州 450001； 2.數學工程與先進計算國家重點實驗室，鄭州 450001)

針對可編程邏輯控制器(PLC)程序在進行NuSMV模型檢測時需要手工對程序進行建模，不僅浪費人力且容易出錯的問題，提出一種基于狀態轉移的PLC程序模型自動化構建方法。該方法首先分析結構化文本(ST)語言特性并解析ST程序為抽象語法樹；其次，在抽象語法樹基礎上，根據不同的文法結構進行控制流分析生成控制流圖；然后，通過數據流分析得到程序依賴圖；最后，根據程序依賴圖生成NuSMV的輸入模型。實驗結果表明，所提方法實現了ST程序到NuSMV輸入模型的自動化構建，并且構建的NuSMV輸入模型既保留了ST程序的原有特性又符合NuSMV模型檢測工具輸入的規范，與傳統手工模型構建方法相比，提高了模型生成的效率和準確率。

工業控制系統安全；模型檢測；NuSMV；程序分析；模型構建

0 引言

工控安全事關經濟發展、社會穩定和國家安全。近年來，隨著信息化和工業化融合的不斷深入，工業控制系統從單機走向互聯、從封閉走向開放、從自動化走向智能化。可編程邏輯控制器作為工業控制系統的大腦，通過其上運行的代碼控制整個系統的運行，同時也成為了工控攻擊的重要對象。隨著Struxnet攻擊的發現，研究者開始關注面向可編程邏輯控制器(Programmable Logic Controller, PLC)的惡意代碼的攻擊，比如早在2011年McLaughlin[1]給出了在PLC上惡意載荷代碼的動態生成方法；2015年在blackhat-US會議上 Klick等[2]通過修改工程代碼在s7-300中注入了一種新型的后門，實現在本地網絡進行SNMP(Simple Network Management Protocol)掃描， 并實現一個socks5代理；2016年在blackhat-Asia會議上Spenneberg等[3]在s7-1200上的工程代碼中插樁一種新型的蠕蟲，該蠕蟲能夠在PLC上進行傳播，并將自己的代碼插裝到用戶主程序中執行任意功能。這些都是利用PLC語言的缺陷實現對PLC的惡意攻擊。PLC代碼的缺陷主要表現在如空指針引用、數組下標越界、無效跳轉、無限循環、冗余代碼等代碼缺陷，以及狀態沖突、時序沖突、傳感器閾值、控制量閾值等違反安全需求的問題。

當前主要采用模型檢測的方法完成PLC代碼缺陷的發現和安全規約違反的驗證，通過設置安全鎖來檢查PLC代碼的邏輯，阻止違反安全的惡意載荷運行，試圖確保系統不會進入某些不安全的狀態，此方法已經得到學術界和工業界的認可。目前研究中主要有3種模型檢測工具：第一種是基于符號模型驗證器(Symbolic Model Verifier, SMV)的模型檢測工具，包含符號模型檢測技術和二元決策圖；第二種是基于時間自動機的模型檢測，其主要來自于UPPAAL家族[4]或Krono[5]；第三種是SPIN(Simple Promela Interpreter)[6]模型檢查器。NuSMV[7]是基于SMV的模型檢測工具，廣泛應用于可編程邏輯控制器缺陷代碼的發現，但是NuSMV不能直接對PLC源程序進行處理，只能手工將源程序翻譯為NuSMV輸入模型，然后再進行模型檢測，不僅浪費大量的人力，而且容易出錯。

Szpyrka等[8]給出了Petri網到NuSMV輸入模型的轉化方法，Adiego等[9]雖然提出了將PLC程序的結構化文本(Strutured Text, ST)語言構建為NuSMV的輸入模型，但只給出相關的形式化理論模型，并沒有給出具體模型構建的細節。文獻[10-12]定義了PLC程序指稱語義的格局、程序語言的語義函數及函數，為其模型檢測和定理證明提供了基礎，研究PLC程序的指稱語義定義，以實現對PLC形式化定義和檢測驗證，但這些研究僅停留在PLC程序語義的形式化定義方面，缺少PLC程序的安全檢測方法。

對于檢測ST程序是否存在代碼缺陷以及違反安全需求的情況，NuSMV是一種非常好的模型檢測工具，但是ST程序在進行NuSMV模型檢測時需要手工對程序進行建模，不僅浪費人力且容易出錯。為了避免NuSMV模型檢測工具對ST程序檢測時的手工模型構建，本文提出一種基于狀態轉換的ST程序模型構建方法，自動化地將ST程序轉化為NuSMV輸入模型，實現NuSMV模型檢測工具對ST程序的自動化檢測。圖1是本文方法的總體技術路線，首先對ST程序進行解析，然后進行控制流、數據流分析，最后生成NuSMV輸入模型。

圖1 本文方法的總體技術路線Fig. 1 Overall technical route of the proposed algorithm

1 相關知識

1.1 編程語言

PLC程序采用“順序掃描，不斷循環”的工作方式，其工作過程分為輸入采樣階段、執行用戶程序階段、輸出刷新階段三個階段。根據IEC61131-1標準定義，PLC編程語言主要包括如下5種，分別為梯形圖(Ladder Diagram, LD)語言、指令表(Instruction List, IL)語言、功能模塊圖(Function Block Diagram, FBD)語言、順序功能流程圖(Sequential Function Chart, SFC)語言及結構化文本(ST)語言。這五種編程器語言擁有相同的函數庫文件，因此相互之間能夠轉化。

其中結構化文本語言是用結構化的文本來描述程序，類似pascal編程語言，是最接近于傳統計算機高級語言的編程語言，編程格式自由，與其他編程語言相比，ST語言語法語義較為簡單易懂，可以使用循環編程結構，適合開發復雜的程序，因此本文選取ST語言作為研究對象。

1.2 NuSMV工具

NuSMV[7]是最流行的模型檢測工具之一，它能夠同時對線性時序邏輯(Linear Temporal Logic, LTL)和分支時序邏輯(Computation Time Logic, CTL)進行模型檢測，廣泛應用于可編程邏輯控制器缺陷代碼的發現或代碼邏輯安全性驗證。

NuSMV模型檢測工具不能直接處理源程序，需要人工將源程序構建為NuSMV的輸入模型。為了避免NuSMV模型檢測工具對ST程序檢測時的手工模型構建，本文根據ST語言的語法以及NuSMV輸入模型的特征分析ST程序與NuSMV輸入模型的映射關系，提出一種PLC程序到NuSMV輸入模型的自動化構建方法。NuSMV輸入模型包含兩個部分：聲明部分和賦值部分。聲明部分又包括狀態和變量的聲明，賦值部分包括狀態初始化，狀態遷移以及系統內變量值的變化。

2 NuSMV模型構建方法

ST語言與NuSMV的輸入模型在形式的上差異較大，ST程序很難通過一次性解析就構建為NuSMV的輸入模型，需要生成中間模型進行過渡。中間模型需要兼顧ST程序特性和NuSMV輸入模型的規范，既能保留原有程序的特性，又接近NuSMV的輸入模型。因此本文選取多個中間模型逐漸進行過渡，首先解析ST程序為抽象語法樹(Abstract Syntax Tree, AST)，然后生成控制流圖，再對控制流圖進行數據流分析生成程序依賴圖，最后構建NuSMV的輸入模型。

2.1 ST程序解析

Antlr4是特定編程語言的開源開發框架，能夠通過給定的語法解析某種編程語言并生成抽象語法樹。本文利用Antlr4語言開發框架解析ST程序為抽象語法樹(AST)。根據IEC61131-1標準定義的ST語言規范，給出一個簡化的ST語言語法，如下所示：

1)

Pro:(′FUNCTION_BLOCK′ Id St′END_FUNCTION_BLOCK′)*

(′VAR_G LOBAL′ Expr+′ END_VAR′)*

′PROGRAM main′ St ′END_PROGRAM′;

2)

ST:Stat+

3)

Stat:Id′(′ Param′)′ ′;′

4)

|′IF′ Expr ′THEN′ St (′ELSE′ St)?

5)

|′WHILE′ Expr ′DO′ St ′END_WHILE′

6)

|′VAR′ Expr+′END_VAR′

7)

|Id′:=′ Expr ′;′;

8)

Param:(Id′:=′ Expr(′,′ Id′:=′ Expr)*)？(′,′ Id ′=>′ Expr)*;

9)

Expr:Expr (′+′|′-′|′*′|′/′|′>′|′<′|′=′|′>=′|′<=′|′<>′) Expr

10)

|Expr (′AND′|′XOR′|′OR′) Expr

11)

|Id (′:′ Type (′:=′ expr )?′;′)?

12)

|Num;

13)

Type:′BOOL′|′INT′|′REAL′;

14)

Id:[a-zA-Z_]+w;

15)

Num:[0-9]+(′.′)?[0-9]*;

上述語法描述中′？′表示對象出現0次或1次，′*′表示對象出現0次或多次，′+′表示對象出現至少一次；第1)行為ST程序的入口，包括功能塊定義、全局變量聲明以及′main′程序模塊定義；第2)行中ST表示語句集合；第3)到7)行分別表示函數調用語句、IF語句、WHILE語句、變量聲明語句以及賦值語句，其中Id表示函數名，Param表示函數參數，Expr表示表達式，在第7)行中′;′表示語句結尾標志；Param在第8)行中給出了定義，′;=′代表參數輸入，′=>′代表參數輸出；Expr在第9)到13)行給出了定義，包括算術、比較、邏輯運算，變量、變量聲明和常數，其中第11)行Id表示變量，第一個括號中聲明變量的類型，內嵌的括號表示在聲明變量時的變量定義。

由于本文對ST程序安全性的檢測前提是編譯無誤，所以上述算法不對ST程序的語法作嚴格的限制，只作為程序變量及語義的提取。上述語法能夠滿足部分ST編程的需要，對于更復雜的ST語言的語法可以根據實際需要在后續實踐中不斷地擴展。

2.2 控制流分析

控制流圖常用于程序分析的中間抽象表示，反映程序的控制流關系，其結構表示直接影響數據流分析及程序模型構建的方式。程序控制流圖(Control Flow Graph, CFG)是一個有向圖，可以用二元結構CFG=(N，E)表示，其中，N代表控制流圖節點的集合，E代表控制流圖弧的集合?？刂屏鲌DCFG可采用基于十字鏈表的存儲方式進行存儲，節點n∈N采用編號進行標識，弧e∈E表示的數據結構如下所示：

tailnumHeadnumEtypeguardassignInterac-tion

其中：tailnum表示弧尾的節點編號；Headnum表示弧頭的節點編號；Etype表示弧的類型，Etype={0,1,2}，當Etype=0時表示弧為順序弧，當Etype=1時表示弧為分支?。籫uard指向對應的謂詞取值表達式，當Etype=2時表示同步關聯；assign指向對應的賦值語句鏈表；Interaction表示同步，用于表示兩個有同步關聯的函數，比如通信的函數之間、調用與被調用函數之間具有同步關聯關系。

ST語言接近于高級編程語言，適合于復雜的PLC編程邏輯，ST語言的不同文法結構具有不同的控制流結構， ST語言的文法主要包括順序語句、跳轉語句、分支語句和循環語句4種類型。本文將順序語句以賦值語句為代表進行闡述，跳轉語句以CALL語句為代表進行闡述，分支語句以IF語句為代表進行闡述，循環語句以WHILE語句為代表進行闡述。賦值語句表示順序結構，以語句“a:=a-b;b:=b=2;c:=c+1;”為代表構建其控制流圖，如圖 2(a)所示，由于賦值語句控制流單一，同時為了縮小控制流圖的狀態空間，當連續掃描到多條賦值語句時可不再增加新的狀態，如圖 2(a)中的語句“b:=b+2;”和語句“c:=c+1;”都是在狀態2下進行賦值。但是由于NuSMV工具是依賴于狀態轉換對變量的值進行跟蹤，如果兩條賦值語句之間的變量存在關聯關系，則必須在第二條語句之前增加新的狀態。例如變量b在語句“a:=a-b;”中屬于定義性出現，變量b在語句“b:=b=2;”中屬于定義性出現和使用性出現，因此這兩個語句存在關聯關系，應在語句“b:=b+2;”之前增加狀態2。如果不增加狀態2，則這兩個語句都是在狀態1下進行賦值，最后生成的NuSMV模型無法區分這兩條語句的先后順序關系，那么對變量a的數據依賴分析也將會出錯。

賦值語句對應的控制流圖生成算法如算法1所示，首先根據賦值語句抽象語法樹Assign_AST獲得賦值語句左側變量ID和賦值語句右側表達式Expr。當遇到一條賦值語句時將其臨時添加到鏈表assign中之前，檢查該賦值語句與鏈表中的賦值語句是否存在關聯關系，即檢查該賦值語句的左側變量ID是否存在鏈表assign中，或者鏈表中的是否存在某一左側變量存在于該賦值語句的右側表達式Expr中，如果存在則增加一個節點和一條邊；否則直到遇到分支或循環語句時增加一個節點和一條邊。Edge函數表示創建一條弧，Num表示控制流圖的節點編號，Edge函數的前兩個參數分別表示弧的尾節點和頭節點，assign表示賦值語句鏈表。當掃描到非賦值語句時該算法終止，由于每條賦值語句都要遍歷鏈表assign中的賦值語句，所以該算法的復雜度為O(n2)，n為ST程序中連續賦值語句的個數。

算法1 Creat_AssignCFG。

輸入 賦值語句的抽象語法樹Assign_AST；

輸出 賦值的控制流圖Assign_CFG。

1)

ID:=Assign_AST.getChild(0)

2)

Expr:=Assign_AST.getChild(2)

3)

if Id is exist in assign or Ids of assign exist in Expr then

4)

Edge(Nnum,++Nnum,0,null,assign，0)

5)

assign:=null

6)

end if

7)

assign.add(Id+":=" Expr)

圖2 控制流圖Fig. 2 Control flow graph

CALL語句表示跳轉語句結構，包括調用跳轉和返回跳轉，該語句在ST程序中稱為功能塊調用或功能調用，功能塊調用屬于含參調用，功能調用屬于無參調用。對于功能塊調用，其控制流由調用功能塊轉移到被調用功能塊，當調用功能塊執行返回后控制流再跳轉到調用功能塊中。調用語句“F2(a:=expr1,b:=expr2)”如圖 2(b)所示，功能塊F1為調用功能塊，功能塊F2為被調用功能塊，對于功能塊F1，本文增加一個新的節點等待被調用功能塊F2的執行返回，在新的節點前后分別增加同步關聯i及i+1，同時在被調用功能塊F2的初始和返回節點處增加同步關聯i及i+1。同步關聯i能夠保證被調用功能塊執行時參數被賦值，同步關聯i+1能夠保證調用功能塊等待被調用功能塊執行完畢并返回以及保證返回值賦值時被調用功能塊執行完畢。對于功能塊調用，NuSMV輸入模型接近源語言的調用方式，并增加同步關聯來控制調用功能塊和被調用功能塊的調用跳轉和返回跳轉。所以對于功能塊調用的控制流圖只要在調用功能塊和被調用功能塊增加同步關聯。

在ST程序中被調用功能塊可能還會調用其他的功能或功能塊，這樣就構成了嵌套調用。對于嵌套調用，只需在嵌套的被調用函數作同樣的處理，即對于所有的功能塊調用和功能調用均增加同步關聯，NuSMV模型檢測工具會對具有嵌套調用性質的同步關聯進行處理。

CALL語句對應的控制流圖生成算法如算法2所示，Num表示節點編號，該算法首先在調用函數控制流圖中添加添加同步交互i和i+1，然后在被調用函數控制流圖中添加同步交互i和i+1。

算法2 Creat_CALLCFG。

輸入 CALL語句的抽象語法樹CALL_AST,被調用功能塊的控制流圖called_CFG′；

輸出 調用與被調用功能塊的控制流圖。

1)

Edge(Nnum,++Nnum,2,null,null,i)

2)

Edge(Nnum,++Nnum,2,null,Null，i+1)

3)

add Edge(0,1,2,null,null,i) to called_CFG′

4)

add Edge(m-1,m,2,null,null,i+1) to called_CFG′

IF語句表示分支結構，不管IF語句中是否包含ELSE關鍵字，都會有兩條對應于IF條件為真或為假的分支，并且最終這兩條分支指向匯合節點，IF語句“IF c1>0 THEN va:=TRUE；vb:=FALSE;ELSE va:=FALSE;END_IF”的控制流圖如圖2(c)所示。

IF語句對應的控制流圖生成算法如算法3所示，該算法的第2)行獲得IF語句的條件表達式con，然后根據con在算法的第3)行創建IF條件為真的弧，與圖2(c)中弧1→2對應，IF語句中還會包含子語句，子語句可能包含賦值語句、IF語句等任意類型的語句，算法在第4)行對子語句進行處理，創建對應的控制流圖。算法第6)行根據IF語句抽象語法樹IF_AST擁有的子樹的個數判斷IF語句是否包含ELSE語句條件分支，如果IF語句不包含ELSE語句條件分支，則只需創建一條IF條件為假的弧，由于IF條件語句的兩個分支最終會指向匯合節點，所以該弧的頭節點編號不再增加，設為Nnum，弧的尾節點標號為preN，表示IF條件語句的頂點。如果IF語句不包含ELSE語句條件分支，則首先創建一條IF條件為假的弧，與圖2(c)中的1→4對應，然后根據ELSE語句分支創建對應的控制流圖。算法在第11)行對弧e的頭節點編號進行修改，使其與ELSE語句分支對應的最后一條弧的頭節點編號相等。

算法3 Creat_IFCFG。

輸入 IF語句的抽象語法樹IF_AST；

輸出 IF語句的控制流圖IF_CFG。

1)

preN:=Nnum

// IF頂點節點編號

2)

con:=IF_AST.getChild(1)

3)

e:=Edge(preN,++Nnum,1,con,null，0)

4)

Creat_CFG(IF_AST.getChild(3)) and mark the last edge as e

5)

assign:=Null

6)

if IF_AST.getChildCount()=5 then

7)

Edge(preN,Nnum,1,!con,null,0)

8)

else

//包含ELSE分支

9)

Edge(preN,++Nnum,1,!con,null,0)

10)

Creat_CFG(IF_AST.getChild(5))

// ELSE子語句

11)

e.header:=Nnum

//修改IF_END節點編號

12)

Assign:=null

13)

end if

WHILE語句表示循環結構，其循環條件可以是任意類型的布爾表達式，語句執行時首先會檢查布爾表達式，如果布爾表達式為真就執行循環體，然后檢查布爾表達式，如果仍為真則再次執行循環體，否則退出WHILE循環。WHILE語句“WHILE i<10 Do stmt；i:=i+1;END_WHILE”的控制流程圖如圖2(d)所示。

WHILE語句對應的控制流圖生成算法如算法4所示，該算法首先獲得WHILE語句的條件表達式，然后算法在3)行和第5)行根據條件表達式分別創建條件為真和條件為假的弧，算法在第4)行對WHILE語句的循環體進行處理，創建對應的控制流圖CFG。

WHILE語句表示循環結構，其控制流圖構成了回路，在程序執行過程中這種回路可循環多次執行，由于NuSMV檢測工具本身會對循環結構進行處理，所以本文在接下來的數據流分析中只需要根據狀態轉換以接近于NuSMV輸入模型的方式表示這種循環結構即可。

算法4 Creat_WHILECFG。

輸入 WHILE語句的抽象語法樹WHILE_AST；

輸出 WHILE語句的控制流圖WHILE_CFG。

1)

preNnum:=Nnum;

//WHILE頂點節點編號

2)

con:=WHILE_AST.getChild(1)

3)

Edge(preNnum,++Nnum,1,con,null,0)

4)

Creat_CFG(WHILE_AST.getChild(3))

5)

assign:=null

6)

Edge(preNnum,++Nnum,1,!con,null，0)

2.3 數據流分析

控制流圖所采用的數據結構與NuSMV輸入模型在形式上差異較大，難以直接轉換為NuSMV輸入模型，需要對控制流圖進行數據流分析生成接近于NuSMV輸入模型的程序依賴圖(Program Dependency Graph, PDG)。本文根據NuSMV輸入模型的特點，采用鄰接表的方式對程序依賴圖(PDG)進行表示，使其適用于構建NuSMV輸入模型的需要。首先，定義如下的數據結構stateConvert來表示控制流圖的狀態遷移關系：

GuardStateNext

其中:Guard表示狀態遷移所需要滿足的條件;State表示狀態遷移的目標狀態;Next指向下一個狀態遷移。定義數據結構variableConvert用于表示系統內變量的取值變化：

StateExprNext

其中:State表示變量被賦值前的狀態;Expr表示系統內變量賦值語句右側的數值或表達式;Next表示該變量下一個取值變化。

下面以圖2(c)中的IF語句控制流圖為例進行數據流分析，以鄰接表的方式構建程序依賴圖PDG的數據結構，如圖3所示。通過對控制流圖進行數據流分析分別生成狀態遷移鄰接表和系統內變量變化鄰接表，其中狀態遷移鄰接表表示程序狀態之間的轉化關系，即哪些狀態之間具有轉化關系以及轉化的條件，而狀態代表了程序的節點，所以狀態轉化鄰接表反映了程序的控制依賴關系，變量變化鄰接表表示程序中各個變量的取值變化，鄰接表中的每一項代表一個變量，每一項對應的鏈表表示變量在不同狀態下的取值，即變量在不同狀態下的定義取值，變量的定義取值可能會使用到其他的變量取值，所以變量變化鄰接表反映了程序的數據依賴關系，因此本文利用狀態遷移鄰接表和系統內變量變化鄰接表作為程序依賴圖PDG的數據結構。

其中狀態遷移鄰接表的生成算法如算法5所示，該算法首先遍歷程序控制流圖cfg的每一條弧，如果狀態鄰接表中存在一個項的狀態等于弧尾表示的狀態，則把語句條件以及下一個狀態添加到對應的項中，否則增加新的項。該算法需要遍歷控制流圖cfg中的每一條弧，并且針對每一條弧需要再遍歷已創建的狀態遷移鄰接表State_List，所以其復雜度為O(n2)，當遍歷控制流圖中的所有弧后算法終止。

圖3 程序依賴圖數據結構Fig. 3 Data structure of program dependency graph

算法5 StateMigrate。

輸入 程序控制流圖cfg;

輸出 狀態遷移鄰接表State_List。

1)

for each Edge e:cfg do

2)

stateTail:="S+e.tailnum"

3)

stateHead:="S+e.headnum"

4)

if ?i，stateTail=State_List[i].state then

5)

p:=State_ List[i].First

6)

s:=new stateConvert(e.guard,stateHead,p)

7)

State_List[i].First:=s

8)

else

9)

new stateItem(++order,stateTail,NULL);

10)

end if

11)

end for

系統內變量變化鄰接表的生成算法如算法6所示，該算法首先遍歷程序控制流圖cfg的每一條弧，如果弧中被賦值的變量在系統內變量變化鄰接表的某一項中存在，則把當前的狀態以及被賦予的值或表達式添加到對應的項中，否則增加新的項。該算法需要遍歷控制流圖cfg中的每一條弧，并且針對每一條弧需要再遍歷已創建的變量變化鄰接表Var_List，所以其復雜度為O(n2)，當遍歷控制流圖中的所有弧后算法終止。

算法6 varChange。

輸入 程序控制流圖cfg;

輸出 變量變化鄰接表Var_List。

1)

for each Edge e:cfg do

2)

stateTail:="S+e.tailnum"；

3)

var:=e.assign.split(":=")[0]

4)

Expr:=e.assign.split(":=")[1]

5)

if ?i，var=Var_List[i].var then

6)

p:=Var_List[i].First

7)

v:=new varConvert(stateTail,expr,p)

8)

Var_List[i].First:=v

9)

else

10)

new VarItem(++order,var,NULL)

11)

end if

12)

end for

2.4 NUSMV輸入模型的生成

構建生成的狀態遷移鄰接表和系統內變量變化鄰接表更接近于NuSMV輸入模型，然后通過遍歷這些鄰接表可以很容易地生成NuSMV輸入模型。NuSMV輸入模型的生成算法如算法7所示，首先通過遍歷程序依賴圖PDG獲取狀態集合S，變量集合V。對于NuSMV輸入模型狀態的聲明部分可以根據狀態集合S進行添加、變量的聲明部分可以根據變量集合V進行添加。通過遍歷鄰接表State_List獲得輸入模型的狀態遷移部分，此外此過程還需要對表示狀態之間遷移所需要滿足的條件Guard是否為NULL兩種情況分別進行處理。通過遍歷鄰接表Var_List獲得系統內各變量取值變化的信息部分，該算法的復雜度為O(n2)。

算法7 CreateModule。

輸入 程序依賴圖PDG;

輸出 NuSMV輸入模型。

1)

visit(PDG){狀態集合S,變量集合V}

2)

add Module main

//Module main

3)

add VAR

//VAR

4)

for all si ∈ S do

5)

add si to state

//S:{s0,s1,…}

6)

end for

7)

for all vi ∈V do

8)

add vi:add type of vi

//v1:boolean;

9)

end for

10)

add Assign

//Assign

11)

init state S

//init(S)=s0;

12)

add next(s):=case

//next(s):=case

13)

for all si ∈ S do

14)

P=State_List[i].First;

15)

While P do

16)

if p.Guard then

17)

add S=si & p.Guard:P.State

18)

else

19)

add S=si:p.State

20)

end if

21)

P:=P.Next

22)

end while

23)

end for

24)

add esac

//esac

25)

for all vi ∈V do

26)

add next(vi):=case

//next(vi):=case

27)

P=Var_List[i].First;

28)

While P do

29)

add S=P.State:P.Expr

//S=si:TRUE;

30)

P:=P.Next

31)

end while

32)

if vi is of Boolean type then

33)

add TRUE:{TRUR,FALSE}

34)

else

35)

add TRUE:0

//TRUE:0

36)

end if

37)

add esac;

//esac

38)

end for

3 實驗結果與分析

3.1 功能測試

為了測試算法的正確性，本文對一個簡單的ST程序進行測試，自動生成NuSMV輸入模型，并給出中間過程生成的抽象語法樹、控制流圖、程序依賴圖的相關信息。

下面是選取的一段簡單的ST程序，該ST程序包含變量聲明、賦值語句、IF語句。

FUNCTION_BLOCK Test

VAR_INPUT

in_1:BOOL;

in_2:BOOL;

END_VAR

VAR_OUTPUT

out_1:REAL;

END_VAR

IF in_1 THEN

IF in_2 THEN

out_1:=out_1+1 500;

IF out_1>10 000 THEN

out_1:=out_1/3;

out_1:=out_1+8 500;

END_IF

END_IF

END_IF

END_FUNCTION_BLOCK

首先本文對上述ST程序進行解析，生成的抽象語法樹AST如圖4所示，它以小括號“(”和“)”進行逐步分層，且內層的節點為外層的子節點，其中[]表示抽象語法樹的根節點。

圖4 AST文本結構Fig. 4 AST text structure

對控制流程序進行控制流分析，生成的控制流圖信息如圖5所示，其中，最左邊兩列表示控制流圖中弧尾節點和弧頭節點，第3列表示弧的類型，第4列表示語句條件，最后一列表示賦值語句列表。

圖5 CFG文本結構Fig. 5 CFG text structure

在控制流圖基礎上進行數據流分析，生成程序依賴圖信息如圖6所示，程序依賴圖信息分為兩部分，一部分表示狀態遷移變化，另一部分表示系統內變量賦值變化。

最后生成的NuSMV的輸入模型如圖7所示，包含狀態和變量的聲明、狀態轉換及變量值的變化，其中模塊Test包含8個狀態之間的轉化關系以及輸出變量out_1在不同狀態下的取值變化情況。由于PLC程序按照“掃描輸入，程序執行，刷新輸出”循環輪詢的方式執行，PLC程序每輪執行都進行輸入掃描，為了模擬所有可能的輸入變量值，輸入變量根據其數據類型設置相應的值，比如BOOL變量其值設置為TRUE或FALSE，整型變量其值設置為隨機值。如圖7中輸入變量in_1、in_2的初始值設置為TRUE或FALSE。其中0sd32_10 000是根據NuSMV輸入模型的規則對數字100進行了轉化，表示signed word類型的數據，長度為32 bit，值的大小為10 000。生成的模型既保留了ST程序的語言特性，又符合NuSMV模型的輸入。

圖6 PDG文本結構Fig. 6 PDG text structure

圖7 NuSMV輸入模型Fig. 7 NuSMV input model

NuSMV工具對程序進行模型檢測時還需要給出程序的安全性規約。對于工業控制系統，設備執行的動作是由PLC輸出向量決定的，為了確保工業控制系統控制程序的安全運行，需要根據工業控制系統現場環境對PLC輸出向量進行安全性規約描述。規約是形式化驗證要檢測的屬性，安全需求屬性是由工業控制現場的安全要求決定，指的是為了保證工業控制系統的安全，對設備狀態、時序、時間、輸入輸出量等的約束。例如一個電機的額定轉速不超過2 000 rpm，交叉路口的路燈不能同時點亮，這就是約束狀態的安全需求。

安全規約可以用線性時態邏輯(LTL)或分支時序邏輯(CTL)來描述，下面給出測試程序的安全規約：

AG test_1.out_1 < 0sd32_15 000

(1)

AG test_1.out_1 < 0sd32_14 999

(2)

上述給出兩個安全規約，其中規約(1)表示為輸出變量test_1.out_1其值小于15 000，規約(2)表示輸出變量test_1.out_1小于14 999。

利用NuSMV模型檢測工具根據安全規約(1)和(2)對程序進行模型檢測，檢測結果如圖8所示，可以看出規約(1)測試結果為真，規約(2)的測試結果為假，即測試程序滿足規約(1)的安全需求，規約(2)違反安全需求。針對違反安全需求的規約，NuMSV給出相應的反例路徑，由于在測試中反例路徑較長，包含177個狀態轉化，這里不給出相應的結果截圖。

同時根據檢測結果還可以得輸出變量的最大值為14 999的結論。

圖8 NuSMV模型檢測結果Fig. 8 Detection results of NuSMV model

3.2 功能測試

為了測試算法的性能，對程序模型構建過程中的抽象語法樹AST生成時間、控制流圖CFG生成時間、程序依賴圖PDG生成時間、NuSMV輸入模型生成時間以及總時間進行測試。

本文分別對程序行數為21、52、77、148、210的ST程序進行測試，每種程序測試3次，然后求其平均值，測試結果如圖9所示，這5條折線分別表示程序模型構建過程中的抽象語法樹AST生成時間(AST時間)、控制流圖CFG生成時間(CFG時間)、程序依賴圖PDG生成時間(PDG時間)、NuSMV輸入模型生成時間(NuSMV時間)以及總時間。 其中，AST生成算法占據模型構建過程中的大部分時間，CFG生成、PDG生成、NuSMV模型生成花費的時間較少，并且隨著ST程序行數的增加，AST生成花費的時間增長較為緩慢，且總時間增長也較為緩慢，可見本文采用的方法能夠滿足較大程序的模型構建。

圖9 本文方法的性能分析Fig. 9 Performance analysis of the proposed method

4 結語

本文提出了一種基于狀態轉換的NuSMV輸入模型的自動化構建方法，實現了NuSMV工具對ST程序進行自動化的模型檢測。實驗表明本文提出的方法能夠正確地將ST程序轉化為NuSMV輸入模型，同時該方法采用的模型構建算法隨著ST程序行數的增加其時間花銷增長緩慢，因此，該方法也適合于較大程序的模型構建。在后續的工作中將進一步完善ST語言的語法以適應更多ST語言特性的需要，并且積極研究如何將PLC的其他語言轉化為ST語言，使得該方法能夠支持更多PLC的編程語言。

References)

[1] MCLAUGHLIN S . On dynamic malware payloads aimed at programmable logic controllers [C]// Proceedings of the 2011 6th USENIX Conference on Hot Topics in Security. Berkeley, CA: USENIX Association, 2011: 1-6.

[2] KLICK J, LAU S, MARZIN D, et al. Internet-facing PLCs — a new back orifice [EB/OL]. [2017- 04- 16]. http://www.inf.fu-berlin.de/inst/ag-si/pub/us-15-Klick-Internet-Facing-PLCs-A-New-Back-Orifice-paper.pdf.

[3] SPENNEBERG R, BRüGGEMANN M, SCHWARTKE H. PLC-blaster: a worm living solely in the PLC [EB/OL]. [2017- 04- 16]. http://regmedia.co.uk/2016/04/29/plc_87458745.pdf.

[4] LARSEN K G, PETTERSSON P, WANG Y, et al. UPPAAL in a nutshell[J]. International Journal on Software Tools for Technology Transfer, 1997, 1(1/2): 134-152.

[5] YOVINE S. KRONOS: a verification tool for real-time systems [J]. International Journal on Software Tools for Technology Transfer, 1997, 1(1/2): 123-133.

[6] HAVELUND K, PENIX J, VISSER W. SPIN model checking and software verification [C]// Proceedings of the 2000 7th International SPIN Workshop on Model Checking of Software, LNCS 1885. Berlin: Springer, 2000: 655-659.

[7] CIMATTI A, CLARKE E, GIUNCHIGLIA F, et al. NuSMV: a new symbolic model verifier [C]// Proceedings of the 1999 International Conference on Computer Aided Verification, LNCS 1633. Berlin: Springer, 1999: 495-499.

[8] SZPYRKA M, A BIERNACKA, BIERNACKI J. Methods of translation of Petri nets to NuSMV language [C/OL]// Proceedings of the 2014 23th International Workshop on Concurrency, Specification and Programming, [2017- 04- 16]. http://www.ceur-ws.org/Vol- 1269/paper245.pdf.

[9] ADIEGO B F, DARVAS D, TOURNIER J C, et al. Automated Generation of Formal Models from ST Control Programs for Verification Purposes, CERN-ACC-NOTE- 2014- 0037 [R]. Geneva, Switzerland: CERN, 2014.

[10] 肖力田,顧明,孫家廣.一種PLC程序語言指稱語義及函數的形式化定義方法[J].中南大學學報(自然科學版),2011,42(增刊1):1107-1113. (XIAO L T, GU M , SUN J G. Formal definition method of denotational semantics and functions for PLC program language [J]. Journal of Central South University (Science and Technology), 2011, 42(Suppl. 1): 1107-1113.)

[11] MCLAUGHLIN S, ZONOUZ S, POHLY D, et al. A trusted safety verifier for process controller code [EB/OL]. [2017- 04- 16]. http://adambates.org/courses/cs598-fa16/slides/cs598- 17-slides-trusted-safety-verifier.pdf.

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

This work is partially supported by the National Key Research and Development Program of China (2016YFB0800203), the Scientific Research Plan Program of Shanghai (14DZ1104800).

CHANGTianyou, born in 1992, M. S. candidate. His research interests include industrial control system security.

WEIQiang, born in 1979, Ph. D., professor. His research interests include software vulnerability analysis, industrial control system security.

GENGYangyang, born in 1994, M. S. candidate. His research interests include industrial control system security.

ConstructingmethodofPLCprogrammodelbasedonstatetransition

CHANG Tianyou1,2*, WEI Qiang1,2, GENG Yangyang1,2

(1.InformationEngineeringUniversity,ZhengzhouHenan450001,China;2.StateKeyLaboratoryofMathematicalEngineeringandAdvancedComputing,ZhengzhouHenan450001,China)

The Programmable Logic Controller (PLC) program needs modeling the program manually in the NuSMV model testing, which is not only a waste of manpower but also an error-prone procedure. In order to solve the problems, an automatic construction method of PLC program model based on state transition was proposed. Firstly, the Structured Text (ST) language features were analyzed and the ST program was parsed as an abstract grammar tree. Secondly, according to the abstract grammar tree, the control flow graph was generated based on different grammatical structure by control flow analysis. And then the program dependency graph was obtained by data flow analysis. Finally, the NuSMV input model was generated according to the program dependency graph. The experimental results shows that, the proposed method achieves the automatic construction from ST program to NuSMV input model, and the constructed NuSMV input model not only retains the original characteristics of ST program but also conforms to the input standard of NuSMV model detection tool. Compared with the traditional manual model construction method, the proposed method improves the efficiency and accuracy of model generation.

industrial control system security; model detection; NuSMV; program analysis; model constructing

2017- 06- 13;

2017- 09- 07。

國家重點研發計劃項目(2016YFB0800203)；上海市科研計劃項目(14DZ1104800)。

常天佑(1992—)，男，河南駐馬店人，碩士研究生，主要研究方向：工控安全； 魏強(1979—)，男，江西南昌人，教授，博士，主要研究方向：軟件脆弱性分析、工控安全； 耿洋洋(1994—)，男，河南周口人，碩士研究生，主要研究方向：工控安全。

1001- 9081(2017)12- 3574- 07

10.11772/j.issn.1001- 9081.2017.12.3574

(*通信作者電子郵箱641644683@qq.com)

TP393.08；TP312

A