基于KLEE的复杂路径中内存泄露检测研究

黄 琦,彭 武，蔡爱华，王冬海

(1.中国电子科学研究院，北京 100041;2.北京联海信息系统有限公司，北京 100041)

0 引 言

在软件安全问题中，内存泄漏[1]指由于疏忽或错误造成程序未能释放已经不再使用的内存的情况。内存泄漏并非指内存在物理上的消失，而是应用程序分配某段内存后，由于设计错误，失去了对该段内存的控制，因而造成了内存的浪费。为了解决这一问题，科研工作者开发了非常多的检测工具例如：ccmalloc[2]，Leaky[3]，LeakTracer[4]，MEMWATCH[5]，Valgrind[6]。这些检测工具虽然检测范围广泛，能够处理很多的内存泄露问题，但是运行花费较大，并且由于如今程序路径的复杂程度越来越高，检测工具对于代码覆盖率不高，因而许多复杂路径中的内存泄露问题无法得到解决。

本文利用符号执行工具KLEE[7]，通过实现Z3[8]求解器在KLEE中的并行实现，生成能够覆盖复杂路径的测试用例，最终利用生成的测试用例检测出复杂路径中的内存泄露。

1 KLEE约束求解并行优化设计

KLEE是一个运行在Linux操作系统上的开源动态符号执行[9]工具，其具有自动化生成测试用例的特点，并且其生成的测试用例达到很高的代码覆盖率。KLEE中的求解模块是由STP[10]求解器构成，由于原STP求解器支持的求解理论不足，我们将支持各种复杂求解理论的Z3求解器与STP求解器并行，共同实现KLEE的约束求解模块，从而实现复杂路径的覆盖。

1.1 KLEE并行约束求解模块

KLEE中使用符号执行时，将收集程序路径中的约束条件。对这些路径约束条 件进行约束求解的主要作用有两点，一是在程序中分支语句处的条件表达式中利用对变量值满足条件与否来选择程序执行路径，起到路径预判的作用，二是在路径选择时，求解出满足路径约束条件的变量值分布。KLEE并行约束求解模块如图1所示。

图1 KLEE并行约束求解模块

KLEE并行约束求解模块的实现将收集到的约束条件集经过KLEE优化模块后，将Z3求解器和STP求解器并行求解，从而解决复杂路径中生成的约束条件求解问题。

1.2 约束条件语法解析模块

KLEE的约束求解模块主要完成的功能是求解符号执行过程中收集而来的约束条件集合来进行路径选择和变量求解。这项功能需要经过如下三个步骤：首先，约束求解模块应用优化算法对约束集合进行化简优化；其次，因为在符号执行中KLEE将约束条件描述成KQuery语法格式，因此约束集全发送到约束求解模块后，还需要对该语法格式的约束条件调用求解器的函数接口进行解析，转换成求解器的语法描述，才能进行求解。最后，求解器接受求解调度控制决定对化简、转换后的约束集合表达式进行求解。

KQuery语言是KLEE中约束表达式的文本表示语言，其语法描述使用扩展巴科斯范式(Extended Backus-Naur Form)表示[11]。KQuery定义了描述约束条件表达式的语法，在求解器和KQuery语言之间提供了一个抽象解析层，降低了具体的求解器代码与KQuery的耦合度，可以增加KLEE中求解器的灵活性，如图2所示。

图2 约束条件解析层次图

解析层定义为一个抽象类型，声明了对于解析KQuery语法的操作函数，而具体的解析动作放在继承类中实现，创建抽象类SolverBuilder用于定义解析KQuery语法的变量、数组以及表达式操作。如：位操作、算术操作、逻辑操作等。STP求解器和Z3求解器分别按照各自的实现方法实现这些操作。

1.3 约束求解调度设计

调用约束求解器的操作，都是在SolverImpl的子类STPSolverImpl中以直接调用STP的求解函数的形式实现，而对SolverImpl的操作又是放在Solver类对象中进行的。因此，可以在Solver的操作函数中，增加一个调度接口。同时在Solver类对象中增加一个SolverImpl实例。让Solver对象需要调用求解器时，都经过调度函数选择两个SolverImpl类型的派生对象来同时求解。如图3所示。

图3 求解调度层次图

利用这种方法对于原有的代码不需要进行修改，只要新增Solver的继承类对象，在其中增加对SolverImpl对象的调度操作，从而实现了STP求解器和Z3求解器的并行设计。

2 KLEE约束求解器并行化的实现

从符号执行过程中得到的约束条件集采用 KQuery语法描述，求解器无法直接求解这种格式的约束条件。STP求解器和Z3求解器都需要将约束条件转换为自身的语法形式，才能完成求解。因此，上图中约束解析层起到解析KQuery语句，将约束条件转换为各个求解器自己设计的语法形式。使用抽象的约束解析层，对外隐藏了各个求解器具体的解析过程，使得解析操作具有一个统一的对外调用形式。

2.1 KQuery抽象解析层

KLEE中原有求解模块改进为并行求解模块后的求解流程。从符号执行过程中得到的约束条件集采用KQuery语法描述，求解器无法直接求解这种格式的约束条件。如图4所示。

图4 抽象解析层实现

KQuery抽象解析层设计的主要目的是为解析KQuery表示的约束条件提供统一的对外调用接口，同时对声明了基本的解析函数名。在设计中，考虑到可扩展性和规范性，没有沿用KLEE源代码中STP的解析设计，而是重新设计了该抽象解析类的操作函数。

如上面所示代码是KQuery的抽象解析的主体部分，定义了与各个KQuery语句对应的虚函数，具体的实现有赖于具体求解器的不同代码。最后一个Analysis方法应用上面的函数，对约束条件进行解析。其伪代码形式如图5所示。

图5 Analysis伪代码

符号执行过程收集起来的约束条件以Expr结构的形式传递给解析过程，通过 读取该结构中的内容，通过类似Switch的分支选择，可以分析出这段字符串中含 有哪些约束条件，通过解析后将这些约束条件转换为求解器相关的语法形式，存入求解器的存储空间也就是*Constraints 指示的空间中。在约束条件解析完成后将该地址返回。

2.2 Z3约束求解器实现

KLEE源代码中有关于STP求解器模块，是KLEE在进行约束求解过程中调用了STP求解器模块进行求解，但是与此同时STP求解器在于非线性问题上的欠缺和理论上的不足，导致对于复杂路径的约束条件无法求解，于是这里我们将Z3求解器并行加入，与STP求解器共同对KLEE中经过符号执行过后收集的约束条件进行求解。当一个子进程结束后，主进程中止运行中的求解，将会得到两者共享的区域中得到结果。

图6 Z3SolverImpl类主要成员及操作

Z3求解器类继承自SolverImpl基类。在图6中给出的Z3SolverImpl类中包含了解析类对象SolverBuilder的指针，以及一个Solver类对象指针。在Z3SolverImpl类对象构造的时候，给这两个指针赋以对应的对象地址。SolverBuilder类型指针用来使用前面构造完成的Z3解析类对象。而Solver类型的指针的作用是在Z3约束求解类对象中加入对约束条件集的优化操作。

KLEE中本来的Solver基类的接口函数与我们设计的ConcurrentSolver类型设计相符合，在使用的时候可以像源代码中使用STPSolver类一样的使用，由于我们设计的接口保持了与原来KLEE原约束求解模块的接口保持了一致，在实验中可以通过直接KLEE的运行参数来调用这两个求解器进行测试用例的生成。求解模块如图7所示。

图7 Z3和STP求解模块调度实现

通过上述对Z3求解器调度的实现，将两个求解器并行加入到KLEE中去，在原有的KLEE基础上，实现了在KLEE中利用多进程使用Z3和STP求解器对约束条件集合同时进行求解的代码实现。从而实现对复杂路径进行约束求解，生成覆盖复杂路径的测试用例。

3 复杂路径中内存泄露检测方法

对于C和C++这种没有Garbage Collection 的语言来讲，我们主要关注两种类型的内存泄漏：堆内存泄漏[12](Heap leak)。对内存指的是程序运行中根据需要分配通过malloc,realloc new等从堆中分配的一块内存，再是完成后必须通过调用对应的 free或者delete 删掉。如果程序的设计的错误导致这部分内存没有被释放，那么此后这块内存将不会被使用，就会产生Heap Leak；系统资源泄露(Resource Leak)[13]主要指程序使用系统分配的资源比如 Bitmap,handle ,SOCKET等没有使用相应的函数释放掉，导致系统资源的浪费，严重可导致系统效能降低，系统运行不稳定。

由于之前利用并行了Z3求解器的KLEE能够生成覆盖复杂路径各个分支的测试数据、路径条数、结点位置。本文利用output窗口定位检测引发内存泄露的代码。

首先将检测程序调成debug模式，然后在需要检测的内存泄露程序cpp头上加上以下代码如图8。

图8 内存泄露检测

最后在由并行了Z3求解器的KLEE测试出来的每条路径上分别加入图9中的检测代码：

图9 内存泄露检测代码

