符号执行研究综述

摘要/Abstract

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

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

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: Concolic testing, Constraint solving, Execution generated test, Path explosion, Symbolic execution

中图分类号:

TP311

叶志斌,严波. 符号执行研究综述[J]. 计算机科学, 2018, 45(6A): 28-35. https://doi.org/

YE Zhi-bin,YAN Bo. Survey of Symbolic Execution[J]. Computer Science, 2018, 45(6A): 28-35. https://doi.org/

参考文献

[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.

相关文章 15

[1]	李明磊, 黄晖, 陆余良, 朱凯龙. SymFuzz:一种复杂路径条件下的漏洞检测技术 SymFuzz:Vulnerability Detection Technology Under Complex Path Conditions 计算机科学, 2021, 48(5): 25-31. https://doi.org/10.11896/jsjkx.200600128
[2]	周晟伊, 曾红卫. 进化算法与符号执行结合的程序复杂度分析方法 Program Complexity Analysis Method Combining Evolutionary Algorithm with Symbolic Execution 计算机科学, 2021, 48(12): 107-116. https://doi.org/10.11896/jsjkx.210200052
[3]	黄钊,黄曙光,邓兆琨,黄晖. 基于SEH的漏洞自动检测与测试用例生成 Automatic Vulnerability Detection and Test Cases Generation Method for Vulnerabilities Caused by SEH 计算机科学, 2019, 46(7): 133-138. https://doi.org/10.11896/j.issn.1002-137X.2019.07.021
[4]	方皓, 吴礼发, 吴志勇. 基于符号执行的Return-to-dl-resolve利用代码自动生成方法 Automatic Return-to-dl-resolve Exploit Generation Method Based on Symbolic Execution 计算机科学, 2019, 46(2): 127-132. https://doi.org/10.11896/j.issn.1002-137X.2019.02.020
[5]	陈正钊, 姜人和, 潘敏学, 张天, 李宣东. 基于约束求解的代码查询技术在StackOverflow上的实证研究 Empirical Study of Code Query Technique Based on Constraint Solving on StackOverflow 计算机科学, 2019, 46(11): 137-144. https://doi.org/10.11896/jsjkx.191100501C
[6]	张永刚, 程竹元. 最大受限路径相容约束传播算法的研究进展 Research Progress on Max Restricted Path Consistency Constraint Propagation Algorithms 计算机科学, 2018, 45(6A): 41-45.
[7]	李航, 臧洌, 甘露. 基于蚁群算法的猜测符号执行的路径搜索 Search of Speculative Symbolic Execution Path Based on Ant Colony Algorithm 计算机科学, 2018, 45(6): 145-150. https://doi.org/10.11896/j.issn.1002-137X.2018.06.025
[8]	张婧,周安民,刘亮,贾鹏,刘露平. Crash可利用性分析方法研究综述 Review of Crash Exploitability Analysis Methods 计算机科学, 2018, 45(5): 5-14. https://doi.org/10.11896/j.issn.1002-137X.2018.05.002
[9]	邓兆琨, 陆余良, 朱凯龙, 黄晖. 基于符号执行技术的网络程序漏洞检测系统 Symbolic Execution Technology Based Defect Detection System for Network Programs 计算机科学, 2018, 45(11A): 325-329.
[10]	邓维,李兆鹏. 形状分析符号执行引擎中的状态合并 State Merging for Symbolic Execution Engine with Shape Analysis 计算机科学, 2017, 44(2): 209-215. https://doi.org/10.11896/j.issn.1002-137X.2017.02.034
[11]	陈勇,徐超. 基于符号执行和人机交互的自动向量化方法 Symbolic Execution and Human-Machine Interaction Based Auto Vectorization Method 计算机科学, 2016, 43(Z6): 461-466. https://doi.org/10.11896/j.issn.1002-137X.2016.6A.109
[12]	梁家彪,李兆鹏,朱玲,沈咸飞. 支持形状分析的符号执行引擎的设计与实现 Symbolic Execution Engine with Shape Analysis 计算机科学, 2016, 43(3): 193-198. https://doi.org/10.11896/j.issn.1002-137X.2016.03.036
[13]	李华,邢熠,张玉荣. 基于Token选取的OpenStack单一平面网络建模方法 Modeling OpenStack Single Plane Network Based on Token Selection 计算机科学, 2016, 43(11): 66-70. https://doi.org/10.11896/j.issn.1002-137X.2016.11.012
[14]	王志文,黄小龙,王海军,刘烃,俞乐晨. 基于程序切片的测试用例生成系统研究与实现 Program Slicing-guied Test Case Generation System 计算机科学, 2014, 41(9): 71-74. https://doi.org/10.11896/j.issn.1002-137X.2014.09.012
[15]	张亚军,李舟军,廖湘科,蒋瑞成,李海峰. 自动化白盒模糊测试技术研究 Survey of Automated Whitebox Fuzz Testing 计算机科学, 2014, 41(2): 7-10.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed