基于GCC的符号执行工具

刘湿润

(北京邮电大学，北京 海淀 100876)

基于GCC的符号执行工具

刘湿润

(北京邮电大学，北京 海淀 100876)

静态分析和符号执行是发现源代码缺陷和提高源代码质量的两种有效方式。然而，这两种技术都面临各自的问题，静态分析误报率较高和符号执行一直面临着路径爆炸难题。为了减少静态分析和符号执行的这些限制，本文构建了一个称为ABARZER-SE的工具，它是第一个基于GCC结合符号执行和静态分析的源代码检测工具。ABAZER-SE由两个阶段组成，第一阶段是通过符号执行获取可行性路径，第二阶段应用静态分析技术对可行性路径分析找到源代码中缺陷。实验结果表明该工具具有可行性、有效性和可扩展性。

信息安全；静态分析；符号执行；GCC；误报

0 引言

静态分析是在不考虑软件运行或输入值的情况下发现软件程序中潜在错误的不可或缺的方法。目前，已经有很多静态分析工具实现用来发现程序中的错误[1-4]。静态分析的核心部分是识别软件代码中的典型错误模式。例如，一些基于Engler[5]思想的工具，使用有限状态机和检查器来表示时序性逻辑漏洞或系统规则，自动机引擎用于源代码和缺陷模式匹配[6-8]。然而，所有这些工具面临着静态分析中较高误报率的挑战。符号执行通常应用于检测系统代码[9]中的严重错误并生成高覆盖率的测试用例。然而，由于路径的数量庞大，这种技术在实际应用中面临着路径爆炸的挑战。为了减少静态分析和符号执行技术在各自应用中的弊端，本文采用一种轻量级的符号执行和静态分析相结合的方法。众所周知，已有许多成熟的基于LLVM的符号执行工具，如KLEE[9]，SAGE[10]。然而，本文的静态分析和符号执行基于GCC。尽管近年来LLVM已经得到广泛应用，但GCC仍然有其不可替代的优势，如GCC是Linux系统的标准编译器，并支持更多的平台和语言。基于以上的方法，并创建了ABARZER-SE，这是一个结合静态分析和符号执行技术的工具，用于高效地检查程序的常规属性。当分析到条件表达式时，它将使用已经收集的数据流信息来判断条件的正确性并选择正确的路径。给定一个程序属性的检查规则，ABARZER-SE执行可行的路径而不是探索其所有路径，大大降低了分析结果中的误报率。此外，它允许用户通过编写自定义检查器进行特定的静态分析。

本文的主要贡献是：

（1）实现了漏洞检测工具ABAZER-SE，第一个基于GCC分析的将符号执行和静态分析相结合的工具。

（2）使用该工具对现实世界的软件程序进行评估，结果表明ABARZER-SE可以显着降低误报率。

1 相关工作

软件漏洞的存在，降低了软件的稳定性和安全性。目前，已有很多技术尝试解决这个挑战，包括代码审查，更高层次的编程语言，测试和静态分析。尽管这些技术可以检测出一些漏洞，但是仍然有很多不足。测试是一个检测代码正确性广泛应用的方法，但是通常只训练一小部分执行路径，每条路径有一个单独输入值集合。因此，会丢失由其它输入触发的漏洞。静态分析，在发现很多类型的漏洞是非常高效的。然而，静态分析通常使用抽象提高可扩展性不能精确地推理程序的值和指针关系。因此，静态工具通常会丢失依赖于特定输入值的深层的漏洞。为了解决现有技术的不足，应之而生的是符号执行技术。通过应用符号执行技术，增加数据流信息的保存，极大的提高了分析的精确性降低了误报率。因此，利用符号执行进行软件和系统漏洞的检测具有深远的研究意义。

静态分析一直是研究领域或商业化市场中的一个活跃的主题。尤其是静态分析的误报得到了越来越多的关注。没有检查或没有准确检查不可行路径是造成误报的重要原因之一。Tripp等人[11]通过对警告进行统计学习精简静态安全检查器的输出来减少误报。Mu等人[12]提出了一种算法，构建了一个面向控制流，数据流和模块之间的相关性的数学模型以提取不可行路径。然而，这些现有的工作需要构建复杂的公式或模型并且需要大量的计算。

符号执行在最近几年重新得到了广泛关注。它可以用于自动软件测试[9]，检查严重缺陷[13,8-9]和验证路径[14]。ABAZER-SE与这些工作相似的地方是都是符号执行和静态分析的结合，最大的区别是所基于的平台ABAZER-SE基于GCC。除此之外，本文的分析基于GCC抽象语法树而不是中间语言，在编译器中抽象语法树在中间语言的前一个阶段所以抽象语法树含有更丰富的源代码信息。

目前国内外很多研究者采用静态分析和符号执行相结合的方法进行漏洞检测。2013年，WOODPECKER[8]的出现是符号执行史上的里程碑事件，首次将其用于系统规则的检查，对于通常的规则它提供了一个安装在内部checkers集合，和一个针对于用户的接口以方便用户检查新的规则。它指示与检测规则相关的符号执行程序路径，消除冗余的路径，加速了符号执行的速度；2015年，基于KLEE的UC-KLEE[15]由David等人提出，UC-KLEE一个新颖的可扩展性框架用于检查C和C++代码，通过直接检测单个函数而不是整个程序提高可扩展性。Su等人[16]采用将符号执行和反例引导下基于精炼抽象模型相结合检测方法，对于可行的测试目标输出测试数据，减少不可行的测试目标。但是以上所有的符号执行分析都基于llvm低层虚拟机平台，利用clang前端编译器将程序生成中间代码提取信息进行分析。

2 实现

2.1 指令模拟

符号执行的核心思想是模拟程序运行以获得精确的数据流信息。ABAZER-SE基于GCC前端，从抽象语法树提取数据流信息和进行内存模拟是ABAZER-SE的主要研究内容。

2.1.1 内存模型

内存模型是语义模拟的基础并是ABAZER-SE的核心组成部分。构建内存模型的一个极端是将存储器空间视为单字节数组[18]。显然这样具有相当高的精度，但是它的可扩展性非常差，并伴随着巨大开销。Burstall内存模型[19]广泛应用于类型安全代码分析。该模型的主要概念是将存储器分成不相交的空间，但是它不够准确。为了对内存进行建模，构建了一个新颖的内存模型，该内存模型可以精确地将每个左值表达式映射到相应的内存对象上。与上述所提到的内存模型相比，该模型具有很大的优势。它支持更丰富的数据类型，包括基本类型，如void，char，integer和floating-point，以及派生类型，如pointer，array和struct。它可以处理各种算术运算。此外，构建了特定的内存模型结构来处理地址不确定的数据。在C语言中，有三种存储区域：栈（本地），静态区域（全局）和堆（动态分配的内存）。在该符号分析模型中，也遵循C语言的存储策略。本文中的内存模型基于分层机制并支持整数类型，浮点类型，指针，数组和结构类型的存储。

为了更好地理解本文所构建的内存模型，通过图1和图2进一步阐释说明，图1是要分析的程序片段，其对应的内存模型则如图2。第一层中的内存单元主要包含程序中定义的变量，第二层内存单元主要包含的内容是第一层指向的元素，后续的内存单元以相同的方式分配。数组a 有五个字段，变量a指向该数组。指针p指向数组的首地址。结构体ss指向包含其结构字段的内存单元。结构体ss的第一个字段的值为1，因此相应的内存单元记录值1。此外，为了处理浮点数运算，因此该内存模型也支持浮点数的存储。浮点数b的值通过调用函数scanf获得，因此并不知道其具体值，所以赋给它一个符号值sym1。

图1 代码片段

图2 图1代码的内存模型

2.1.2 指令语义的模拟

接下来，将使用上一节中构建的内存模型来进行语句语义的模拟。为了收集数据流信息，指令语义模拟主要计算变量的值和地址。模拟指令语义的核心操作是操作符的处理。目前，已经模拟了32个运算符的语义，包括算术运算符，逻辑运算符，关系运算符，指针解引用，数组，结构引用等等。目前，已经实现了C语言中73%操作符的语义模拟。

AST是表示源代码的抽象语法结构。树中的每个节点都包含着源代码的信息。首先，模拟工作从AST根结点开始，然后递归解析抽象语法树的左子树和右子树。一个表达式的树编码类型表示此表达式的类型同时也是指令语义模拟分析的基本结构，树编码类型可以使用宏操作TREE_CODE获取。接着，在第一步中获得的树编码类型可以决定需要模拟的语义。如果表达式是一个变量声明或一个参数声明表达式，可以从抽象语法树中得到该变量或参数的类型、名字和其他有关信息，然后为该变量分配内存存储单元。如果表达式是算术运算，逻辑运算，关系运算或内存引用操作表达式，可以从抽象语法树中获取操作符和操作数并递归地计算它们的值。需要计算操作数的地址还是值由第一步中的获得的树编码决定。最后，使用获得的操作数的值并基于操作符的语义完成相应操作运算。

图3展示了赋值表达式a=1的抽象语法树。该赋值表达式的语义是给变量a赋值1。为了模拟该语句的语义，使用该操作TREE_CODE(a=1)可以得到该表达式的树编码类型MODIFY_EXPR。为了模拟MODIFY_EXPR的语义，需要得到左操作数（左子树）的地址和右操作数（右子树）的值。左子树是一个VAR_DECL表达式，相应的变量地址可以从内存模型中获取。右子树是一个INTERGER_CST树结点，值1可以通过宏操作直接从AST上获取。最后一步是将值1存储到变量的地址。至此，完成了对表达式a=1的语义模拟。

2.2 不确定性内存地址的处理

图3 赋值语句a=1的抽象语法树

不确定性地址数据的处理是符号执行的挑战之一。当然在本文的分析过程中，也面临着这个问题。例如，指针间接引用*(p + i)中变量p指向数组头地址，变量i为输入变量即其值不确定。对于这种情况，不能从已构建的内存模型中获取*(p+i)值，因为无法得到p + i指向的地址。为了解决这个问题，创建了特定的内存结构。通过创建链表，用链表结点来存储此特定数据类型。链表结点字段包括值，类型和索引。如果链表结点没有具体值，则将为其分配符号值。可以在链表中频繁地添加或查询结点进行不确定地址的处理。

2.3 约束求解

为了检查生成的约束集的可满足性，本文使用Z3求解器来检查。Z3是由微软公司开发的一种新型的高效的SMT求解器，可从微软官网上免费下载。Z3通常用于验证各种软件和分析应用程序。可满足性模理论（SMT）问题是关于一阶逻辑公式的决策问题，涉及很多理论背景知识，例如：算术、位向量、数组和未解释函数[17]。ABARZER-SE使用由Z3提供的API进行约束求解。首先，将路径条件转换为由Z3可以识别的SMTLIB2.0标准形式。然后，将路径条件传送到Z3接口进行约束求解。最后，ABARZE-SE可以根据求解器的返回值确定路径可行性。

3 实验

图4 实验代码

如图4所示实验代码样本，代码中包含不可达路径。ABAZER检测该代码时无法识别其中的不可达路径，故对所有路径都会进行分析，导致在不可达路径中检测到内存泄露和指针未分配空间即释放的问题，而ABAZER-SE分析该代码时，通过符号执行分析得到b=(int*)malloc(4)语句执行结束后表示2*m-1=n条件成立且m已经被赋值为20，通过符号执行的分析可知m+n<=16是不可能成立的，故不存在指针为分配空间即释放问题。上述两种缺陷的误报在ABAZER-SE的分析结果中不会出现。以此证明，引入符号执行可有效裁剪不可达路径，降低ABAZER的误报率。

表1显示了ABAZER-SE与ABAZER实验结果对比，包括真阳性、误报率和运行时间，人工验证了所有的误报。实验测试对象为Coreutils 6.11，由于ABAZER-SE是基于规则的漏洞扫描工具，故在实验过程中主要关注三类缺陷，包括内存泄漏，约束溢出和除零错误。结果说明ABAZER-SE在对检测出真正缺陷没有影响的情况下可以有效减少误报误报，并且时间开销在可以接受的范围内。

表1 ABAZER-SE与ABAZER实验结果对比

4 结论

在本文中，使用符号执行技术来减少静态分析中的误报。ABAZER-SE是第一个在GCC上构建的符号执行引擎，从GCC语法树中提取信息进行符号化分析，最终构建了ABAZER-SE漏洞检测工具。虽然已有一些成熟的符号执行工具在LLVM上实现，实验结果表明，基于GCC的符号执行仍然有其相对优势。使用符号执行技术和静态分析两种技术互补检测源代码中的缺陷,利用符号执行提供的足够的数据流信息提高静态分析的精确性。当然，由于ABAZER-SE符号化分析还不够完善该工具还在构建中，目前还不能解析位运算符，与KLEE相比其分析精度还不够高，接下来我们会进一步完善该工具。

[1] PolySpaceVerifier, http://www.softdevtools.com/modules/weblinks/ singlelink.php?lid=116(2007).

[2] Coverity-A Higher Code, http://www.coverity.com/library/pdf/coverity_prevent.pdf (2008).

[3] CodeSonar Source-Code Analyser, http://www.scl.com/grammatech/codesonar (2008).

[4] Papcun J. Integrating Static Code Analysis and Defect Tracking[D]. Masarykova univerzita, Fakulta informatiky, 2014.

[5] Engler D, Chelf B, Chou A, et al. Checking system rules using system-specific, programmer-written compiler extensions[C]// Proceedings of the 4th conference on Symposium on Operating System Design & Implementation-Volume 4. USENIX Association, 2000: 1.

[6] Kremenek T. Finding software bugs with the clang static analyzer[J]. California: Apple Inc, 2008.

[7] Ivannikov V P, Belevantsev A A, Borodin A E, et al. Static analyzer Svace for finding defects in a source program code[J]. Programming and Computer Software, 2014, 40(5): 265-275.

[8] Cui H, Hu G, Wu J, et al. Verifying systems rules using rule-directed symbolic execution[J]. ACM SIGARCH Computer Architecture News, 2013, 41(1): 329-342.

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

[10] Godefroid, P., Levin, M. Y., Molnar, D. Automated white box fuzz testing[C]. NDSS'08, Proceedings of the conference on Network and Distributed System Security Symposium. USA, 2008: 151-166.

[11] Tripp O, Guarnieri S, Pistoia M, et al. Aletheia: Improving the usability of static security analysis[C]//Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security. ACM, 2014: 762-774.

[12] Mu Y, Zheng Y, Zhang Z, et al. The algorithm of infeasible paths extraction oriented the function calling relationship[J]. Chinese Journal of Electronics, 2012, 21(2).

[13] Zhang Y, Clien Z, Wang J, et al. Regular property guided dynamic symbolic execution[C]//Proceedings of the 37th International Conference on Software Engineering-Volume 1. IEEE Press, 2015: 643-653.

[14] D. A. Ramos and D. R. Engler. Practical, low-effort equivalence verification of real code. In Proceedings of the 23rd international conference on Computer aided verification, CAV’11, pages 669–685, 2011.

[15] LAHIRI, S., HAWBLITZEL, C., KAWAGUCHI, M., AND REBELO, H. SymDiff: A language-agnostic semantic diff tool for imperative programs. In Proc. of Intl. Conf. on Computer Aided Verification (CAV) (2012).

[16] Su, Ting, et al. "Combining symbolic execution and model checking for data flow testing." 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering. Vol. 1. IEEE, 2015.

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

[18] Clarke E, Kroening D, Lerda F. A tool for checking ANSI-C programs[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 2004: 168-176.

[19] Burstall R M. Some techniques for proving correctness of programs which alter data structures[J]. Machine intelligence, 1972, 7(23-50): 3.

The Symbolic Execution Tool Based on GCC

LIU Shi-run
(Beijing University of Posts and Telecommunications, Beijing city Haidian District Xitucheng Road No. 10)

Static analysis and symbolic execution are two powerful ways of finding bugs and improving the quality of software. However, both of these techniques face their respective issues, e.g. false positives with static analysis tools and path explosion with symbolic execution method. To mitigate these limitations of static analysis and symbolic execution, we present a tool called ABARZER-SE, which is the first to implement symbolic execution and static analysis based on GCC. The workflow of ABAZER-SE consists of two phases, the first phase is to achieve feasible path by using symbolic execution, the second combines static analysis to analyze potential bugs. Experiment results show the effectiveness and scalability of the tool when it is used to analyze real-world software.

Static analysis; Symbolic execution; False positives; GCC

TP311.1

A

10.3969/j.issn.1003-6970.2016.12.022

本文著录格式：刘湿润. 基于GCC的符号执行工具[J]. 软件，2016，37（12）：97-101