2. 数学工程与先进计算国家重点实验室, 郑州 450001
2. State Key Laboratory of Mathematical Engineering and Advanced Computing, Zhengzhou Henan 450001, China
工控安全事关经济发展、社会稳定和国家安全。近年来，随着信息化和工业化融合的不断深入，工业控制系统从单机走向互联、从封闭走向开放、从自动化走向智能化。可编程逻辑控制器作为工业控制系统的大脑，通过其上运行的代码控制整个系统的运行，同时也成为了工控攻击的重要对象。随着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 本文方法的总体技术路线 Figure 1 Overall technical route of the proposed algorithm |
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代表控制流图弧的集合。控制流图CFG可采用基于十字链表的存储方式进行存储，节点n∈N采用编号进行标识，弧e∈E表示的数据结构如下所示：
|
其中：tailnum表示弧尾的节点编号；Headnum表示弧头的节点编号；Etype表示弧的类型，Etype={0, 1, 2}，当Etype=0时表示弧为顺序弧，当Etype=1时表示弧为分支弧；guard指向对应的谓词取值表达式，当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的数据依赖分析也将会出错。
|
图 2 控制流图 Figure 2 Control flow graph |
赋值语句对应的控制流图生成算法如算法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)
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来表示控制流图的状态迁移关系：
|
其中:Guard表示状态迁移所需要满足的条件; State表示状态迁移的目标状态; Next指向下一个状态迁移。定义数据结构variableConvert用于表示系统内变量的取值变化：
|
其中:State表示变量被赋值前的状态; Expr表示系统内变量赋值语句右侧的数值或表达式; Next表示该变量下一个取值变化。
下面以图 2(c)中的IF语句控制流图为例进行数据流分析，以邻接表的方式构建程序依赖图PDG的数据结构，如图 3所示。通过对控制流图进行数据流分析分别生成状态迁移邻接表和系统内变量变化邻接表，其中状态迁移邻接表表示程序状态之间的转化关系，即哪些状态之间具有转化关系以及转化的条件，而状态代表了程序的节点，所以状态转化邻接表反映了程序的控制依赖关系，变量变化邻接表表示程序中各个变量的取值变化，邻接表中的每一项代表一个变量，每一项对应的链表表示变量在不同状态下的取值，即变量在不同状态下的定义取值，变量的定义取值可能会使用到其他的变量取值，所以变量变化邻接表反映了程序的数据依赖关系，因此本文利用状态迁移邻接表和系统内变量变化邻接表作为程序依赖图PDG的数据结构。
|
图 3 程序依赖图数据结构 Figure 3 Data structure of program dependency graph |
其中状态迁移邻接表的生成算法如算法5所示，该算法首先遍历程序控制流图cfg的每一条弧，如果状态邻接表中存在一个项的状态等于弧尾表示的状态，则把语句条件以及下一个状态添加到对应的项中，否则增加新的项。该算法需要遍历控制流图cfg中的每一条弧，并且针对每一条弧需要再遍历已创建的状态迁移邻接表State_List，所以其复杂度为O(n2)，当遍历控制流图中的所有弧后算法终止。
算法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+1500;
IF out_1>10000 THEN
out_1:=out_1/3;
out_1:=out_1+8500;
END_IF
END_IF
END_IF
END_FUNCTION_BLOCK
首先本文对上述ST程序进行解析，生成的抽象语法树AST如图 4所示，它以小括号“(”和“)”进行逐步分层，且内层的节点为外层的子节点，其中[]表示抽象语法树的根节点。
|
图 4 AST文本结构 Figure 4 AST text structure |
对控制流程序进行控制流分析，生成的控制流图信息如图 5所示，其中，最左边两列表示控制流图中弧尾节点和弧头节点，第3列表示弧的类型，第4列表示语句条件，最后一列表示赋值语句列表。
|
图 5 CFG文本结构 Figure 5 CFG text structure |
在控制流图基础上进行数据流分析，生成程序依赖图信息如图 6所示，程序依赖图信息分为两部分，一部分表示状态迁移变化，另一部分表示系统内变量赋值变化。
|
图 6 PDG文本结构 Figure 6 PDG text structure |
最后生成的NuSMV的输入模型如图 7所示，包含状态和变量的声明、状态转换及变量值的变化，其中模块Test包含8个状态之间的转化关系以及输出变量out_1在不同状态下的取值变化情况。由于PLC程序按照“扫描输入，程序执行，刷新输出”循环轮询的方式执行，PLC程序每轮执行都进行输入扫描，为了模拟所有可能的输入变量值，输入变量根据其数据类型设置相应的值，比如BOOL变量其值设置为TRUE或FALSE，整型变量其值设置为随机值。如图 7中输入变量in_1、in_2的初始值设置为TRUE或FALSE。其中0sd32_10000是根据NuSMV输入模型的规则对数字100进行了转化，表示signed word类型的数据，长度为32 bit，值的大小为10000。生成的模型既保留了ST程序的语言特性，又符合NuSMV模型的输入。
|
图 7 NuSMV输入模型 Figure 7 NuSMV input model |
NuSMV工具对程序进行模型检测时还需要给出程序的安全性规约。对于工业控制系统，设备执行的动作是由PLC输出向量决定的，为了确保工业控制系统控制程序的安全运行，需要根据工业控制系统现场环境对PLC输出向量进行安全性规约描述。规约是形式化验证要检测的属性，安全需求属性是由工业控制现场的安全要求决定，指的是为了保证工业控制系统的安全，对设备状态、时序、时间、输入输出量等的约束。例如一个电机的额定转速不超过2000 rpm，交叉路口的路灯不能同时点亮，这就是约束状态的安全需求。
安全规约可以用线性时态逻辑(LTL)或分支时序逻辑(CTL)来描述，下面给出测试程序的安全规约：
| ${\rm{AG test\_1}}{\rm{.out\_1 < 0sd32\_15000}}$ | (1) |
| ${\rm{AG test\_1}}{\rm{.out\_1 < 0sd32\_14999}}$ | (2) |
上述给出两个安全规约，其中规约(1) 表示为输出变量test_1.out_1其值小于15000，规约(2) 表示输出变量test_1.out_1小于14999。
利用NuSMV模型检测工具根据安全规约(1) 和(2) 对程序进行模型检测，检测结果如图 8所示，可以看出规约(1) 测试结果为真，规约(2) 的测试结果为假，即测试程序满足规约(1) 的安全需求，规约(2) 违反安全需求。针对违反安全需求的规约，NuMSV给出相应的反例路径，由于在测试中反例路径较长，包含177个状态转化，这里不给出相应的结果截图。
同时根据检测结果还可以得输出变量的最大值为14999的结论。
|
图 8 NuSMV模型检测结果 Figure 8 Detection results of NuSMV model |
为了测试算法的性能，对程序模型构建过程中的抽象语法树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 本文方法的性能分析 Figure 9 Performance analysis of the proposed method |
本文提出了一种基于状态转换的NuSMV输入模型的自动化构建方法，实现了NuSMV工具对ST程序进行自动化的模型检测。实验表明本文提出的方法能够正确地将ST程序转化为NuSMV输入模型，同时该方法采用的模型构建算法随着ST程序行数的增加其时间花销增长缓慢，因此，该方法也适合于较大程序的模型构建。在后续的工作中将进一步完善ST语言的语法以适应更多ST语言特性的需要，并且积极研究如何将PLC的其他语言转化为ST语言，使得该方法能够支持更多PLC的编程语言。
| [1] | MCLAUGHLIN S. On dynamic malware payloads aimed at programmable logic controllers[C]//Proceedings of the 20116th 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, BRVGGEMANN 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 20007th 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 201423th 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. |