Computer Science ›› 2018, Vol. 45 ›› Issue (6A): 28-35.

• Review • Previous Articles     Next Articles

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

CLC Number: 

  • 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.
[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.
[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] ZHOU Sheng-yi, ZENG Hong-wei. Program Complexity Analysis Method Combining Evolutionary Algorithm with Symbolic Execution [J]. Computer Science, 2021, 48(12): 107-116.
[2] HUANG Zhao,HUANG Shu-guang,DENG Zhao-kun,HUANG Hui. Automatic Vulnerability Detection and Test Cases Generation Method for Vulnerabilities Caused by SEH [J]. Computer Science, 2019, 46(7): 133-138.
[3] FANG Hao, WU Li-fa, WU Zhi-yong. Automatic Return-to-dl-resolve Exploit Generation Method Based on Symbolic Execution [J]. Computer Science, 2019, 46(2): 127-132.
[4] CHEN Zheng-zhao, JIANG Ren-he, PAN Min-xue, ZHANG Tian, LI Xuan-dong. Empirical Study of Code Query Technique Based on Constraint Solving on StackOverflow [J]. Computer Science, 2019, 46(11): 137-144.
[5] ZHANG Yong-gang, CHENG Zhu-yuan. Research Progress on Max Restricted Path Consistency Constraint Propagation Algorithms [J]. Computer Science, 2018, 45(6A): 41-45.
[6] LI Hang, ZANG Lie, GAN Lu. Search of Speculative Symbolic Execution Path Based on Ant Colony Algorithm [J]. Computer Science, 2018, 45(6): 145-150.
[7] ZHANG Jing, ZHOU An-min, LIU Liang, JIA Peng and LIU Lu-ping. Review of Crash Exploitability Analysis Methods [J]. Computer Science, 2018, 45(5): 5-14.
[8] DENG Wei and LI Zhao-peng. State Merging for Symbolic Execution Engine with Shape Analysis [J]. Computer Science, 2017, 44(2): 209-215.
[9] CHEN Yong and XU Chao. Symbolic Execution and Human-Machine Interaction Based Auto Vectorization Method [J]. Computer Science, 2016, 43(Z6): 461-466.
[10] LIANG Jia-biao, LI Zhao-peng, ZHU Ling and SHEN Xian-fei. Symbolic Execution Engine with Shape Analysis [J]. Computer Science, 2016, 43(3): 193-198.
[11] LI Hua, XING Yi and ZHANG Yu-rong. Modeling OpenStack Single Plane Network Based on Token Selection [J]. Computer Science, 2016, 43(11): 66-70.
[12] WANG Zhi-wen,HUANG Xiao-long,WANG Hai-jun,LIU Ting and YU Le-chen. Program Slicing-guied Test Case Generation System [J]. Computer Science, 2014, 41(9): 71-74.
[13] ZHANG Ya-jun,LI Zhou-jun,LIAO Xiang-ke,JIANG Rui-cheng and LI Hai-feng. Survey of Automated Whitebox Fuzz Testing [J]. Computer Science, 2014, 41(2): 7-10.
[14] CHEN Shu,YE Jun-min and ZHANG Fan. Automatic Program Testing with Dynamic Symbolic Execution and Model Learning [J]. Computer Science, 2013, 40(8): 161-164.
[15] CHEN Xiang,GU Qing and CHEN Dao-xu. Research Advances in Test Suite Augmentation for Regression Testing [J]. Computer Science, 2013, 40(6): 8-15.
Full text



No Suggested Reading articles found!