常天佑，魏 強(qiáng)，耿洋洋

(1.信息工程大學(xué)，鄭州 450001； 2.數(shù)學(xué)工程與先進(jìn)計(jì)算國(guó)家重點(diǎn)實(shí)驗(yàn)室，鄭州 450001)

基于狀態(tài)轉(zhuǎn)換的PLC程序模型構(gòu)建方法

常天佑1,2*，魏 強(qiáng)1,2，耿洋洋1,2

(1.信息工程大學(xué)，鄭州 450001； 2.數(shù)學(xué)工程與先進(jìn)計(jì)算國(guó)家重點(diǎn)實(shí)驗(yàn)室，鄭州 450001)

針對(duì)可編程邏輯控制器(PLC)程序在進(jìn)行NuSMV模型檢測(cè)時(shí)需要手工對(duì)程序進(jìn)行建模，不僅浪費(fèi)人力且容易出錯(cuò)的問題，提出一種基于狀態(tài)轉(zhuǎn)移的PLC程序模型自動(dòng)化構(gòu)建方法。該方法首先分析結(jié)構(gòu)化文本(ST)語言特性并解析ST程序?yàn)槌橄笳Z法樹；其次，在抽象語法樹基礎(chǔ)上，根據(jù)不同的文法結(jié)構(gòu)進(jìn)行控制流分析生成控制流圖；然后，通過數(shù)據(jù)流分析得到程序依賴圖；最后，根據(jù)程序依賴圖生成NuSMV的輸入模型。實(shí)驗(yàn)結(jié)果表明，所提方法實(shí)現(xiàn)了ST程序到NuSMV輸入模型的自動(dòng)化構(gòu)建，并且構(gòu)建的NuSMV輸入模型既保留了ST程序的原有特性又符合NuSMV模型檢測(cè)工具輸入的規(guī)范，與傳統(tǒng)手工模型構(gòu)建方法相比，提高了模型生成的效率和準(zhǔn)確率。

工業(yè)控制系統(tǒng)安全；模型檢測(cè)；NuSMV；程序分析；模型構(gòu)建

0 引言

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

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

Szpyrka等[8]給出了Petri網(wǎng)到NuSMV輸入模型的轉(zhuǎn)化方法，Adiego等[9]雖然提出了將PLC程序的結(jié)構(gòu)化文本(Strutured Text, ST)語言構(gòu)建為NuSMV的輸入模型，但只給出相關(guān)的形式化理論模型，并沒有給出具體模型構(gòu)建的細(xì)節(jié)。文獻(xiàn)[10-12]定義了PLC程序指稱語義的格局、程序語言的語義函數(shù)及函數(shù)，為其模型檢測(cè)和定理證明提供了基礎(chǔ)，研究PLC程序的指稱語義定義，以實(shí)現(xiàn)對(duì)PLC形式化定義和檢測(cè)驗(yàn)證，但這些研究?jī)H停留在PLC程序語義的形式化定義方面，缺少PLC程序的安全檢測(cè)方法。

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

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

1 相關(guān)知識(shí)

1.1 編程語言

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

其中結(jié)構(gòu)化文本語言是用結(jié)構(gòu)化的文本來描述程序，類似pascal編程語言，是最接近于傳統(tǒng)計(jì)算機(jī)高級(jí)語言的編程語言，編程格式自由，與其他編程語言相比，ST語言語法語義較為簡(jiǎn)單易懂，可以使用循環(huán)編程結(jié)構(gòu)，適合開發(fā)復(fù)雜的程序，因此本文選取ST語言作為研究對(duì)象。

1.2 NuSMV工具

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

NuSMV模型檢測(cè)工具不能直接處理源程序，需要人工將源程序構(gòu)建為NuSMV的輸入模型。為了避免NuSMV模型檢測(cè)工具對(duì)ST程序檢測(cè)時(shí)的手工模型構(gòu)建，本文根據(jù)ST語言的語法以及NuSMV輸入模型的特征分析ST程序與NuSMV輸入模型的映射關(guān)系，提出一種PLC程序到NuSMV輸入模型的自動(dòng)化構(gòu)建方法。NuSMV輸入模型包含兩個(gè)部分：聲明部分和賦值部分。聲明部分又包括狀態(tài)和變量的聲明，賦值部分包括狀態(tài)初始化，狀態(tài)遷移以及系統(tǒng)內(nèi)變量值的變化。

