自“震网”病毒面世以来,人们对工业控制系统安全的认识达到了前所未有的高度。作为工业控制系统的核心组件,可编程逻辑控制器(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) 在中间表示的基础上划分基本块,构建程序控制流图用于过程内分析。
由于前两步的工作已公开发表不再赘述,本文主要介绍中间表示的生成与优化以及所面临的主要困难,并给出了程序的控制流图生成算法。
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所示。
累加器(ACCUx)是执行STL指令操作的关键部件。除位逻辑运算以外,大部分语句表操作都是在累加器中进行[10]。不同PLC型号的累加器数目不同,本文以两个累加器的为例介绍STL指令的副作用。
3.2 指令副作用STL语言的指令副作用主要源于状态字, 对状态位的隐式读写操作由PLC解释执行,其增加了程序的条件分支,但并未显式地表现在代码中。
例如图 2所示,双斜杠后的内容表示指令的隐式操作。与操作“A”将操作数的布尔值赋予状态寄存器STA,第3行根据该指令是否是逻辑串的首指令来决定后续的指令流向,这就是指令副作用产生的额外控制流。为了减少副作用引起的额外控制流,需要对部分指令进行预处理及优化,最为主要的有FC状态位和OR状态位。
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。
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所示。
prog表示构成程序的逻辑块结构,ins代表指令,包括跳转指令jmp id、条件跳转指令cjmp id, exp、功能调用指令call id、功能块调用指令call id, id、块结束指令BE、带有标签的指令label: < ins>、赋值指令 < var>:= < exp>。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 < M 0.2”和“M 0.2=RLO”两条指令。
3.4.4 主控继电器指令主控继电器(Master Control Relay, MCR)指令控制着一片区域的指令是否被正常执行,自“MCR(”指令开始,以“MCR)”指令结束。“MCR(”指令将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 基本块。基本块是最大化的连续指令序列,控制流只能从第一条指令进入,从最后一条指令退出,基本块内部不存在分支。
基本块划分规则是:
1) 第一条指令是入口语句。
2) 条件跳转或无条件跳转的目标语句是入口语句。
3) 条件跳转或无条件跳转指令的后一条指令是入口语句。
4) 每条入口语句到下一个入后语句前的所有语句为一个基本块。
根据基本块的最后一条指令,可以分为四种类型:
1) 单出口基本块:末指令是无条件跳转指令,或者该指令的下一条指令是分支转移的目标地址。
2) 双出口基本块:末指令是条件跳转指令。
3) 多出口基本块:末指令是多分支跳转指令,根据累加器的低字决定跳转目标。
4) 返回基本块:末指令是功能、功能块返回指令或者块结束指令。
实际上,多分支跳转指令很少应用于PLC程序中[11],所以在概念验证时不考虑多分支跳转。
定义2 控制流图。控制流图G=(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[1];
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分别是整个控制流图的入口块和出口块,二者均不含指令。
将图 5中字符串形式的控制流图转换为图形化表示如图 6所示。BB5是一个循环体,因此存在一条指向自身的回边。由于BB6中最后一条指令是无条件跳转指令,因此不存在指向BB7的边。
本文提出了PLC程序控制流分析方法,在对源程序进行语法分析的基础上,利用中间表示有效解决了指令副作用的问题,生成的控制流图为后续研究奠定了良好的基础。未来工作主要集中于以下三方面:1) 浮点数指令的中间表示转换;2) SSIR中间表示的静态单赋值形式转化;3) PLC程序的数据流分析方法研究。
[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. DOI:10.1109/TII.2015.2489184 |
[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. |
[6] | PRÄHOFER H, ANGERER F, RAMLER R, et al. Opportunities and challenges of static code analysis of IEC 61131-3 programs[C]//Proceedings of the 2012 IEEE 17th Conference on Emerging Technologies & Factory Automation. Piscataway, NJ:IEEE, 2012:1-8. |
[7] | HUUCK R. Semantics and analysis of instruction list programs[J]. Electronic Notes in Theoretical Computer Science, 2005, 115: 3-18. DOI:10.1016/j.entcs.2004.09.026 |
[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/13e951b58c1725250cb60afc27f08d8bf02c.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.) |