一种基于Actor模型的并行动态符号执行方法

张晓文,贾向阳,常 亮,刘钱超,胡小辉

1(桂林电子科技大学 广西可信软件重点实验室,广西 桂林 541004) 2(武汉大学 软件工程国家重点实验室,武汉 430000)

1 引 言

符号执行技术是一种经典的程序分析技术.它使用符号值来代替具体的值来模拟执行程序,系统化地探索程序的可行的路径,从而来发现难以发现的缺陷,以及为各个路径生成测试用例[1-3].动态符号执行技术(如Concolic Testing[9-13]和Dart[5,8])在符号执行中引入了具体值,利用具体值执行程序,记录程序中的符号值和各个分支的路径条件(Path Condition).在一条路径执行完成后,通过对其它分支的路径条件进行约束求解,来生成针对新路径的程序输入,引导下一次执行.

动态符号执行相对静态符号执行具有更高的效率,因此在目前得到了更广泛的应用.然而,由于动态符号执行同样需要探索大量的路径,并进行耗时的约束求解,因此对于稍大规模的程序,效率往往难如人意[4].

将符号执行中耗时的工作并行化是提高效率的有效手段.目前国内外也有一些此类的探索工作[6,7].然而,符号执行的并行优化仍然面临着一些挑战性的问题:

1)任务的动态迭代式产生问题:在动态符号执行中,路径探索和约束求解这些耗时的工作是动态迭代式产生的:每求解路径条件并探索完一条路径后,都会产生一组新路径需要进行约束求解和路径探索.这种动态迭代式的任务,很难通过静态任务分配方式来实现并行化.

2)大规模任务的通信代价问题:动态符号执行中路径探索和约束求解的任务数据巨大,单个任务则一般执行时间并不长.这种大规模的小任务对任务调度的通信代价具有很高的敏感性.

本文针对上述问题,提出了一种基于Actor并行模型的动态符号执行并行优化方法.该方法将符号执行中的任务按照符号执行树的子树方式分配到多个独立运行的Actor工作节点中.各个Actor工作节点负责对该子树的路径条件进行求解,对可行路径进行探索.每条路径探索完然后发现新路径时,将新增加的路径数目通知调度中心.调度中心监控各个节点的路径数目,如果某个节点处于空闲状态时,则从最多路径的节点“拆借”一个子树分配给该节点,从而实现了任务的动态负载均衡.工作节点向调度中心发送路径数时采用异步方式,并且数据量很小,通信代价基本可以忽略.由于各个工作节点只探索相对独立的路径子树,基本兼容了之前的符号执行工作模式,因此已有的优化机制仍然可以很方便地整合使用.

2 基于Actor模型的并行符号执行方法

2.1 Actor模型

Actor模型是一种经典的并行计算模型,在Actor模型中,Actor是一种可以响应外部消息的计算实体[19].异步消息是Actor之间唯一的通信方式.Actor模型中各个Actor可以并行执行计算任务,但各个Actor又相互独立运行,没有锁机制等依赖关系.

Actor模型等这些特点非常符合并行符号执行的特定需求.各个并行计算节点做为Actor可以不依赖其他节点、相对独立地执行局部任务.而异步消息保证了通信不会影响本节点的计算工作.

2.2 方法概述

总体框架设计如图1所示,由Master和多个Worker组成.方法使用了两种类型的Actor:MasterActor和WorkerActor.主要功能是:

1)MasterActor:负责负载均衡和任务分配.该部分维护一个负载表,记录每个Worker发送来的负载消息.任务中心会根据负载表判断是否需要启动负载均衡工作(负载值超过负载表中任务的负载最大值),若需要则会给负载大的Worker节点发送任务转移消息,收到相应消息后会将任务发送给给空闲的工作节点,以此实现多个节点的任务均衡分配.

2)WorkerActor:负责对程序某个特定的路径子树进行符号执行.节点维护一个维护待求解路径栈和一个待探索路径栈.该部分实现了worker内部约束求解和路径探索的并行工作:worker节点响应MasterActor提供的任务,放入待求解路径栈中,约束求解器从栈中读取任务,进行求解,求解后的路径放入待探索路径栈中.路径探索模块从待探索路径栈中读取路径进行探索,探索完成后,又会产生新的一组路径,放入待求解路径栈中.依次迭代直到所有的路径都探索完成,或者找到满足目标的路径.

工作节点在每次路径探索结束后,会将当前的两个栈中的任务数作为结点的负载发给MasterActor.而MasterActor如果需要负载均衡的时候,忙节点的WorkerActor会将当前未探索的子树转移到空闲节点上,来实现负载均衡.

