一种安全关键软件系统符号执行优化方法

戴延军，吴志强，刘 杰，刘朝晖，陈 智，肖安红

(1.南华大学计算机科学与技术学院，湖南 衡阳 421000;2.中国核动力研究设计院核反应堆系统设计技术国家级重点实验室，四川 成都 610000)

0 引 言

安全关键系统(Safety-Critical Systems, SCS)是指系统功能一旦失效将引起生命、财产的重大损失以及环境可能遭到严重破坏的系统[1]。此类系统广泛存在于航空航天、核电及国防军工等诸多安全关键领域。控制软件是安全关键系统的重要组成部分[2]，高效的测试方法的研究是提高安全关键系统可靠性的重要途径[3]。

符号执行技术是一种重要的程序分析技术,由King等[4]于1976年提出，其优势是能以较少的测试用例集获得较高覆盖率，从而探测软件深层错误。符号执行将实际输入用符号代替,程序的操作转换为符号表达式操作，程序的执行随着遇到分支指令进行分叉,以探索各分支,同时将分支条件加入到当前路径条件，通过约束求解判定路径是否可行，若路径条件有解,则表明路径可行;反之,则终止该路径分析。符号执行的研究主要经历传统符号执行[4]→动态符号执行[5]→选择符号执行[6]的发展过程。

符号执行生成测试用例优势明显，但符号执行工业应用面临着2个方面的困难和挑战:1)路径爆炸问题[7]，针对该问题的相关研究较多，例如基于懒符号执行的路径求解算法[8]、控制流污点信息导向的符号执行技术[9]、符号摘要方法[10]；2)约束求解困难[11]，这是符号执行过程中最为耗时的部分,有研究表明其约占到执行时间的40%～90%[12]。文献[13]将多次约束求解合并成一次求解,从而减少约束求解消耗的时间,并使用蚁群算法提高路径成功猜测率。文献[14]使用机器学习的方法来简化复杂约束。文献[15]使用扩展的并行KLEE[16]约束求解器来缩短约束求解的时间。

安全关键软件系统的模块之间存在耦合性，这类系统直接使用符号执行生成测试用例会遇到符号执行技术工业应用中的约束求解困难，这直接决定了符号执行对这类系统生成测试用例的可能性。

约束求解困难是阻碍符号执行工业应用的重要因素，同时这类问题是一个NP完全问题，相关研究在解决这类通用问题的基本思路是大约束化为小约束求解，其中较为突出的是约束独立求解的思想[20]，即如果2个约束相互独立，单独求解即可。然而，安全关键系统的软件耦合使得约束独立优化方法不能直接使用，局部解可能造成全局约束的不可解。为了在分割约束的过程中，各约束子集之间的依赖最小，以使分割后约束的可解性更高，本文提出一种带权最小割集的分割方法对大约束进行分割，这种带权最小割集的优化方法将软件系统的各模块解耦，降低约束求解的难度，使符号执行能用到安全关键软件耦合系统的测试用例生成。

1 安全关键软件系统的耦合性

控制软件是安全关键软件系统的重要组成部分，在工业领域，常使用算法组态来建立控制算法模型。许多现代控制理论算法都是基于状态空间描述或传递函数矩阵[17]，这种集中描述方式难用于实际的分布式工业过程。组态控制[18]的思路则不同，其通过简单的标准结构单元(如积分器、基本PIO等)的任意连接组成复杂的控制算法，如前馈、串级和微分导前等。如图1所示的图形就是一个counter图形组态，实现按周期加1的功能。安全关键控制系统由基本的组态搭建而成，组态之间共同变量的存在使得软件存在耦合性。图2所示为一个控制算法功能模块的组态组合模型。耦合性是程序模块之间关联性的度量，它取决于各模块间接口复杂程度、模块调用方式和接口传递的信息。在安全关键系统中，存在4种耦合方式。

1)非直接耦合。

2个控制算法组态之间无直接关系，双方的联系通过主控模块的控制和调节实现，此类耦合称为非直接耦合。

图1 counter图形组态

图2 控制算法组态模型

2)数据变量耦合。

当2个组态之间通过数据变量传递信息时，则称2个组态之间存在数据变量耦合。

3)控制参数耦合。

如果一个组态通过传递开关、标示或其他枚举值等控制信息，对另一组态的功能产生了影响，则这2个组态称为控制参数耦合。

4)混合型耦合。

如果2个模块之间既存在数据变量耦合，也存在混合型耦合，则称这种耦合为混合型耦合。

安全关键系统的耦合性相当复杂，但在使用组态的方式进行建模的过程中，可以将复杂的耦合性概括为以上4种情况。实际生产中，大型系统通常会包含以上4种情况。

2 安全关键系统的符号执行

