基于多线程并行的符号执行引擎设计与实现  

Design and Implementation of a Parallel Symbolic Execution Engine Based on Multi-Threading

作　　者：周彭 左志强 Zhou Peng;Zuo Zhiqiang(Department of Computer Science and Technology,Nanjing University,Nanjing 210023;National Key Laboratory for Novel Software Technology(Nanjing University),Nanjing 210023)

机构地区：[1]南京大学计算机科学与技术系,南京210023 [2]计算机软件新技术国家重点实验室(南京大学),南京210023

出　　处：《计算机研究与发展》2023年第2期248-261,共14页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(62272217)。

摘　　要：符号执行作为一种高效的测试生成技术,被广泛应用于软件测试、安全分析等领域.然而,由于程序中的执行路径数量随着分支数量的增加而指数级上升,符号执行往往无法在大规模程序上进行高效执行,缺乏可扩展性.已有的基于多进程的并行化方法具有较大的额外通信开销,并且缺乏对现有约束求解优化技术的利用.提出了基于多线程并行处理模型的符号执行加速方法.具体来讲,为解决并行符号执行中的不同工作节点负载不平衡问题,设计了不需要中间节点参与的工作窃取算法.为充分利用现有约束求解优化技术,提出了让不同工作节点共享约束求解信息的加速求解方法.基于符号执行引擎(KLEE)实现了多线程并行化符号执行方案,从而形成多线程并行化符号执行引擎(PKLEE).实验验证表明,在穷尽执行路径场景下,KLEE平均耗时是在给定8个线程下PKLEE的3~4倍;在同样的时间内,PKLEE执行的有效工作负载平均是KLEE的3倍.Symbolic execution,as an effective test generation technique,has been increasingly used for software testing and vulnerability discovery,etc.However,the number of execution paths in a program rises exponentially with the number of branches,and symbolic execution can hardly be performed efficiently on large-scale programs,leading to poor scalability.Considering that multi-processed parallel symbolic execution approaches not only suffer from high communication overhead,but also fail to use the existing constraint solving optimization techniqnes.To tackle the above problems,we devise a novel work-stealing algorithm that requires no centralized nodes.In addition,to exploit the existing constraint solving optimizations,we enable different worker nodes to share the constraint solving information so as to accelerate the solving process.Based on the above mechanisms,we implement our parallel engine PKLEE(parallel KLEE)on the top of KLEE and conduct the experimental evaluations on it.In the exhaustive execution path scenario,the average time consumed by KLEE is three to four times longer than that of PKLEE with 8 threads available,and the effective workload executed by PKLEE is on average three times higher than that of KLEE in the same period of time.

关 键 词：符号执行 负载均衡 约束求解 并行加速 可扩展性 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]