2.3 基于子树转移的动态负载均衡方法

由于在动态符号执行中,待探索的路径是动态迭代式产生的,因此很难准确评估各个节点的负载,从而实现精确的负载均衡.本文中采取了动态负载均衡方法,只有存在空闲节点时,才从繁忙的节点处拆借任务到空闲节点上.这样保证各个节点都处于工作状态,达到一定程度上的负载均衡.

在本文中,节点的负载表示为待求解路径栈和待探索路径栈中的总路径数目.每一条路径探索完成后,可能会产生新路径,放入待求解路径栈中,从而使节点的负载发生变化.这时,工作节点会将新的负载发送到Master节点.当子树的最后一条路径探索完成,没有新路径产生时,节点的负载变为0.

当负载为0的节点出现后,Master节点会启动负载均衡,查找负载最大的节点,进行路径转移.为了避免分析后期阶段少量任务的多次转移.我们为节点设置了一个最少负载,只有超过这个最少负载的节点才会拆借出子树给空闲节点.

在工作节点中,取待求解路径栈和待探索路径栈中的路径实际上代表了一个未展开的子树.在进行子树转移时,实际上就是取路径栈中的某个路径转移给其他节点.然而,具体选择哪个子树进行转移,需要根据分析的目标和算法,设定不同的策略来确定.例如,为了避免转移了过小子树造成过于频繁的负载均衡,我们可以取待求解路径栈中长度最短的路径进行转移.在深度优先搜索中,长度最短路径就是栈底的路径.或者,为了在启发式搜索中更快地找到目标,我们可以将接近栈顶的路径进行转移,因为这些路径找到目标的可能性较大.

图2 子树转移Fig.2 Subtree shifting

如图2所示,当左边节点需要转移任务到右边节点时.由于路径树中A是根节点,A的左子树正在探索,而右子树(节点B是根节点)是未探索的子树.该节点代表的路径目前存放在待求解路径栈中.于是B开始的子树将被转移到右边的空闲节点上,进行约束求解和生成待探索路径.转移后,左节点将不再探索B节点代表的子树.

空闲节点会出现在两个时间点:

1)并行符号执行刚最开始启动时,路径树的根节点被分配给一个工作节点进行分析,其他节点处于空闲状态.

2)某个节点分析的子树的所有路径都探索完成时,当前节点的负载为0,称为空闲节点.

2.4 路径探索与约束求解的并行

原始符号执行是路径探索和约束求解分别执行,当程序执行时将所有的待求解的路径探索出来,然后使用约束求解器将探索路径进行求解,但是这样的模式对于大规模程序而言,耗时较长,严重浪费系统资源.针对上述问题,提出路径探索和约束求解并行执行,这样可以节省程序执行时间.

图3 并行路径探索与约束求解Fig.3 Parallel path exploration and constraint solving

如图3所示，包含两个栈:待求解路径栈和待探索路径栈;节点A为路径的根节点;节点B为未展开节点;P1、P2等是待求解路径栈;P7、P8等是待探索路径栈;并行路径探索和约束求解是通过该栈相互操作,实现任务的并行操作.当执行路径操作时,首先将待求解的路径存入待求解路径栈,空闲节点从该栈中取相应任务,然后通过约束求解器Z3将待求解路径进行求解操作,同时生成待探索路径,存入待探索路径栈,进行路径探索,探索完成后,产生的新路径又会存放到待求解任务栈中,这样递归完成对所有路径的探索和求解.待探索任务栈中会不停的存和取任务,而待探索任务栈会根据求解结果存放路径,这样,可以并行完成任务操作.

3 实验与评估

我们基于动态符号执行工具Jdart和Jdart Actor框架,实现了一个并行动态符号执行原型工具Jdart-parallel.我们将Jdart-parallel较原来Jdart符号执行效率进行对比,来评估本文方法的有效性.同时,对Jdart-parallel符号执行工具在不同节点数下的执行效率进行了评估,分析并行的规模对效率的作用效果.

3.1 实验环境

本实验主要是使用6个计算机节点操作,每一个节点的配置如下:Dell台式电脑、Intel Core i7-4790、CPU:3.6GHz、8GB RAM 、Windows 操作系统、Sun JRE 1.8 (64-bit mode)、Eclipse(64-bit mode)、Ant 1.9.

实验中待测试的程序包括:

1)Euclid:计算两个整数之间的差值;

