（计算机科学与技术专业论文）面向符号执行的内存模型研究.pdf

国防科学技术大学研究生院硕士学位论文 摘要 在软件可信性质保证的诸多方法中，面向软件源代码的分析与验证具有重要 意义。形式化方法在软件可信性质保证中有不可替代的作用，但是距离大规模广 泛应用还有不小的差距。符号执行是一种重要的形式化方法，在测试数据生成和 静态分析中有广泛应用。但是，符号执行面临一些问题。其中，内存模型是影响 符号执行的精确性和可扩展性的主要问题之一。 论文综述了面向符号执行的内存模型问题的研究现状，分析了符号执行中符 号状态跟踪面临的主要问题和现有的内存抽象的不足，提出了基于抽象符号表的 内存模型。抽象符号表的基本思想是，通过为可寻址对象生成抽象地址统一处理 各种数据类型和建模内存操作。研究了使用抽象符号表建立内存模型的方法，给 出了抽象地址生成方法以及符号执行算法。基于抽象符号表的内存模型能够很好 地解决面向符号执行的内存模型面临的主要问题，包括指针和别名问题、类型不 安全的内存访问和大小不确定的数据。最后，通过实验评估了基于抽象符号表的 内存模型，设计的一个符号执行工具能够精确地跟踪符号状态，并且通过与其他 内存模型的比较，说明了这个内存模型具有一定的可扩展性。 精确而且可扩展的内存模型是提高符号执行技术的实用性的关键，能够有效 地推动符号执行技术在软件可信性质保证中的深入应用。本文提出了基于抽象符 号表的内存模型，对符号执行技术的发展和应用有一定的积极意义。 主题词：符号执行，内存模型，抽象符号表，静态分析，l l v m 第i 页 国防科学技术大学研究生院硕士学位论文 a b s t r a c t a m o n go t h e rm e t h o d s ，s o u r c ec o d e b a s e da n a l y s i sa n dv e r i f i c a t i o np l a y sa l l i m p o r t a n tr o l e i nt h ea s s u r a n c eo fs o f t w a r et r u s t w o r t h i n e s s f o r m a lm e t h o d sa r e i r r e p l a c e a b l ei nt h ea s s u r a n c eo fs o f t w a r et r u s t w o r t h i n e s s ，b u tt h e yr e m a i nb e f o r et h e s t a g eo fm a s s i v ea n db r o a da p p l i c a t i o n s s y m b o l i ce x e c u t i o ni sa ni m p o r t a n tf o r m a l m e t h o dt h a th a st h ep e r s p e c t i v eo fb r o a da p p l i c a t i o n si nt h ea r e a so ft e s td a t ag e n e r a t i o n a n ds t a t i ca n a l y s i s h o w e v e r ，t h e r ea r es e v e r a ld i f f i c u l t i e sf a c i n gs y m b o l i ce x e c u t i o n , o n eo fw h i c hi st h em e m o r ym o d e lu s e dt h a ti so n eo fm a i ns o u r c e so fs y m b o l i c e x e c u t i o n sp o o rp r e c i s i o na n ds c a l a b i l i t y t 1 1 i sp a p e rs u r v e y st h er e s e a r c ha b o u tm e m o r ym o d e l sf o rs y m b o l i ce x e c u t i o n m a i nc h a l l e n g e so fm e m o r ym o d e l sf o r s y m b o l i ce x e c u t i o na r ep r e s e n t e da n d d r a w b a c k so fc u r r e n ta p p r o a c h e sa r ed i s c u s s e d t h ea b s t r a c ts y m b o lt a b l e - b a s e d m e m o r y m o d e li sp r o p o s e d t h em a i ni d e ao ft h ea b s t r a c ts y m b o lt a b l ei st h eg e n e r a t i o n o fa na b s t r a c ta d d r e s sf o re v e r ya d d r e s s a b l eo b j e c tt oh a n d l ev a r i o u sd a t at y p e sa n d m e m o r yo p e r a t i o n su n i f o r m l y a b s t r a c ts y m b o lt a b l e sa r e t oa b s t r a c tt h eu n d e r l y i n g m e m o r yo fp r o g r a m s ，a n dt h ea p p r o a c ho fg e n e r a t i o no fa b s t r a c ta d d r e s s e sa n dt h e a l g o r i t h mo fs y m b o l i ce x e c u t i o nu s i n gt h ea b s t r a c ts y m b o lt a b l e - b a s e dm e m o r ym o d e l a r ep r e s e n t e d t h ea b s t r a c ts y m b o lt a b l e - b a s e dm e m o r ym o d e lc a no v e r c o m em a i n p r o b l e m so fm e m o r ym o d e l sf o rs y m b o l i ce x e c u t i o nv e r yw e l l ，i n c l u d i n gt h ep r o b l e mo f p o i n t e ra n da l i a s i n g ，t y p e - u n s a f em e m o r ya c c e s s e sa n dd a t aw i t h o u tc o n c r e t es i z e a t l a s t ，as i m p l es y m b o l i ce x e c u t i o nt o o li si m p l e m e n t e d ，t h r o u g hw h i c ht h ea b s t r a c t s y m b o lt a b l e - b a s e dm e m o r ym o d e l i s e v a l u a t e d e x p e r i m e n t ss h o wt h i sm e m o r y m o d e l sp o w e ro fp r e c i s et r a c ko fs y m b o l i cs t a t ea n di t sa c c e p t a b l es c a l a b i l i t yb yt h e c o m p a r i s o nw i mt h em o n o l i t h i cm e m o r y m o d e l ap r e c i s ea n ds a l a b l e m e m o r ym o d e li s t h e k e yo fs y m b o l i ce x e c u t i o n s p r a c t i c a b i l i t y ，w h i c hw i l lp r o m p tt h ed e 印a p p l i c a t i o no fs y m b o l i ce x e c u t i o ni nt h e a s s u r a n c eo fs o f t w a r et r u s t w o r t h i n e s s t h ep r o p o s e da b s t r a c ts y m b o lt a b l e b a s e d m e m o r ym o d e lw i l lm a k ep o s h i v ei n f l u e n c eo nt h er e s e a r c ha n da p p l i c a t i o no fs y m b o l i c e x e c u t i o n k e yw o r d s ：s y m b o l i ce x e c u t i o n , m e m o r ym o d e l ，a b s t r a c ts y m b o lt a b l e ，s t a t i c a n a l y s i s ，l l v m 第i i 页 国防科学技术大学研究生院硕士学位论文 表目录 表4 1 符号执行图4 1 中代码片段得到的抽象符号表2 6 表4 2 符号执行图4 2 代码片断得到的抽象符号表3 0 表6 1符号执行工具分析程序的时间4 6 第1 i i 页 国防科学技术大学研究生院硕士学位论文 图2 图2 图2 图3 图 图 图 图 图 图 图 图 2 3 4 5 图4 5 图4 6 图4 7 图5 1 图5 2 图6 1 图6 2 图6 3 图目录 求两个整数的最大值的代码片段。5 用i f e l s e 语句和g o t o 语句表示w h i l e 语句6 路径模拟引擎的结构9 符号执行系统整体结构1 6 符号状态中m 的语义17 单片内存模型定义的动态内存分配的语义1 7 单片内存模型l9 b u r s t a l l 内存模型2 0 一个演示抽象地址生成的代码片段2 6 一个简单的演示指针别名的代码片段3 0 演示不同内存模型处理类型转换方式的代码片段31 字节数组方法在图4 3 代码片段的l 2 处的内存布局3 l 单片内存模型方法在图4 3 代码片段的l 2 处的内存布局3 2 a s t a b l e 方法在图4 3 代码片段的l 1 处的内存布局3 2 a s t a b l e 方法在图4 3 代码片段的l 2 处的内存布局3 2 符号执行中一般的约束求解器判定公式的过程。3 7 p r e s b u r g e r 算术定义3 8 符号执行工具结构4 4 实验中使用的一个代码片段4 5 图6 2 中l 4 和l 5 之间程序点的符号状态4 5 第1 v 页 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得 的研究成果尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含 其他人已经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它 教育机构的学位或证书而使用过的材料与我一同工作的同志对本研究所做的任 何贡献均已在论文中作了明确的说明并表示谢意。 学位论文题目：亘囱签曼执盈鲍凼盔搓型珏究 学位论文作者签名：主羔日期：z p 1 年- 2 月工7 日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留、使用学位论文的规定。本人授权 国防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子 文档，允许论文被查阅和借阅；可以将学位论文的全部或部分内容编入有关数据 库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文 ( 保密学位论文在解密后适用本授权书。) 学位论文题目： 亘自签曼执征鲍卤盔搓型珏究 学位论文作者签名： i 基丕互 作者指导教师签名：一互暖璺一 日期：如j 7 年，z 月巧日 日期：1 年p 月7 日 国防科学技术大学研究生院硕士学位论文 第一章绪论 1 1 课题研究背景和意义 随着软件承担的功能和作用越来越重要，软件失效的代价也越来越大，直至 不能容忍。软件错误给美国造成每年6 0 0 多亿美元的经济损失1 1 1 。软件的可信性质 受到国内外研究机构、政府和企业的广泛关注。软件的可信性质包括可靠性、安 全性( 包括可靠安全性( s a f e t y ) 和保密安全性( s e c u r i t y ) ) 、可用性等性质。其 中，可靠性是指在规定的时间内和规定的运行环境下，软件正常运行的能力。软 件可信性质保证是一个系统工程，贯穿软件整个生命周期，从需求分析到软件设 计，直至实现与维护，每个阶段都需要进行相应的软件可信性质保证活动。其中， 面向软件源代码的分析与验证在软件可信性质保证中具有重要意义。其中一个重 要原因是源代码是软件的最终体现，源代码的正确性才能保证软件运行的可靠性。 形式化方法在软件可信性质保证中有不可替代的作用，但是目前距离大规模广泛 应用还有不少差距。符号执行是一种应用广泛的形式化方法。符号执行本身包括 路径可行性分析，而静态分析方法面临的一个严重问题是误报率太高。因此，使 用符号执行技术分析静态分析的结果能排除大量的因为路径的不可行导致的误 报，提高分析结果的精确性。同时，把符号执行作为静态分析引擎，使静态分析 获得了路径敏感性。在符号执行过程中，通过断言能发现大量的编码错误。另外， 符号执行在测试数据生成方面有广泛应用，是近期的一个研究热点。 符号执行系统包括解释器、约束求解器和内存模型三个主要部分。解释器执 行代码操作的符号语义，约束求解器判定约束公式，内存模型的作用是跟踪符号 状态。为了支持一些复杂的语法成分，比如类型不安全的内存访问( 比如，c 代码 中常常出现的类型转换) ，内存模型需要足够精确。与其他静态分析一样，符号 执行也需要面对指针和别名问题。同时，符号执行必须处理一些特殊问题，比如 函数的参数是包含无界数据的复杂数据结构。当程序规模较大时，需要记录大量 的符号状态，数据读写的时间消耗也不可忽视。这时，内存模型的性能( 可扩展 性) 成为制约其实用性的关键。鉴于这些问题，设计一种精确、具有一定的可扩 展性( c a l a b i l i t y ) 的内存模型，支持各种数据类型和语法成分，是推动符号执行深 入、广泛应用的关键。 本课题的基本任务是研究面向符号执行的内存模型问题，解决其中涉及的关 键问题。相关理论和方法可指导符号执行和静态分析的研究与应用，有广泛的应 用前景。 本课题的研究意义体现在理论和实践两个方面。在理论上，提出了一种实用 第1 页 国防科学技术大学研究生院硕士学位论文 的面向符号执行的内存模型；在实践上，有利于符号执行技术的研究，并有利于 符号执行技术在工业领域的推广应用。 1 2 课题研究内容 符号执行是一种被长期研究的技术。近期，由于硬件性能的提高以及其在静 态分析、错误查找和测试等方面的广泛应用前景，符号执行引起了研究者的极大 研究热情。如何处理源代码的各种数据类型和语法成分，跟踪符号状态，以得到 路径条件是符号执行必须解决的问题。内存模型的对程序的支持能力和它的运行 性能严重影响着整个符号执行系统的精确性和可扩展性。 本课题研究的基本内容是符号状态跟踪的困难和问题所在，给出解决方案， 最终提出一种精确并且实用的面向符号执行的内存模型。具体研究内容包括： 1 ) 定义内存模型在符号执行系统中的角色和功能，总结相关研究工作； 2 ) 研究符号状态跟踪所面临的问题，以及符号执行必须解决的特殊问题； 3 ) 研究通过为可寻址对象分配抽象地址统一处理各种数据类型和语法成分 的方法，以及基于抽象符号表建模符号内存的方法； 4 ) 通过把约束公式转换为一般形式研究使用通用的定理证明器判定内存模 型特定的约束公式的方法； 5 ) 在l l v m 框架下编写符号执行工具，进行试验，以及实验结果分析。 1 3 论文结构 论文共分为七章。 第一章是绪论。主要介绍了课题的研究背景和意义、研究内容，以及论文结 构。 第二章概述符号执行的一般过程和基本概念，总结符号执行技术的应用领域 和应用状态，综述符号执行技术的当前研究状况。 第三章介绍了符号状态跟踪面临的问题和一般的解决方法，定义了内存模型 在符号执行系统中的位置和作用，并综述了面向符号执行的内存模型的研究现状。 第四章介绍了抽象符号表的概念和基本方法，给出了抽象地址的生成方法和 符号执行算法。 第五章给出了使用抽象符号表建模符号内存的方法，定义了内存操作的语义， 讨论了使用通用定理证明器求解约束公式的方法，最后讨论了内存模型性能优化 策略。 第六章介绍了l l v m ，实现了一个符号执行执行工具，进行试验，并给出了 第2 页 国防科学技术大学研究生院硕士学位论文 相应的实验结果。 第七章总结了论文的主要工作，明确了需要进一步加强的工作和可能的进一 步研究方向。 1 4 论文研究成果 本文的主要贡献和创新工作主要包括以下三个方面： 1 ) 提出了抽象符号表的概念。抽象符号表通过为可寻址对象生成抽象地址达 到了统一处理各种数据类型和语法成分的目的。 2 ) 提出了支持符号执行的基于抽象符号表的内存模型。定义了数据读写操作 的实现，定义了内存相关操作的语义，提出一种通过公式转换使用通用定理证明 器判定内存模型相关的公式的方法，以及讨论了内存模型的运行性能优化技术。 3 ) 实现了一个基于l l v m 的简单符号执行工具，通过实验评估了基于抽象符 号表的内存模型。 第3 页 国防科学技术大学研究生院硕士学位论文 第二章符号执行概述 符号执行技术使用符号值代替数字值执行程序，得到的变量的值是由输入变 量的符号值和常量组成的表达式。符号执行技术首先由k i n g 在1 9 7 6 年提出【引，经 过三十多年的发展，现在仍然被广泛研究，它在软件测试和程序验证中发挥着重 要作用。符号执行是一种重要的形式化方法和静态分析技术，它使用数学和逻辑 符号抽象，优点体现在普遍性( g e n e r a l ) 和严格性( r i g o r o u s ) 两个方面p j 。普遍 性是指一次符号执行相当于常规执行一组( 可能无限多个) 输入( 称为输入等价 类) ；严格性是指符号执行获得变量和路径条件的逻辑表达式，通过严格的推理， 可以得到程序的多种性质。 2 1 符号执行的基本原理 首先，定义一些基本概念。程序的路径( p a t h ) 是程序的一个语句序列，这个 语句序列包括程序的一些顺序的代码片段，代码片段之间的连接是由于分支语句 导致的控制转移。一个路径是可行的( f e a s i b l e ) ，是指存在程序输入变量的至少 一组值，如果以这组值作为输入，程序将沿着这条路径执行。否则，路径就是不 可行的( i n f e a s i b l e ) 。路径条件( p a t he o n d i t i o n ，p c ) 是针对一个路径的，它是一 个关于程序输入变量的符号值的约束，一组输入值使得程序沿着这条路径执行当 且仅当这组输入值满足这条路径的路径条件。 符号执行是常规执行的自然扩展【2 】。符号执行使用输入变量的符号值模拟执行 程序，各种操作在符号上进行。与常规的基于确定值的程序执行不同，符号执行 过程中变量的值是由符号和常量组成的表达式。需要解释一下符号执行为什么需 要路径条件。常规执行的程序状态包括堆、栈和寄存器的状态，以及程序计数器。 其中，堆、栈和寄存器的状态表示在某个执行位置上各个变量的取值。符号执行 的状态( 以下称为符号状态) 同样包括变量的取值和程序计数器，除了变量的值 是符号值外，其他的含义与常规执行类似。然而符号执行有一种特殊的情况，考 虑符号执行分支语句。由于符号值的不确定性，分支条件的真值可能是不确定的， 即如果取恰当的输入值，多个分支路径都是可能被执行的。这时，继续执行某一 个分支路径时，需要对分支条件做相应的假设，并把假设记录下来。所执行过的 路径上的所有假设的逻辑合取就是这个路径的路径条件。 下面以一个简单的例子演示符号执行的过程，如图2 1 所示。首先为输入变量 a 和b 分别指定符号值a 和b ( a 和b 表示任意的整数值) ，从语句l 1 开始执行 程序，变量x 的值未定义。执行到l 2 时，要判断a 和b 的大小关系，由于a 和 第4 页 国防科学技术大学研究生院硕士学位论文 b 的值不定，其大小关系也不确定。要使程序继续执行下去，必须做出假设a = b 或者a = b 下，符号执行的路径是p a t h l ：l 1 一l 2 _ l 3 _ l 5 ， r e t u r n 语句处x 的值为a 。在假设a = b ，p a t h 2 的p c 是a b 。 图2 1 求两个整数的最大值的代码片段 符号状态包括三部分，变量到其符号值的映射、程序计数器和路径条件。记 符号状态为s y m b o l i c s t a t e ，则s y m b o l i c s t a t e = 。其中： 一m 是变量到符号值的映射； i p 是指令指针，即程序计数器，指向下一个要执行的语句； 一p c 是路径条件。 程序通过编译生成面向硬件机器的目标代码，编译器定义了编程语言的语义。 同样地，可以为编程语言定义精确的符号语义。编程语言的符号语义针对以符号 为输入对程序的执行，它定义各种数据类型的符号表示，操作符如何计算符号数 据，以及定义在符号状态下，程序控制的流动。如同常规执行，符号执行语句s 使得符号状态从s y m b o l i c s t a t e = 更新为s y m b o l i c s t a t e 7 = 。初始符号状态设置如下：p c 的初始值设为t r u e ，口指向程序的第一条语句， m 把每个输入变量映射到互不相同的符号。下面定义编程语言中基本语句类型的 符号语义。 1 ) s 为赋值语句。计算赋值语句右侧表达式的符号值，把得到的表达式赋值 给左侧的变量，m 更新为m 。i p 指向下一条语句，p c p c 。 2 ) s 是分支语句。以i f ( c ) s le l s es 2 为例。调用约束求解器判定公式p c c ( “一 表示逻辑蕴涵) ，如果为真，更新i p ，口，指向s l 的第一条语句。m7 = m ， p c = p c 。否则，判定公式p c 一一c ，如果为真，更新m ，i p7 指向s 2 的第一条 语句。m = m ，p c = p c 。如果p c c 和p c 一一c 都不为真，则t h e n 和e l s e 分支路径都是可能被执行的。复制s y m b o l i c s t a t e 为s y m b o l i c s t a t e l = 和s y m b o l i c s t a t e 2 = ，分别对应t h e n 分支和e l s e 分支。再做更新： 第5 页 国防科学技术大学研究生院硕士学位论文 m i = m 2 = m ，i p l 指向s l 的第一条语句，i p 2 指向s 2 的第一条语句，p c i = p c 八c ， p c 2 = p c 八一c 。 3 ) s 是函数调用。有两种基本的方法处理函数调用，宏扩展和函数摘要 ( f u n c t i o ns u m m a r y ) 。如果采用函数摘要方式，则装载被调用函数的摘要，根据 函数摘要的内容，更新符号状态，可能分出多个分支路径。如果采用宏扩展方式， 把控制转移到被调用函数内，进行参数值的传入，退出函数时进行返回值的传出。 4 ) s 是循环语句。g o t o 语句已经被多数现代编程语言摒弃，但是g o t o 语句 的符号语义却很简单，只需要把控制转移到相应的语句。循环语句可以用i f e l s e 语句和g o t o 语句表示，其符号语义由i f e l s e 语句和g o t o 语句的符号语义定义。 图2 2 演示了把w h i l e 语句转换为i f e l s e 语句和g o t o 语句组合的方法。有关符 号执行更详细的说明可以参考 2 】。 图2 2 用i f e l s e 语句和g o t o 语句表示w h i l e 语句 2 2 符号执行的应用 本节从两个方面总结符号执行的应用：测试数据生成、静态分析和错误查找。 2 2 1 测试数据生成 符号状态中包括路径条件p c ，求解p c 可以得到多组程序输入变量的值，使 用任意一组值做输入执行程序，程序都会沿着p c 对应的程序路径运行。所以，这 组值就是使程序执行相应路径的测试用例。可见，测试数据生成是符号执行的自 然应用，当时k i n g 提出符号执行的概念时就指出，软件测试是其主要应用之一。 基于符号执行自动生成测试数据的基本方法是符号执行被测试程序，求解路径条 件即得到执行相应路径的测试数据。基于符号执行的测试数据生成属于白盒测试 方法，主要应用在单元测试中。 典型的应用是符号执行技术与面向路径测试方法的结合。面向路径测试方法 的重要一步是依据覆盖标准( 语句覆盖、分支覆盖等) 选出一组路径，但是很多 程序路径是不可行的【4 1 ，如果选中这样的路径，则不存在相应的测试数据，无法达 第6 页 国防科学技术大学研究生院硕士学位论文 到相应的覆盖标准。符号执行本身包括路径可行性分析，可以用来剔除不可行路 径。文献【5 】给出了一个为基本路径测试生成可行路径的算法。大致思想是不断地 提取路径，对符合基本路径条件的路径先使用符号执行做可行性分析，只把可行 的路径添加到基本路径集合中，直至基本路径集合构造完成。符号执行技术与面 向路径测试方法结合的优势体现在测试数据生成的完全自动化和路径的可行性。 符号执行也被引入到面向对象程序的单元测试中。面向对象的单元测试的测 试对象是类，测试数据包括两个部分：方法调用序列和每个方法调用的参数。文 献 6 】定义了面向对象程序的符号状态，是一个约束( c ) 和一个符号堆( h ) 组成 的二元组 。其中，符号堆被建模为一个有向图，节点是对象，包括简单类 型数据，边表示对象间的成员( 域) 关系。即一条有向边从0 l 指向晓，表示d 2 是d l 的成员。表示数组和其元素之间的边还要标上相应元素的数组索引。状态 空间包括符号执行所有可能的被测试类的方法序列所产生的符号状态。s y m s t r a 6 1 做符号状态空间探测的基本方法是，使用宽度优先搜索策略，探测符号执行长度 不超过一个固定值的方法调用序列所产生的所有符号状态。在符号状态空间探测 过程中，使用状态包含( s u b s u m p t i o n ) 剪除部分待探测的状态空间。即，检查待 探测状态空间，如果存在一个已经探测的状态空间包含这个状态空间，则剪除这 个状态空间。基于状态包含的状态空间剪除技术使得s y r n s t r a 可以探测大规模的程 序。s y m s t r a 通过系统地探测符号状态空间，生成方法调用序列和方法参数。该方 法的优势体现在完全自动化以及能够产生覆盖所有方法调用序列的测试用例。 c o n c o l i c ( c o n c r e t ea n ds y m b o l i c ) t t j i 贝t j 试是一种新的测试数据生成方法，它基 于c o n c o l i c 执行，即同时常规执行和符号执行程序。c o n c o l i c 执行以一个随机输入 开始执行程序，同时跟随着符号执行，符号执行的目的是收集被执行路径的路径 条件。当执行一个路径结束时，调用约束求解器求解这个路径的p c 的一个变种， 变种与路径探测策略有关。求解的结果作为程序输入开始新一轮执行，它将迫使 程序在新的路径上执行。通过这样的不断迭代，最终将探测到程序的所有可执行 路径。c o n c o l i c 测试又被称为d a r t ( d i r e c t e da u t o m a t e dr a n d o mt e s t i n g ) s l ，或 者动态符号执行( d y n a m i cs y m b o l i ce x e c u t i o n ) 桫j 。文献 8 有c o n c o l i c 测试的算法 的详细描述。同传统静态符号执行相比，c o n c o l i c 测试可以利用常规执行所得到的 信息。c o n c o l i c 测试不需要所有的操作都符号地执行，也不要求所有的变量一定取 符号值，在路径条件的收集过程中，一些变量可以用具体值代替符号值，些难 以符号地处理的操作可以使用具体值进行执行。根据文献 8 】，c o n c o l i c 测试有两个 主要优势。其一是发现的任何错误都是真实的错误，因为存在具体输入值使得程 序执行到错误位置；其二是，缓解了约束求解器的能力不足的问题。在分支语句 处，即使约束求解器不能判定分支路径的可行性，伴随的常规执行表明了一个可 第7 页 国防科学技术大学研究生院硕士学位论文 行分支路径，使得符号执行可以继续执行。c o n c o l i c 测试是符号执行和随机测试的 结合，部分地克服了符号执行技术的可扩展性差和随机测试覆盖率低的问题。 0 8 年底发表的研究成果k l e e 1 0 j 是一个完全自动化的测试数据产生工具和错 误查找工具，它为g n uc o r e u t i l s 工具包中的8 9 个独立程序生成的测试数据 的平均代码覆盖率高达9 0 以上。k l e e 通过大量的实验数据表明了符号执行技术 在测试数据生成上的现实应用的前景。 2 2 2 静态分析和错误查找 静态分析工具面临的一个主要问题是产生太多的误报( f a l s ep o s i t i v e s ) ，而人 工检查这些误报费时费力。不精确性成为静态分析方法推广应用的主要障碍。由 于很多程序路径是不可行的1 4 j ，静态分析工具产生的误报中，相当一部分是因为误 报所在的路径是不可行的。由于符号执行技术包含路径可行性分析，符号执行成 为提高静态分析的精确性的主要方法之一。 虽然可以检查功能错误【l o 】，基于符号执行的错误查找方法主要应用于检查程 序的一些编程错误，比如空指针解引用、数组越界、内存泄漏等。某些程序正确 性质可以表示为约束形式的规则，由于符号执行精确地记录了每个执行位置的符 号状态，通过判定这些规则的可满足性就可以检查程序是否有相应的错误发生。 基于符号执行的错误查找的基本方法是，符号执行程序，在符号执行的过程中， 针对特定的操作，使用约束求解器判定相应的规则，规则的违反意味着相应错误 的发生。断言违规也是符号执行可以检查的典型错误。 p r e f i x u 】是一个典型的基于符号执行的静态错误查找工具。它可以检查空指 针解引用、使用未初始化的内存、内存泄漏等错误。在跟踪执行路径的过程中， p r e f i x 对每个程序操作检查相应的一致性规则，不一致性意味着发现了错误。 p r e f i x 展示了使用符号执行技术做静态分析的一个优点，就是能够对每个错误给 出足够多的信息，包括错误发生的程序执行路径、执行相应路径需要满足的路径 条件等，这大大方便了程序员对错误的定位和分析。 a r c h e r 1 2 】是一个检查内存访问错误的过程间( i n t e r - p r o c e d u r a l ) 静态分析工 具，检查的错误包括数组越界、指针越界和通过指针和大小两个参数访问内存的 函数调用所引起的内存访问错误。它是这样检查数组引用a 【i 】的，首先依据符号状 态和约束求解器确定a 的大小和i 的边界。如果i 小于o 或者大于等于a 的大小， 则报告一个数组越界错误。其他的错误检查与此类似。由于a r c h e r 自底向上的 分析顺序( 首先分析被调用函数，再分析调用函数) ，对于包括形式参数的内存 访问无法进行错误检查。6 眦印珉通过引入“触发器 ( t r i g g e r ) 的概念来解决 这个问题。触发器表示错误发生条件。符号执行函数时生成并记录下它的触发器， 第8 页 国防科学技术大学研究生院硕士学位论文 在这个函数的调用处，读取它的触发器，用实际参数代替触发器中的形式参数， 然后通过判定触发器来确定是否有错误发生。 文献【1 3 】设计了个支持路径敏感的数据流分析的通用符号路径模拟引擎，用 到的主要技术是符号执行。通过使用定制的内存模型和模块化的系统结构，路径 模型引擎具有较好的可扩展性和灵活性，能够应用于多种静态分析。与常规的单 一路径模拟不同，路径模拟引擎支持数据流分析中的j o i n 操作，所以它能支持一 些高级分析方法，具有更好的通用性。路径模拟引擎的结构如图2 3 【i3 】所示。路径 模型引擎包括一个模拟接口和一个模拟状态管理器。模拟接口的作用是符号地执 行用户程序，根据执行结果建立并更新符号状态。模拟状态管理器的作用包括跟 踪符号状态，同时承担着约束求解器的功能。不同的用户程序可能需要不同的模 拟接口，而模拟状态管理器是通用的。通过为不同的用户程序定制相应的模拟接 口，可以重用模拟状态管理器。因此，这个结构设计使得路径模拟引擎可以灵活 的支持不同的用户程序做路径可行性分析。 图2 3 路径模拟引擎的结构 2 3 符号执行的研究现状 符号执行的研究进展表现在三个方面，即处理无界输入数据的惰性初始化系 列算法、抽象符号执行以及组合符号执行。 2 3 1 惰性初始化 j a v a 、c + + 等现代编程语言的个高级结构是可能包含无数个数据的复杂数据 结构( 以下称此为无界复杂数据) ，比如链表( 1 i s t ) 、树( t r e e ) 等。符号执行必 须面对以这些数据作为输入的函数所造成的困难。无界复杂数据往往包括引用类 第9 页 国防科学技术大学研究生院硕士学位论文 型的数据域，引用域链接不同的内存位置，往往使数据呈现为复杂的堆结构( h e a p s t r u c t u r e ) 。符号执行中，可以给一个简单类型( 标量数据) 变量一个符号，表示 此类型的任意一个值。但是，如果给一个引用类型变量一个“符号地址 ，则为 接下来的分析造成困难。原因是，引用变量的符号值使得被引用对象的状态符号 化，这大大增加了需要跟踪的符号状态。所以，当需要知道一个引用变量的值时， 需要分类确定它所指向的具体对象。描述无界复杂数据需要两个属性：它的结构 和针对简单数据域的约束。其中，无界复杂数据的结构表示它的引用数据域的指 向关系。所以，会出现这样的情况，一个很小的仅包含两个i f e l s e 分支语句的 代码段有七个不同的输入等价类【1 4 1 ，多出的三个是因为无界复杂数据的结构的不 同。 传统符号执行为有限个简单类型的输入变量赋予不同的符号，然后开始执行 程序。显然，这种思想无法处理无界复杂数据类型变量作为输入变量的情况。为 了能够符号执行输入变量是无界复杂数据类型的函数，文献 1 4 1 、【1 5 、 1 6 】提出 了一系列惰性初始化( 1 a z yi n i t i a l i z a t i o n ) 算法。惰性初始化的基本思想是，开始 符号执行时，无界复杂数据类型的符号对象的域是没有被初始化的。在符号执行 过程中，根据需要对这些未被初始化的域进行初始化，把引用类型数据域初始化 为“具体值 。并且，初始化进行的越迟，算法的性能越高。 文献【1 4 】提出的惰性初始化算法的基本思想是，以域未初始化的符号对象为输 入开始执行程序，在符号执行过程中，当这些域第一次被访问时初始化他们。具 体地，第一次访问简单数据域时，为其生成一个新的符号；第一次访问引用数据 域时，分三种情况初始化：把它初始化为n u l l ，或者初始化为一个域未初始化的 新的符号对象，或者初始化为每一个已经存在的类型适合( 类型相同或者是数据 域类型的子类型) 的对象。注意，每一个初始化产生一个不同的执行路径。可见， 惰性初始化算法也是一种处理别名问题的技术。 即使符号执行很小的一个程序，由于引用数据域的初始化，惰性初始化算法 也会产生一个很大的符号执行树，这严重影响了符号执行的性能。文献 1 5 1 改进了 惰性初始化算法，称为l a z i e ri n i t i a l i z a t i o n 算法，它具有更好的性能。明显，域初 始化越晚，符号执行树的节点数越少，性能越高。l a z i e ri n i t i a l i z a t i o n 算法延迟了 域初始化，分为两步：第一次访问一个引用域时，首先把它初始化为n u l l 和一 个符号引用。如果接下来有使用这个符号引用，包括访问它的域、相等性测试和 调用它的函数，再把这个符号引用替换为一个新的域未初始化的符号对象或者每 一个已经存在的类型适合的对象。这些已经存在的类型适合的对象可以作为初始 值的对象集合在初始化时计算。简单数据域的初始化与l a z yi n i t i a l i z a t i o n 算法相 同。 第l o 页 国防科学技术大学研究生院硕士学位论文 文献 1 6 改进l a z i e ri n i t i a l i z a t i o n 算法，称为l a z i e r # i n i t i a l i z a t i o n 算法，进一步 提高了惰性初始化算法的性能。l a z i e ri n i t i a l i z a t i o n 算法在第一次访问引用数据域 时就直接把它初始化为n u l l 或者一个符号引用，这种过早的分开初始化在一些 情况下是没有必要的。所以，l a z i e r # i n i t i a l i z a t i o n 算法的做法是：第一次读一个未 初始化的引用域时，把它初始化为一个符号值。当这样的符号值的域被访问时， 把它替换为n u l l 或者一个新的符号引用。对符号引用的进一步处理与l a z i e r i n i t i a l i z a t i o n 算法相同。 2 3 2 抽象符号执行 传统符号执行在数据的表示层面进行。即符号执行操作的数据单元是简单类 型数据和引用，对结构化类型数据和对象的访问根据在代码中相应的数据类型声 明被映射为对相应的域的访问，符号执行进入数据的代码层面的实现细节。在数 据表示层面进行符号执行是符号执行可扩展性的一个主要障碍【1 7 1 。考虑常见的库 类。为了性能等方面的考虑，库类的实现往往十分复杂。一些常用库类在程序中 大量出现，如果在数据表示层面符号执行这些库类，符号执行的工作量和复杂性 都大大增加。同时，在数据表示层面符号执行库类往往是没有必要的，库类往往 经过大量测试，错误很少。而且，检查的目标往往是客户代码。因此，在符号执 行中抽象这些库类，把它们作为数据单元直接处理，将有效提高符号执行的性能。 在抽象层面符号执行一些复杂数据类型称为抽象符号执行【l 7 】【l 引。符号执行需 要处理两个核心问题：定义操作的符号语义以及路径条件的表示和约束求解。抽 象符号执行也不例外，需要在抽象层面定义被抽象数据相关的路径条件的表示与 约束求解，以及作用在被抽象数据上的操作的符号语义。文献 1 7 1 提出了抽象符号 执行常用库类( 包括集合( s e t ) 和链表( 1 i s t ) ) 的方法。为集合和列表定义相应 的符号表示( 一个类) ，返回布尔值的a p i 对应一个相应的约束，更新对象状态 的方法对应于更新符号状态的一个方法。通过字节码插桩，把对集合和链表的引 用以及函数调用替换为相应的符号部分做符号执行。使用一种枚举过滤方法 ( e n u m e r a t e a n d f i l t e r ) 求解约束，基本思想是先枚举出所有可能的解，再使用路 径条件检查过滤，进而判定路径条件的可满足性。 文献 1 8 】说明了抽象符号执行库类j a v a 1 a n g s t r i n g 的方法，基本思想是使用有 限自动机( f i n i t e s t a t ea u t o m a t a ) 表示对串的约束，有限自动机接受所有满足约束的串 值。这样，有限自动机既记录了串约束，又是这个约束的求解器。约束公式的求 解以及给路径条件添加一个新的约束实现为对相应符号串的有穷自动机的精化。 对串上的谓词操作( j a v a 中的e q u a l s o 、s t a r t s w i t h o ) 的有穷自动机精化算法是特 定于谓词操作的。对串上的其他操作( j a v a 中的l e n g t h ( ) 、t r i m o 等) ，通过分类考 第1 1 页 国防科学技术大学研究生院硕士学位论文 虑输入的不同情况或者输入输出之间的关系定义符号语义。 2 3 3 组合符号执行 程序的路径可能是程序规模的指数，规模较大的程序包含数量巨大的路径， 这就是程序的路径爆炸问题。处在函数调用图顶端的函数会包