计算机科学 ›› 2018, Vol. 45 ›› Issue (6A): 28-35.

• 综述研究 • 上一篇    下一篇

符号执行研究综述

叶志斌,严波   

  1. 江南计算技术研究所 江苏 无锡214083
  • 出版日期:2018-06-20 发布日期:2018-08-03
  • 作者简介:叶志斌(1992-),男,硕士生,主要研究方向为信息安全,E-mail:SOSCapture@163.com(通信作者);严 波(1978-),男,硕士,高级工程师,主要研究方向为信息安全。
  • 基金资助:
    国家自然科学基金项目(91430214)资助

Survey of Symbolic Execution

YE Zhi-bin,YAN Bo   

  1. Jiangnan Institute of Computing Technology,Wuxi,Jiangsu 214083,China
  • Online:2018-06-20 Published:2018-08-03

摘要: 符号执行作为一种重要的程序分析方法,可以为程序测试提供高覆盖率的测试用例,以触发深层的程序错误。首先,介绍了经典符号执行方法的原理;然后,阐述了基于符号执行发展形成的混合测试、执行生成测试和选择性符号执行方法,同时,对制约符号执行方法在程序分析中的主要因素进行了分析,并讨论了缓解这些问题和提高符号执行可行性的主要方法;随后,介绍了当前主流的符号执行分析工具,并比较分析了其优缺点;最后,总结并讨论了符号执行的未来发展方向。

关键词: 符号执行, 混合测试, 执行生成测试, 路径爆炸, 约束求解

Abstract: As an important program analysis method,symbolic execution can generate high coverage tests to trigger deeper vulnerabilities.This paper firstly introduced the principle of classical symbolic execution,and elaborated three dynamic symbolic execution methods which are known as concolic testing,execution generated test and selective symbolic execution.Meanwhile,the essence of main challenges of symbolic execution and the current major solutions were discussed.Symbolic execution has been incubated in dozens of tools which were described and compared in this paper.Finally,the develop directions of symbolic execution were forecasted.

Key words: Symbolic execution, Concolic testing, Execution generated test, Path explosion, Constraint solving

中图分类号: 

  • TP311