2 NuSMV模型構(gòu)建方法

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

2.1 ST程序解析

Antlr4是特定編程語言的開源開發(fā)框架，能夠通過給定的語法解析某種編程語言并生成抽象語法樹。本文利用Antlr4語言開發(fā)框架解析ST程序?yàn)槌橄笳Z法樹(AST)。根據(jù)IEC61131-1標(biāo)準(zhǔn)定義的ST語言規(guī)范，給出一個(gè)簡(jiǎn)化的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]*;

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

由于本文對(duì)ST程序安全性的檢測(cè)前提是編譯無誤，所以上述算法不對(duì)ST程序的語法作嚴(yán)格的限制，只作為程序變量及語義的提取。上述語法能夠滿足部分ST編程的需要，對(duì)于更復(fù)雜的ST語言的語法可以根據(jù)實(shí)際需要在后續(xù)實(shí)踐中不斷地?cái)U(kuò)展。

2.2 控制流分析

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

tailnumHeadnumEtypeguardassignInterac-tion

其中：tailnum表示弧尾的節(jié)點(diǎn)編號(hào)；Headnum表示弧頭的節(jié)點(diǎn)編號(hào)；Etype表示弧的類型，Etype={0,1,2}，當(dāng)Etype=0時(shí)表示弧為順序弧，當(dāng)Etype=1時(shí)表示弧為分支??；guard指向?qū)?yīng)的謂詞取值表達(dá)式，當(dāng)Etype=2時(shí)表示同步關(guān)聯(lián)；assign指向?qū)?yīng)的賦值語句鏈表；Interaction表示同步，用于表示兩個(gè)有同步關(guān)聯(lián)的函數(shù)，比如通信的函數(shù)之間、調(diào)用與被調(diào)用函數(shù)之間具有同步關(guān)聯(lián)關(guān)系。

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

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

算法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語句表示跳轉(zhuǎn)語句結(jié)構(gòu)，包括調(diào)用跳轉(zhuǎn)和返回跳轉(zhuǎn)，該語句在ST程序中稱為功能塊調(diào)用或功能調(diào)用，功能塊調(diào)用屬于含參調(diào)用，功能調(diào)用屬于無參調(diào)用。對(duì)于功能塊調(diào)用，其控制流由調(diào)用功能塊轉(zhuǎn)移到被調(diào)用功能塊，當(dāng)調(diào)用功能塊執(zhí)行返回后控制流再跳轉(zhuǎn)到調(diào)用功能塊中。調(diào)用語句“F2(a:=expr1,b:=expr2)”如圖 2(b)所示，功能塊F1為調(diào)用功能塊，功能塊F2為被調(diào)用功能塊，對(duì)于功能塊F1，本文增加一個(gè)新的節(jié)點(diǎn)等待被調(diào)用功能塊F2的執(zhí)行返回，在新的節(jié)點(diǎn)前后分別增加同步關(guān)聯(lián)i及i+1，同時(shí)在被調(diào)用功能塊F2的初始和返回節(jié)點(diǎn)處增加同步關(guān)聯(lián)i及i+1。同步關(guān)聯(lián)i能夠保證被調(diào)用功能塊執(zhí)行時(shí)參數(shù)被賦值，同步關(guān)聯(lián)i+1能夠保證調(diào)用功能塊等待被調(diào)用功能塊執(zhí)行完畢并返回以及保證返回值賦值時(shí)被調(diào)用功能塊執(zhí)行完畢。對(duì)于功能塊調(diào)用，NuSMV輸入模型接近源語言的調(diào)用方式，并增加同步關(guān)聯(lián)來控制調(diào)用功能塊和被調(diào)用功能塊的調(diào)用跳轉(zhuǎn)和返回跳轉(zhuǎn)。所以對(duì)于功能塊調(diào)用的控制流圖只要在調(diào)用功能塊和被調(diào)用功能塊增加同步關(guān)聯(lián)。