组态开发方式也是基于模型开发思想的。通常这类系统不会手工编写代码，而是使用经过相关认证工具设计控制算法模型，然后生成通用高级语言[19](如C和Ada)。图2所示的模型通常会转换为一个通用高级语言的函数，每个单独的算法块也会转换成等价的高级语言的函数，连线表示共同变量传递，即，设模型生成的函数OP(Pn)，其中，n为共同变量的个数，Pn={p1,p2，…，pn}为变量。设Fs(Qm)为基本算法块生成的函数，其中，s为函数的个数，m为每个Fs包含的变量个数，Fs={f1,f2，…，fs}，Qm={q1,q2，…，qm}，Q⊆P。对于2个函数F1和F2，如果Q1∩Q2=K≠Ø，则函数F1和F2存在依赖，且K为Q1和Q2的共同变量集。设符号执行将OP(Pn)生成路径约束公式C，每个单独的函数fi生成路径约束公式Ci，则对于安全关键系统符号执行生成的路径约束可表述如公式(1)所示：

(1)

定义1约束独立。如果Ci和Cj不含共同变量，则约束Ci和Cj相互独立，如x+y<3∧z>5。

定义2约束耦合。如果Ci和Cj包含共同变量，则约束Ci和Cj存在耦合，如x+y<3∧y>4。

安全关键软件使用符号执行生成路径约束会包含定义1和定义2所示的2种情况。2个路径约束公式要么相互独立，要么包含共同变量出现约束耦合现象。组态所体现的4种耦合性最终会表现为约束耦合。

约束求解是一个NP完全问题，引言部分已介绍通用的处理方法，其中，约束独立求解的思想较为通用。然而，约束耦合使得约束独立优化无法直接使用。局部解可能造成全局约束的不可解，如x+y<3∧y>4∧y+z<3∧z>1，将y用5替换使得子公式x+y<3∧y>4可解，但对于y+z<3∧z>1不可解。如果不可解，则不进行分割求解。为了在分割约束的过程中，各约束子集之间的依赖最小，以使分割后约束的可解性更高，本文提出一种带权最小割集的分割方法对大约束进行分割。

3 解约束耦合的优化方法

图3 约束的图模型

算法1带权最小割集Min_Weight_Constraint_Cut

输入:约束集C

输出:分割出的约束子集PC1和PC2

1. Min_Weight_Constraint_Cut(C)

2.For i←1 to |C|

3.图G push Ci

4.For j←1 to |组合(|C|,2)|

5.s,t←组合序列(|C|,2)

6.If Vst=Cs∩Ct≠Ø Then

8.图G push Eij

9.End If

10.End For

11.End For

12.Return PC1,PC2=MinimunCut(图G)

算法重点处理约束的公共变量提取以及权值的计算，最小割集算法MinimunCut较为通用。由于变量在约束中出现的频率会对约束的依赖产生影响，因此在求解最小依赖时需要考虑。

4 实 验

安全关键软件耦合现象广泛存在于此领域的各种软件系统中。实验选取较为典型的核安全级仪控系统控制算法的功能模块，从每个模块中选取和其他模块存在耦合性的路径约束，算法块和耦合约束图模型统计信息如表1所示。实验工具为KLEE、CVC4和Z3[23]约束求解器，其中，KLEE是学术界和工业界较为成熟的符号执行工具，CVC4[24]和Z3是学术界和工业界表现较好的约束求解器。实验对比了使用传统的符号执行工具KLEE+CVC4、KLEE+Z3求解器和使用KLEE+优化算法+CVC4、KLEE+优化算法+Z3所体现的求解时间上的优势。对比实验结果如表2所示，时间对比如图4所示，分割后约束可满足性如表3所示。从图4可以看出，M1在不进行符号约束优化的情况下，CVC4所消耗的时间为53 ms，Z3所消耗的时间为34 ms。M4在不进行符号约束优化的情况下，CVC4所消耗的时间为113 ms，Z3所消耗的时间为86 ms。M1使用优化算法后，CVC4求解的时间为35 ms，Z3求解时间为28 ms，求解的时间平均减少了25.80%。对于长约束M4，CVC4和Z3所用时间分别为113 ms和86 ms，优化后所用时间分别为101 ms和74 ms，求解时间平均减少了12.28%。M1～M4的平均求解时间减少了19.18%。大型系统通常会存在大量的这类约束耦合公式，处理多条路径约束时间上会显著减少。从表3可满足性数据看出，由于考虑了变量在子公式出现的频率，常量替换后的约束公式可满足性比较接近直接求解。通过实验对比可以看到，带权最小割集优化分割一方面提高了约束求解的速度，另一方面也提高了约束分割后的可解性。

表1 核安全级仪控系统控制算法

控制算法算法块数耦合约束图模型M14M28M310M416

表2 时间对比结果 单位：ms

控制算法CVC4Z3优化+CVC4优化+Z3M153343528M271486140M374646244M41138610174

表3 带权最小割集可满足性

控制算法CVC4Z3优化+CVC4优化+Z3M1satsatsatsatM2satsatsatsatM3satsatsatsatM4satsatunsatsat

图4 求解时间对比图

5 结束语

对于安全关键系统而言，其可靠性需要通过大量的测试来进行。符号执行作为一种优势明显的测试用例生成方式被用在自动化测试方面。本文针对安全关键软件系统的耦合性提出了一种基于最小割集的带权约束分解方法。通过实验表明，优化方法不仅提升了约束求解的速度，也提高了约束分割后的可解性。在以后的研究中，将对2个方面进行改进，一是对约束的分割方法进行改进，二是深度挖掘约束的变量之间的关系，使得分割后约束的可解性进一步提高。