[1]BOYER R S,ELSPAS B,LEVITT K N.Select—a formal sys- tem for testing and debugging programs by symbolic execution[C]∥International Conference on Reliable Software.New York,USA,ACM,1975:234-245.
[2]KING J C.Symbolic execution and program testing[J].Communications of the Acm,1976,19(7):385-394.
[3]MYERS G J.Art of Software Testing.New York:John Wiley & Sons,Inc.,1979.
[4]CADAR.Symbolic Execution for Software Testing in Practice-a Preliminary Assessment[C]∥International Conference on Software Engineering.IEEE,2011:1066-1071.
[5]SEN K.Concolic testing[C]∥Ieee/acm International Conferen- ce on Automated Software Engineering.ACM,2007:571-572.
[6]MESNARD F, TIENNE P,GERMN V.Concolic testing in logic programming[J].Theory & Practice of Logic Programming,2015,15(4/5):711-725.
[7]PALACIOS A,VIDAL G.Concolic Execution in Functional Programming by Program Instrumentation[C]∥International Symposium on Logic-Based Program Synthesis and Transformation.Springer International Publishing,2015:277-292.
[8]SEN K.Concolic testing:a decade later (keynote)[C]∥International Workshop on Dynamic Analysis.ACM,2015:1-1.
[9]CADAR C,GANESH V,PAWLOWSKI P M,et al.EXE:automatically generating inputs of death[C]∥Proceedings of the 13th ACM Conference on Computer and Communications Security.ACM,2006:322-335.
[10]CADAR C,ENGLER D.Execution Generated Test Cases:How to Make Systems Code Crash Itself[M]∥Model Checking Software.DBLP,2005:902-902.
[11]CADAR C,SEN K.Symbolic execution for software testing: three decades later.http://www.cs.umd.edu/class/fall2017/cmsc818O/papers/symbolic-execution.pdf.
[12] CHIPOUNOV V,GEORGESCU V,ZAMFIR C,et al.Selective Symbolic Execution[C]∥The Workshop on Hot Topics in System Dependability.2009:1286-1299.
[13]MAJUMDAR R,SEN K.Hybrid Concolic Testing[C]∥International Conference on Software Engineering.IEEE,2007:416-426.
[14]WEN S,FENG C,MENG Q,et al.Testing Network Protocol Binary Software with Selective Symbolic Execution[C]∥International Conference on Computational Intelligence and Security.IEEE,2017:318-322.
[15]MORAN K,LINARES-VSQUEZ,BERNAL-CRDENAS, et al. Denys Poshyvanyk[C]∥2016 IEEE International Conference on Automatically Discovering Reporting and Reproducing Android Application Crashes,Software Testing Verification and Validation (ICST).2016:33-44.
[16]STEPHENS N,GROSEN J,SALLS C,et al.Driller:Augmen- ting fuzzing through selective symbolic execution[C]∥23nd Annual Network and Distributed System Security Symposium(NDSS 2016).2016.
[17]CADAR C,DUNBAR D,ENGLER D R.KLEE:Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs[C]∥Usenix Conference on Operating Systems Design and Implementation.USENIX Association,2008:209-224.
[18]BURNIM J,SEN K.Heuristics for Scalable Dynamic Test Gene- ration[C]∥IEEE/ACM International Conference on Automated Software Engineering.2008:443-446.
[19]SEN K,AGHA G.CUTE and jCUTE:Concolic Unit Testing and Explicit Path Model-Checking Tools∥International Conference on Computer Aided Verification.2006:419-423.
[20]BOONSTOPPEL P,CADAR C,ENGLER D.RWset:Attacking Path Explosion in Constraint-Based Test Generation[C]∥Theory and Practice of Software,International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems.Springer-Verlag,2008:351-366.
[21]GODEFROID P.Compositional dynamic test generation[C]∥Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL 2007).New York,USA,ACM,2007:47-54.
[22]HANSEN T,SCHACHTE P,S NDERGAARD H.Runtime verification.chapter State Joining and Splitting for the Symbolic Execution of Binaries[M]∥Berlin:Springer-Verlag,2009:76-92.
[23]KUZNETSOV V,KINDER J,BUCUR S,et al.Efficient state merging in symbolic execution.In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI 2012).New York,USA,ACM,2012:193-204.
[24]AVGERINOS T,REBERT A,SANG K C,et al.Enhancing symbolic execution with veritesting∥International Conferen-ce on Software Engineering.ACM,2014:1083-1094.
[25]MARINESCU P D,CADAR C.make test-zesti:a symbolic execution solution for improving regression testing[C]∥International Conference on Software Engineering.IEEE,2012:716-726.
[26]ENGLER D,DUNBAR D.Under-constrained execution:making automatic code destruction easy and scalable[C]∥International Symposium of Software Testing and Analysis.ACM,2007:1-4.
[27]RAMOS D A,ENGLER D.Under-constrained symbolic execution:correctness checking for real code[C]∥Usenix Conference on Security Symposium.USENIX Association,2015:49-64.
[28]MOURA L D,BJ RNER N.Z3:An Efficient SMT Solver∥ Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2008:337-340.
[29]SANG K C,AVGERINOS T,REBERT A,et al.Unleashing Mayhem on Binary Code[C]∥Security and Privacy.IEEE,2012:380-394.
[30]BARRETT C,BEREZIN S.CVC Lite:A New Implementation of the Cooperating Validity Checker[C]∥Computer Aided Verification,International Conference(CAV 2004).Boston,MA,USA,DBLP,2004:515-518.
[31]BARRETT C,TINELLI C.19th International Conference on Computer Aided Verification (CAV’07)[M]∥Damm W,Hermanns H,eds.Berlin:Springer,2007:298-302.
[32]ENDERTON H B,COMPUTABILITY M D,UNSOLVABILITY.Hilbert’s Tenth Problem is Unsolvable∥American Mathematical Monthly.1973:233-269.
[33]XIAO X,XIE T,TILLMANN N,et al.Precise identification of problems for structural test generation[C]∥ICSE 2011.ACM,2011:611-620.
[34]RAMOS D A,ENGLER D.Under-constrained symbolic execution:correctness checking for real code[C]∥Usenix Conference on Security Symposium.USENIX Association,2015:49-64.
[35]SEN K,AGHA G.CUTE and jCUTE:Concolic Unit Testing and Explicit Path Model-Checking Tools[C]∥International Conference on Computer Aided Verification.Springer-Verlag,2006:419-423.
[36]CHAUDHURI A,FOSTER J S.Symbolic security analysis of ruby-on-rails web applications[C]∥ACM Conference on Computer and Communications Security.ACM,2010:585-594.
[37]TILLMANN N,DE HALLEUX J.Pex:white box test generation for .NET∥Tests & Proofs,Second International Conference.Tap,Prato,Italy,2008:134-153.
[38]P S REANU C S,RUNGTA N.Symbolic PathFinder:sym- bolic execution of Java bytecode[C]∥IEEE/ACM International Conference on Automated Software Engineering(ASE 2010).Antwerp,Belgium,DBLP,2010:179-180.
[39]SHOSHITAISHVILI Y,WANG R,SALLS C,et al.SOK: (State of) The Art of War:Offensive Techniques in Binary Analysis[C]∥2016 IEEE Symposium on Security and Privacy (SP).IEEE,2016:138-157.
[40]YAN S,WANG R,HAUSER C,et al.Firmalice-Automatic Detection of Authentication Bypass Vulnerabilities in Binary Firmware[C]∥Network and Distributed System Security Sympo-sium.2015.
[41]STEPHENS N,GROSEN J,SALLS C,et al.Driller:Augmen- ting Fuzzing Through Selective Symbolic Execution[C]∥Network and Distributed System Security Symposium.2016.
[42]LEVIN M Y,LEVIN M Y,MOLNAR D.SAGE:whitebox fuzzing for security testing.https://www.researchgate.net/publication/220309880_SAGE_Whitebox_Fuzzing_for_Security_Testing.
[43]GODEFROID P,KLARLUND N,SEN K.DART:directed automated random testing[C]∥ACM Sigplan Conference on Programming Language Design and Implementation.ACM,2005:213-223.
[44]SONG D,BRUMLEY D,YIN H,et al.BitBlaze:A New Approach to Computer Security via Binary Analysis[C]∥Information Systems Security,International Conference(ICISS 2008).Hyderabad,India,DBLP,2008:1-25.
[45]BABIC′ D,MARTIGNONI L,MCCAMANT S,et al.Statically-directed dynamic automated test generation[C]∥Proceedings of the 2011 International Symposium on Software Testing and Analysis.ACM,2011:12-22.
[46]MARTIGNONI L,MCCAMANT S,POOSANKAM P,et al. Path-exploration lifting:Hi-fi tests for lo-fi emulators[C]∥ACM SIGARCH Computer Architecture News.ACM,2012:337-348.
[1] 黄钊,黄曙光,邓兆琨,黄晖. 基于SEH的漏洞自动检测与测试用例生成[J]. 计算机科学, 2019, 46(7): 133-138.
[2] 方皓, 吴礼发, 吴志勇. 基于符号执行的Return-to-dl-resolve利用代码自动生成方法[J]. 计算机科学, 2019, 46(2): 127-132.
[3] 张永刚, 程竹元. 最大受限路径相容约束传播算法的研究进展[J]. 计算机科学, 2018, 45(6A): 41-45, 62.
[4] 李航, 臧洌, 甘露. 基于蚁群算法的猜测符号执行的路径搜索[J]. 计算机科学, 2018, 45(6): 145-150.
[5] 张婧,周安民,刘亮,贾鹏,刘露平. Crash可利用性分析方法研究综述[J]. 计算机科学, 2018, 45(5): 5-14, 23.
[6] 邓兆琨, 陆余良, 朱凯龙, 黄晖. 基于符号执行技术的网络程序漏洞检测系统[J]. 计算机科学, 2018, 45(11A): 325-329.
[7] 邓维,李兆鹏. 形状分析符号执行引擎中的状态合并[J]. 计算机科学, 2017, 44(2): 209-215.
[8] 陈勇,徐超. 基于符号执行和人机交互的自动向量化方法[J]. 计算机科学, 2016, 43(Z6): 461-466, 492.
[9] 梁家彪,李兆鹏,朱玲,沈咸飞. 支持形状分析的符号执行引擎的设计与实现[J]. 计算机科学, 2016, 43(3): 193-198.
[10] 李华,邢熠,张玉荣. 基于Token选取的OpenStack单一平面网络建模方法[J]. 计算机科学, 2016, 43(11): 66-70, 106.
[11] 王志文,黄小龙,王海军,刘烃,俞乐晨. 基于程序切片的测试用例生成系统研究与实现[J]. 计算机科学, 2014, 41(9): 71-74.
[12] 张亚军,李舟军,廖湘科,蒋瑞成,李海峰. 自动化白盒模糊测试技术研究[J]. 计算机科学, 2014, 41(2): 7-10,22.
[13] 陈翔,顾庆,陈道蓄. 回归测试中测试用例集扩充技术研究进展[J]. 计算机科学, 2013, 40(6): 8-15.
[14] 牛伟纳,丁雪峰,刘智,张小松. 基于符号执行的二进制代码漏洞发现[J]. 计算机科学, 2013, 40(10): 119-121,138.
[15] 李程,魏强,彭建山,王清贤. 基于分解重构的网络软件测试数据生成方法[J]. 计算机科学, 2013, 40(10): 108-113.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] 编辑部. 新网站开通,欢迎大家订阅![J]. 计算机科学, 2018, 1(1): 1 .
[2] 雷丽晖,王静. 可能性测度下的LTL模型检测并行化研究[J]. 计算机科学, 2018, 45(4): 71 -75, 88 .
[3] 夏庆勋,庄毅. 一种基于局部性原理的远程验证机制[J]. 计算机科学, 2018, 45(4): 148 -151, 162 .
[4] 厉柏伸,李领治,孙涌,朱艳琴. 基于伪梯度提升决策树的内网防御算法[J]. 计算机科学, 2018, 45(4): 157 -162 .
[5] 孙启,金燕,何琨,徐凌轩. 用于求解混合车辆路径问题的混合进化算法[J]. 计算机科学, 2018, 45(4): 76 -82 .
[6] 张佳男,肖鸣宇. 带权混合支配问题的近似算法研究[J]. 计算机科学, 2018, 45(4): 83 -88 .
[7] 伍建辉,黄中祥,李武,吴健辉,彭鑫,张生. 城市道路建设时序决策的鲁棒优化[J]. 计算机科学, 2018, 45(4): 89 -93 .
[8] 刘琴. 计算机取证过程中基于约束的数据质量问题研究[J]. 计算机科学, 2018, 45(4): 169 -172 .
[9] 钟菲,杨斌. 基于主成分分析网络的车牌检测方法[J]. 计算机科学, 2018, 45(3): 268 -273 .
[10] 史雯隽,武继刚,罗裕春. 针对移动云计算任务迁移的快速高效调度算法[J]. 计算机科学, 2018, 45(4): 94 -99, 116 .