在ST程序中被調(diào)用功能塊可能還會(huì)調(diào)用其他的功能或功能塊，這樣就構(gòu)成了嵌套調(diào)用。對(duì)于嵌套調(diào)用，只需在嵌套的被調(diào)用函數(shù)作同樣的處理，即對(duì)于所有的功能塊調(diào)用和功能調(diào)用均增加同步關(guān)聯(lián)，NuSMV模型檢測(cè)工具會(huì)對(duì)具有嵌套調(diào)用性質(zhì)的同步關(guān)聯(lián)進(jìn)行處理。

CALL語句對(duì)應(yīng)的控制流圖生成算法如算法2所示，Num表示節(jié)點(diǎn)編號(hào)，該算法首先在調(diào)用函數(shù)控制流圖中添加添加同步交互i和i+1，然后在被調(diào)用函數(shù)控制流圖中添加同步交互i和i+1。

算法2 Creat_CALLCFG。

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

輸出 調(diào)用與被調(diào)用功能塊的控制流圖。

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語句表示分支結(jié)構(gòu)，不管IF語句中是否包含ELSE關(guān)鍵字，都會(huì)有兩條對(duì)應(yīng)于IF條件為真或?yàn)榧俚姆种?，并且最終這兩條分支指向匯合節(jié)點(diǎn)，IF語句“IF c1>0 THEN va:=TRUE；vb:=FALSE;ELSE va:=FALSE;END_IF”的控制流圖如圖2(c)所示。

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

算法3 Creat_IFCFG。

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

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

1)

preN:=Nnum

// IF頂點(diǎn)節(jié)點(diǎn)編號(hào)

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節(jié)點(diǎn)編號(hào)

12)

Assign:=null

13)

end if

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

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

WHILE語句表示循環(huán)結(jié)構(gòu)，其控制流圖構(gòu)成了回路，在程序執(zhí)行過程中這種回路可循環(huán)多次執(zhí)行，由于NuSMV檢測(cè)工具本身會(huì)對(duì)循環(huán)結(jié)構(gòu)進(jìn)行處理，所以本文在接下來的數(shù)據(jù)流分析中只需要根據(jù)狀態(tài)轉(zhuǎn)換以接近于NuSMV輸入模型的方式表示這種循環(huán)結(jié)構(gòu)即可。

算法4 Creat_WHILECFG。

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

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

1)

preNnum:=Nnum;

//WHILE頂點(diǎn)節(jié)點(diǎn)編號(hào)

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 數(shù)據(jù)流分析

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

GuardStateNext

其中:Guard表示狀態(tài)遷移所需要滿足的條件;State表示狀態(tài)遷移的目標(biāo)狀態(tài);Next指向下一個(gè)狀態(tài)遷移。定義數(shù)據(jù)結(jié)構(gòu)variableConvert用于表示系統(tǒng)內(nèi)變量的取值變化：

StateExprNext

其中:State表示變量被賦值前的狀態(tài);Expr表示系統(tǒng)內(nèi)變量賦值語句右側(cè)的數(shù)值或表達(dá)式;Next表示該變量下一個(gè)取值變化。

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

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

圖3 程序依賴圖數(shù)據(jù)結(jié)構(gòu)Fig. 3 Data structure of program dependency graph

算法5 StateMigrate。

輸入 程序控制流圖cfg;

輸出 狀態(tài)遷移鄰接表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

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

算法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輸入模型的生成

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

算法7 CreateModule。

輸入 程序依賴圖PDG;

輸出 NuSMV輸入模型。

1)