通过上述的操作之后，能够在输出中看到检测程序的内存泄露情况，上述原理是将MFC中的内存泄露检测方法推广到一般的内存泄露检测问题中，从而生成内存泄露问题的检测报告。报告中不仅能检测出内存泄露问题，还能定位内存泄露的位置和个数，达到内存泄露检测的目的。

4 实 验

为了验证本文方法的正确性和有效性，我们在linux系统下进行KLEE的测试，最终的内存泄露检测在windows系统下进行，在编写的10条复杂路径中的每段分支都加入内存泄露代码，通过上述方法进行内存泄露的检测，生成内存泄露报告。

进行测试的部分源代码如图10所示。

图10 部分内存泄露代码

下面给出KLEE及Z3求解器并行之后的KLEE测试结果：

KLEE测试的结果如图11所示。

图11 KLEE测试结果

改进后KLEE测试的结果如图12所示。

图12 Z3求解器并行的KLEE测试结果

通过上述求解的结果的对比，并行Z3求解器后的KLEE测试出10条路径中的8条，并且对每条路径都生成了能够覆盖的测试数据，而原KLEE求解器只覆盖了其中5条路径。充分说明了Z3求解器并行实现的KLEE具有更强的求解复杂路径的能力，该方法具有正确性和可行性。

下面利用上面的测试的数据，按照本文中采用的内存泄露检测方法，进行漏洞泄露检测，实验结果如图13所示。

图13 内存泄露检测结果

通过上述的内存泄露检测结果我们可以看出，利用Z3求解器并行后的KLEE找到了复杂路径的各条路径之后，对每条路径进行内存泄露检测，最终得到了内存泄露的位置、个数，证明了本文方法的正确性和可行性。

5 结 语

本文在原有的符号执行工具KLEE的基础上，改进了原有KLEE中STP求解器支持理论不足的问题，加入Z3求解器与STP求解器并行来求解复杂路径问题，继而利用测试数据对每条路径分别进行内存泄露的检测，最终实现了复杂路径中的内存泄露检测。通过结果定位了内存泄露的位置和个数，充分证明了该方法的正确性和可行性。

本文在原KLEE的基础上进行了Z3求解器的并行移植，最终通过求解数据分析出每条路径对每条路径分别进行内存泄露检测，提高了内存泄露检测的范围。但是对于爆炸路径的程序，这种检测方法工作量将极其巨大，通过本文中已经解决的复杂路径的检测方法可以进行推广、优化，为解决爆炸路径提供了参考。

[1] Joy M M, Mueller W, Rammig F J. Source code annotated memory leak detection for soft real time embedded systems with resource constraints[C]//Dependable, Autonomic and Secure Computing (DASC), 2014 IEEE 12th International Conference on. IEEE, 2014: 166-172.

[2] Parashar S, Parashar A. Application Specific Data Trace Cache Design[J]. International Journal of Computer Applications, 2011, 22(5): 18-21.

[3] Bellinger A M, Reiken S, Carlson C, et al. Hypernitrosylated ryanodine receptor calcium release channels are leaky in dystrophic muscle[J]. Nature medicine, 2009, 15(3): 325-330.

[4] Wang G, Li N, Li F. Method of cumulative helium mass spectrometric combination test by using argon as gross-leak tracer gas: U.S. Patent Application 14/134,006[P]. 2013-12-19.

[5] Books L L C. Free Memory Management Software: Valgrind, Memcached, Mtrace, Leb128, Splint, Duma, Electric Fence, Memory Pool System, Mpatrol, Memwatch[J]. 2010.

[6] Developers V. Valgrind[J]. Web page at http://valgrind. org (2000-2005), 2010.

[7] Cadar C, Dunbar D, Engler D R. KLEE: Unassisted and Automatic eneration of High-Coverage Tests for Complex Systems Programs[C]//OSDI. 2008, 8: 209-224.

[8] De Moura L, Bjørner N. Z3: An efficient SMT solver[M]//Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 2008: 337-340.

[9] R. Martins, V. Manquinho, I. Lynce, An overview of parallel SAT solving, Constraints[R], 2012，17(3)： 304-347.

[10] H. Zhu, D. Huang, W. Zhang, Z. Wu, Y. Lu, H. Jia, M. Wang, C. Lu, The novel virulence-related gene stp of Streptococcus suis serotype 9 strain contributes to a significant reduction in mouse mortality, Microbial Pathogenesis[C], 51 (2011) 442-453.

[11] KQuery Language Reference Manual [EB/OL]. http://klee.github.io/klee/KQuery.html

[12] Serna F J. The info leak era on software exploitation[J]. Black Hat USA, 2012.

[13] Torlak E, Chandra S. Effective interprocedural resource leak detection[C]//Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering-Volume 1. ACM, 2010: 535-544.