一种基于Actor模型的并行动态符号执行方法
|
摘要
动态符号执行用程序变量的具体值替换动态数据结构及复杂表达式中的符号变量以便简化路径条件,但是该方法面临路径爆炸问题.针对符号执行中路径探索和约束求解耗时问题,提出了一个并行化动态符号执行方法.该方法基于Actor并行模型,将动态符号执行中的路径探索与约束求解任务在多个节点并行执行,并基于子树转移方式实现节点任务的动态负载均衡,减少了节点间的通信代价.基于上述方法,研制了并行动态符号执行工具Jdart-parallel.与动态符号执行工具JDart的对比试验显示在使用多个工作节点时,相比于JDart,在时间效率上有了显著提升.
Dynamic symbolic execution replaces the symbolic variables in dynamic data structures and complex expressions with concrete values to simplify the path condition,but this method has a problem of path explosion. Aiming at the time consuming problem of path exploration and constraint solving in symbolic execution,a parallel dynamic symbolic execution method is proposed. Based on the Actor parallel model,this approach makes path exploration and constraint solving tasks in parallel execution in dynamic symbol execution run parallelly on multiple worker nodes,and enables the dynamic load balancing of node tasks based on the subtree shifting,which reduces the communication cost among nodes. Based on the above methods,we developed a parallel dynamic symbol execution tool Jdart-parallel. Compared with dynamic symbol execution tool JDart. Jdart-parallel improves the perfromace of symbolic execution significantly by using multiple worker nodes.
Dynamic symbolic execution replaces the symbolic variables in dynamic data structures and complex expressions with concrete values to simplify the path condition,but this method has a problem of path explosion. Aiming at the time consuming problem of path exploration and constraint solving in symbolic execution,a parallel dynamic symbolic execution method is proposed. Based on the Actor parallel model,this approach makes path exploration and constraint solving tasks in parallel execution in dynamic symbol execution run parallelly on multiple worker nodes,and enables the dynamic load balancing of node tasks based on the subtree shifting,which reduces the communication cost among nodes. Based on the above methods,we developed a parallel dynamic symbol execution tool Jdart-parallel. Compared with dynamic symbol execution tool JDart. Jdart-parallel improves the perfromace of symbolic execution significantly by using multiple worker nodes.
引文
[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-w orld softw are 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 Softw are Engineering Notes,2015,40(1):1-5.
[8]Kasper Luckow,Marko Dimjasevic,Dimitra Giannako poulou,et al.JDart:a dynamic symbolic analysis framew ork[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 Softw are 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.Par Sym: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 Softw are 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-w orld softw are 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 Softw are Engineering Notes,2015,40(1):1-5.
[19]Cassar I,Francalanza A.On implementing a monitor oriented programming framew ork 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.
[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-w orld softw are 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 Softw are Engineering Notes,2015,40(1):1-5.
[8]Kasper Luckow,Marko Dimjasevic,Dimitra Giannako poulou,et al.JDart:a dynamic symbolic analysis framew ork[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 Softw are 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.Par Sym: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 Softw are 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-w orld softw are 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 Softw are Engineering Notes,2015,40(1):1-5.
[19]Cassar I,Francalanza A.On implementing a monitor oriented programming framew ork 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.