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

摘要 动态符号执行用程序变量的具体值替换动态数据结构及复杂表达式中的符号变量以便简化路径条件,但是该方法面临路径爆炸问题.针对符号执行中路径探索和约束求解耗时问题,提出了一个并行化动态符号执行方法.该方法基于Actor并行模型,将动态符号执行中的路径探索与约束求解任务在多个节点并行执行,并基于子树转移方式实现节点任务的动态负载均衡,减少了节点间的通信代价.基于上述方法,研制了并行动态符号执行工具Jdart-parallel.与动态符号执行工具JDart的对比试验显示在使用多个工作节点时,相比于JDart,在时间效率上有了显著提升