2)WBS:使用整数和布尔类型输入来进行更新操作;

3)ArraysCh6、ArraysCh7、ArraysCh8、ArraysCh9、ArraysCh10、ArraysCh11:对数组进行的基本操作,其中程序名称后面的6、7、8、9、10、11代表执行程序的参数的个数;

4)Double2Long:将双精度类型数据转换成长整形;CEV4、CEV5、CEV6、CEV7、CEV8、CEV9、CEV10:计算方差,其中程序名称后面的4、5、6、7、8、9、10代表程序的执行个数.

3.2 实验结果分析

实验1.与JDart的对比分析

如表1,总的路径数目对于不同数目节点是相同的,单节点的 JDart(动态符号执行)其执行时间相比于其它节点明显长许多.如ArrayCh9,JDart的执行时间是1266323ms,而并行框架不同节点的运行时间相比其是大幅度减少:2节点运行时间20607ms,3节点运行时间为10734ms,如此,随着节点数目的增加,程序执行时间在逐渐的缩短.相比JDart,2节点的执行时间相比单节点节省了将近62倍,节点规模的不断扩大,该数字也在不断增长.

表1 与单节点符号执行(Jdart)的运行时间对比
Table 1 Comparison run time with single node

程序名称路径数不同数目节点运行时间/ms单节点Jdart2节点3节点4节点5节点6节点Euclid5015338010481048104810481048WBS13824615350414238397129892799ArraysCh615625906763786061582350424969ArraysCh77812553998100326702597347024523ArraysCh8390625245512150609928822567274515ArraysCh9195312512663232060710734944477086500ArraysCh10#∗25963138271030698458625ArraysCh11#∗321191622011551102169009CEV465611094385476305504537032400CEV559049140876104768905603149123809CEV653144114065821563210248809565204325CEV7#∗20449132211008587476645CEV8#∗24082160471292397457566CEV9#∗30566241941319498588656CEV10#∗355792016911481108719658Double2Long400303310081008100810081008∗：代表运行时间长于1h，#：代表路径条数大于200万条

从表1可以看出,JDart的执行效率相比于Jdart-parallel有明显的差距,Jdart-parallel的执行效率明显优于JDart.随着节点数目的增加,Jdart-parallel的执行效率在不断的提高,从本质上证明了Jdart-parallel并行符号执行的优势.

实验2.节点规模对符号执行的性能影响

从实验中可以看出,随着节点数目的不断增加,程序的执行效率在明显提升,并且随着节点数目的逐渐增多,程序的执行效率越高,能更好的体现出并行符号执行的优势.此外,随着节点数目的增加,程序的执行时间在逐渐的缩短,从执行时间上可以对比分析出并行符号执行的优势,具体影响如下图标所示:

本实验主要对照的是节点数目对实验的影响,拟使用6个实验节点来检测,检测每个节点具体运行对实验结果的影响,然后对比最初始的程序运行时间,对比判断出随着节点数目的增多,实验结果的最终变化,以此来预测节点规模对实验的影响.

图4 不同节点规模下的符号执行运行时间Fig.4 Symbolic Execution Runtime at Different Node Scales

图4描述了在Jdart-parallel执行工具下,对于待测程序,在不同工作节点下的执行时间,其中对每一个待测程序而言,从左到右节点数目在逐渐的增加.从图中可以看出,对于每一个待测程序,随着节点数目的增加,执行时间在逐渐的缩短,对于程序Double2Long和Euclid,由于程序结构比较简单、规模较小,所以在执行的过程中只用到了其中某一个节点,因此执行时间基本上是相同的.

图4横轴表示待测程序的名称,纵轴表示待测程序的执行时间,柱状图的高度表示程序的具体执行时间,不同的颜色代表不同的节点数目执行待测程序的时间,图中可以看出:随着节点数目的增加,执行相同待测程序的时间在减少.

图5和图6描述了待测程序CEV、Arrays和其变化程序在不同节点下的运行时间.从图中可以看出,随着节点数目的不断增加,每个待测程序的执行时间在逐渐的减少,说明了并行符号执行的执行效率随着节点数目的增加在提升,同时执行程序的规模随着节点数目的增加在增大.

图7描述了在并行框架下,部分程序的加速比(加速比=单节点/n节点,其中n:2,3,4,5,6),随着节点数目的逐渐增加,加速比在逐渐的提升,程序的运行效率在逐渐提升,其中程序Euclid和Double2Long由于程序规模较小,只使用一个节点,所以加速比没变化.

实验分析:

执行时间:随着程序规模逐渐增加,Jdart(单节点)的执行时间在逐渐增加,但是Jdart-parallel的执行时间相比Jdart执行时间明显减少.Jdart执行时间比并行时间多,如表1中单节点和2 节点最为明显,原因是Jdart的执行没使用到多核技术,执行的过程中随着内存的逐渐消耗程序会出现卡顿等现象,卡顿期间的时间消耗比较高.并行执行时每个节点都使用较小的路径树,占用资源较少,减轻了卡顿现象.

图5 CVE在不同节点下运行时间Fig.5 CVE run time at different nodes

图6 Arrays在不同节点下运行时间Fig.6 Arrays run time at different nodes

图7 加速比Fig.7 Speedup ratio

执行大规模程序能力:随着程序规模的逐渐增加,Jdart-parallel随着节点数目的增加,程序的执行效率在不断的增强,体现了Jdart-parallel执行大规模程序的能力.

从上述的实验结果可以看出,Jdart-parallel并行符号执行在执行程序方面的优势:首先并行符号执行在执行程序的过程中相比于非并行执行时间明显缩短;其次是随着节点数目的不断增多,执行相同的程序,并行方式明显比非并行执行能力强;随着程序规模的逐渐增加,并行符号执行执行时间比非并行节省许多,说明了并行符号执行可以执行较大规模程序的能力.

与动态符号执行相比,并行动态符号执行使用多个节点,在多节点上分别执行路径探索任务.由以上实验结果可以看出,并行动态符号执行工具相比于原来的动态符号执行工具而言测试相同的程序能有效地缩短执行时间,并行符号执行使用多个节点测试相应程序比原始动态符号执行测试相同的程序提高时间效率,同时加速比在逐渐增加(加速比=单节点/n节点,其中n:2,3,4,5,6),实验结果证明并行动态符号执行工具Jdart-parallel在提高符号执行效率方面具有良好的效果.

4 相关工作

为了解决并行符号执中面临的效率问题,学术界提出了一些基于并行技术的优化方法.

ParSym[14]是一种并行动态符号执行,通过一个Symbolic Execution Monitor对整个符号执行进行控制和任务分配,符号执行中的每条路径被当作一个独立的任务.在符号执行中产生的新任务被动态地分配到各个节点进行执行.ParSym采用了集中式的任务调度方法,涉及到较多的任务分配和回收等操作,当路径比较庞大时会耗费较多的通信代价.

静态分区技术[15]使用一系列的前置条件来对符号执行树进行分区,这样做的目的是允许我们可以高效的分布执行符号执行,减少搜索的时间,它们在执行的过程中每一个并行实例执行各自的运行框架,相互之间很少有交互,节省时间,但是使用这些先决条件可能使得不同的节点搜索相同的路径,搜索的重复率较高,浪费时间,同时静态分区不能实现节点之间的负载均衡.

Cloud9[16,17]是第一个使用大规模集群的符号执行系统可以线性的扩展许多的节点,是一个请求式的测试软件,它主要的功能结构包括工作节点和负载均衡器,主要依赖均衡器来分配相应的搜索任务,并把搜索进行并行化操作,它可以自动化的测试现实世界中的软件,节省了很多时间.Cloud9提供了一个系统的写符号测试的接口,只需要输入测试数据和测试行为,可以提升测试的效率.Cloud9有许多自身的优势:不仅可以处理单线程的程序,还可以处理多线程的程序和分布式系统,在多路径、多任务同时进行时,Cloud9通过均衡器来实现对于负载的均衡.但是Cloud9在执行的过程中需要维护整棵符号执行树,路径搜索消耗大量多余时间.而本文需要维护的只是个子树,节省了存储空间和搜索时间.此外,Cloud9是针对经典的符号执行工具而非动态符号执行,在任务的产生和分配机制上与本文是不同的.

Quoc-Sang Phan等人提出了一种Concurrent Bounded Model Checking(CBMC)方法[18].该方法基于经典的符号执行工具Symbolic PathFinder进行并行的模型检测.它首先通过路径探索,搜索到特定路径的所有可行路径,然后将这些路径进行合并成一个大的约束进行求解.求解时采用并行技术,将各条路径的约束分配到多个节点进行求解.该方法只针对的是模型检测的应用场景,只对约束求解过程进行并行,与本文的动态符号执行在应用场景和并行模式上是不同的.

5 总 结