visit(PDG){狀態(tài)集合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 實(shí)驗(yàn)結(jié)果與分析

3.1 功能測(cè)試

為了測(cè)試算法的正確性，本文對(duì)一個(gè)簡(jiǎn)單的ST程序進(jìn)行測(cè)試，自動(dòng)生成NuSMV輸入模型，并給出中間過程生成的抽象語法樹、控制流圖、程序依賴圖的相關(guān)信息。

下面是選取的一段簡(jiǎn)單的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

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

圖4 AST文本結(jié)構(gòu)Fig. 4 AST text structure

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

圖5 CFG文本結(jié)構(gòu)Fig. 5 CFG text structure

在控制流圖基礎(chǔ)上進(jìn)行數(shù)據(jù)流分析，生成程序依賴圖信息如圖6所示，程序依賴圖信息分為兩部分，一部分表示狀態(tài)遷移變化，另一部分表示系統(tǒng)內(nèi)變量賦值變化。

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

圖6 PDG文本結(jié)構(gòu)Fig. 6 PDG text structure

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

NuSMV工具對(duì)程序進(jìn)行模型檢測(cè)時(shí)還需要給出程序的安全性規(guī)約。對(duì)于工業(yè)控制系統(tǒng)，設(shè)備執(zhí)行的動(dòng)作是由PLC輸出向量決定的，為了確保工業(yè)控制系統(tǒng)控制程序的安全運(yùn)行，需要根據(jù)工業(yè)控制系統(tǒng)現(xiàn)場(chǎng)環(huán)境對(duì)PLC輸出向量進(jìn)行安全性規(guī)約描述。規(guī)約是形式化驗(yàn)證要檢測(cè)的屬性，安全需求屬性是由工業(yè)控制現(xiàn)場(chǎng)的安全要求決定，指的是為了保證工業(yè)控制系統(tǒng)的安全，對(duì)設(shè)備狀態(tài)、時(shí)序、時(shí)間、輸入輸出量等的約束。例如一個(gè)電機(jī)的額定轉(zhuǎn)速不超過2 000 rpm，交叉路口的路燈不能同時(shí)點(diǎn)亮，這就是約束狀態(tài)的安全需求。

安全規(guī)約可以用線性時(shí)態(tài)邏輯(LTL)或分支時(shí)序邏輯(CTL)來描述，下面給出測(cè)試程序的安全規(guī)約：

AG test_1.out_1 < 0sd32_15 000

(1)

AG test_1.out_1 < 0sd32_14 999

(2)

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

利用NuSMV模型檢測(cè)工具根據(jù)安全規(guī)約(1)和(2)對(duì)程序進(jìn)行模型檢測(cè)，檢測(cè)結(jié)果如圖8所示，可以看出規(guī)約(1)測(cè)試結(jié)果為真，規(guī)約(2)的測(cè)試結(jié)果為假，即測(cè)試程序滿足規(guī)約(1)的安全需求，規(guī)約(2)違反安全需求。針對(duì)違反安全需求的規(guī)約，NuMSV給出相應(yīng)的反例路徑，由于在測(cè)試中反例路徑較長(zhǎng)，包含177個(gè)狀態(tài)轉(zhuǎn)化，這里不給出相應(yīng)的結(jié)果截圖。

同時(shí)根據(jù)檢測(cè)結(jié)果還可以得輸出變量的最大值為14 999的結(jié)論。

圖8 NuSMV模型檢測(cè)結(jié)果Fig. 8 Detection results of NuSMV model

3.2 功能測(cè)試

為了測(cè)試算法的性能，對(duì)程序模型構(gòu)建過程中的抽象語法樹AST生成時(shí)間、控制流圖CFG生成時(shí)間、程序依賴圖PDG生成時(shí)間、NuSMV輸入模型生成時(shí)間以及總時(shí)間進(jìn)行測(cè)試。

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

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

4 結(jié)語

本文提出了一種基于狀態(tài)轉(zhuǎn)換的NuSMV輸入模型的自動(dòng)化構(gòu)建方法，實(shí)現(xiàn)了NuSMV工具對(duì)ST程序進(jìn)行自動(dòng)化的模型檢測(cè)。實(shí)驗(yàn)表明本文提出的方法能夠正確地將ST程序轉(zhuǎn)化為NuSMV輸入模型，同時(shí)該方法采用的模型構(gòu)建算法隨著ST程序行數(shù)的增加其時(shí)間花銷增長(zhǎng)緩慢，因此，該方法也適合于較大程序的模型構(gòu)建。在后續(xù)的工作中將進(jìn)一步完善ST語言的語法以適應(yīng)更多ST語言特性的需要，并且積極研究如何將PLC的其他語言轉(zhuǎn)化為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程序語言指稱語義及函數(shù)的形式化定義方法[J].中南大學(xué)學(xué)報(bào)(自然科學(xué)版),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。

國(guó)家重點(diǎn)研發(fā)計(jì)劃項(xiàng)目(2016YFB0800203)；上海市科研計(jì)劃項(xiàng)目(14DZ1104800)。

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

1001- 9081(2017)12- 3574- 07

10.11772/j.issn.1001- 9081.2017.12.3574

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

TP393.08；TP312

A