摘要
动态符号执行用程序变量的具体值替换动态数据结构及复杂表达式中的符号变量以便简化路径条件,但是该方法面临路径爆炸问题.针对符号执行中路径探索和约束求解耗时问题,提出了一个并行化动态符号执行方法.该方法基于Actor并行模型,将动态符号执行中的路径探索与约束求解任务在多个节点并行执行,并基于子树转移方式实现节点任务的动态负载均衡,减少了节点间的通信代价.基于上述方法,研制了并行动态符号执行工具Jdart-parallel.与动态符号执行工具JDart的对比试验显示在使用多个工作节点时,相比于JDart,在时间效率上有了显著提升.
Dynamic symbolic execution replaces the symbolic variables in dynamic data structures and complex expressions with con-crete values to simplify the path condition, but this method has a problem of path explosion. Aiming at the time consuming problem ofpath exploration and constraint solving in symbolic execution ,a parallel dynamic symbolic execution method is proposed. Based on theActor parallel model, this approach makes path exploration and constraint solving tasks in parallel execution in dynamic symbol execu-tion run parallelly on multiple worker nodes, and enables the dynamic load balancing of node tasks based on the subtree shifting, whichreduces the communication cost among nodes. Based on the above methods, we developed a parallel dynamic symbol execution toolJdart-parallel. Compared with dynamic symbol execution tool JDart. Jdart-parallel improves the perfromace of symbolic execution sig-nificantly by using multiple worker nodes.
出处
《小型微型计算机系统》
CSCD
北大核心
2018年第1期12-16,共5页
Journal of Chinese Computer Systems
基金
国家自然科学基金面上项目(61373038
61272108
61363030)资助
广西可信软件重点实验室开放课题(kx201534)资助
关键词
符号执行
Actor模型
并行
负载均衡
symbolic execution
actor model
parallelization
load balancing