本文基于Actor并行模型,提出了一种并行动态符号执行方法,它实现了两个层面上的并行.首先可以在多个节点上并行分析程序的路径子树,并通过子树转移实现动态的负载均衡.另一方面在节点内部,将约束求解和路径探索两项耗时的工作并行,来进一步提高效率.

通过原型工具Jdart-parallel做的相关对比试验结果表明,相比于原来的动态符号执行工具,测试相同的程序,能在时间效率上得到很大提升,证明了并行化符号执行在提高效率方面的有效性,同时也体现出并行符号执行工具Jdart-parallel在提高符号执行效率方面的优势,在处理较大规模程序中效果也比较明显.

未来的工作主要考虑能否在约束求解任务分配支持启发式地搜索分配方式,能更加准确快速地搜索到与上一条相似度最高的那条路径分配,充分利用上一条已保存的求解结果,可以进一步地提高效率,此外还希望该模型可以支持规模更大的程序,结合已有的各种优化机制,期望能够在实际的项目得到应用.

[1] Bezier B.Software testing techniques,2nd edition[M].Van Nostrand Reinhold,New York,1990.

[2] King J C.Symbolic execution and program testing[J].Communications ACM,1976,19(7):385-394.

[3] Li Zhou-jun,Zhang Jun-xian,Liao Xiang-ke.Survey of software vulnerabllity detection techniques[J].Journal of Computer,2015,38(4):717-732.

[4] King J C.Symbolic execution and program testing[J].Communications of the Acm,1976,19(7):385-394.

[5] Sen K.DART:directed automated random testing[J].Acm Sigplan Notices,2005,40(6):213-223.

[6] Bucur S,Ureche V,Zamfir C,et al.Parallel symbolic execution for automated real-world software testing[C].Conference on Computer Systems,ACM,2011:183-198.

[7] Phan Q S,Malacaria P,Reanu C S.Concurrent bounded model checking[J].Acm Sigsoft Software Engineering Notes,2015,40(1):1-5.

[8] Kasper Luckow,Marko Dimjasevic,Dimitra Giannako poulou,et al.JDart:a dynamic symbolic analysis framework[C].International Confercence on Tools and Algorithms for the Construction and Analysis of Systems,Springer Berlin Heidelberg,2016:442-459.

[9] Dong Qi-xing,Zeng Fan-ping,Yan Jun.Improve the solving of non-linear arithmetic constraints in dynamic symbolic execution[J].Journal of Chinese Computer System,2014,35(11):2396-2401.

[10] Cadar C,Dunbar D,Engler D.KLEE:unassisted and automatic generation of high-coverage tests for complex systems programs[C].Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation,USE-NIX Association,2008:209-224.

[11] Gupta A.Feedback-directed unit test generation for C /C ++ using concolic execution[C].International Conference on Software Engineering,IEEE,2013:132-141.

[12] Godefroid P,Levin M Y,Molnar D.SAGE:whitebox fuzzing for security testing[J].Queue,2012,10(1):40-44.

[13] An Jing.A research on key technologies of dynamic symbolic[D].Beijing:Beijing University of Posts and Telecommunications,2014.

[14] Siddiqui J H,Khurshid S.ParSym:parallel symbolic execution[C].International Conference on Software Technology and Engineering,2010:V1-405-V1-409.

[15] Staats M,Pǎsǎreanu C.Parallel symbolic execution for structural test generation[C].Nineteenth International Symposium on Software Testing and Analysis,ISSTA 2010,Trento,Italy,2010:183-194.

[16] Ciortea L,Zamfir C,Bucur S,et al.Cloud9:a software testing service.[J].Acm Sigops Operating Systems Review,2009,43(4):5-10.

[17] Bucur S,Ureche V,Zamfir C,et al.Parallel symbolic execution for automated real-world software testing [C].Conference on Computer Systems,ACM,2011:183-198.

[18] Phan Q S,Malacaria P,Reanu C S.Concurrent bounded model checking[J].Acm Sigsoft Software Engineering Notes,2015,40(1):1-5.

[19] Cassar I,Francalanza A.On implementing a monitor oriented programming framework for actor systems[J].Lecture Notes in Computer Science,2016.

附中文参考文献：

[3] 李舟军,张俊贤,廖湘科,等.软件安全漏洞检测技术[J].计算机学报,2015,38(4):717-732.

[10] 董齐兴,曾凡平,严 俊,等.改进动态符号执行中的非线性约束求解过程[J].小型微型计算机系统,2014,35(11):2396-2401.

[12] 安 靖.动态符号执行关键技术研究[D].北京:北京邮电大学,2014.