Home   >   CSC-OpenAccess Library   >    Manuscript Information
Full Text Available

This is an Open Access publication published under CSC-OpenAccess Policy.
Publications from CSC-OpenAccess Library are being accessed from over 158 countries worldwide.
A Survey of Symbolic Execution Tools
Salahaldeen Duraibi, Abdullah Alashjaee, Jia Song
Pages - 244 - 254     |    Revised - 30-11-2019     |    Published - 31-12-2019
Volume - 13   Issue - 6    |    Publication Date - December 2019  Table of Contents
Symbolic Execution, Concrete Execution, Concolic Execution, Binary Analysis.
In the software development life cycle (SDLC), testing is an important step to reveal and fix the vulnerabilities and flaws in the software. Testing commercial off-the-shelf applications for security has never been easy, and this is exacerbated when their source code is not accessible. Without access to source code, binary executables of such applications are employed for testing. Binary analysis is commonly used to analyze on the binary executable of an application to discover vulnerabilities. Various means, such as symbolic execution, concolic execution, taint analysis, can be used in binary analysis to help collect control flow information, execution path information, etc. This paper presents the basics of the symbolic execution approach and studies the common tools which utilize symbolic execution in them. With the review, we identified that there are a number of challenges that are associated with the symbolic values fed to the programs as well as the performance and space consumption of the tools. Different tools approached the challenges in different ways, therefore the strengths and weaknesses of each tool are summarized in a table to make it available to interested researchers.
1 refSeek 
2 Doc Player 
3 Scribd 
4 SlideShare 
1 D Andriesse. "Practical Binary Analysis", no starch press. 2019.
2 D Song, David Brumley, Heng Yin, Juan Caballero, Ivan Jager, Min Gyung Kang, Zhenkai Liang, James Newsome, Pongsin Poosankam, Prateek Saxena. "BitBlaze: A new approach to computer security via binary analysis." in International Conference on Information Systems Security. 2008. Springer.
3 M von Maltitz, C Diekmann, G Carle. "Privacy Assessment Using Static Taint Analysis (Tool Paper)." in International Conference on Formal Techniques for Distributed Objects, Components, and Systems. 2017. Springer.
4 X Lin, T Chen, T Zhu, K Yang, F Wei, "Automated forensic analysis of mobile applications on Android devices." Digital Investigation, 2018. 26: p. S59-S66.
5 Z Xing, Z Bin, F Chao, Z Quan. "Staticly Detect Stack Overflow Vulnerabilities with Taint Analysis." in ITM Web of Conferences. 2016. EDP Sciences.
6 C Feng, X Zhang. "A Static Taint Detection Method for Stack Overflow Vulnerabilities in Binaries." 4th International Conference on Information Science and Control Engineering (ICISCE). 2017. IEEE.
7 S Chen, J. Xu , N. Nakka, Z. Kalbarczyk, R.K. Iyer. "Defeating memory corruption attacks via pointer taintedness detection." in 2005 International Conference on Dependable Systems and Networks (DSN'05). 2005. IEEE.
8 GE Suh, JW Lee, D Zhang, S Devadas. "Secure program execution via dynamic information flow tracking." in ACM Sigplan Notices. 2004. ACM.
9 G Venkataramani, Ioannis Doudalis, Yan Solihin, Milos Prvulovic. "Flexitaint: A programmable accelerator for dynamic taint propagation." in 2008 IEEE 14th International Symposium on High Performance Computer Architecture. 2008. IEEE.
10 J Shin, Hongce Zhang, Jinyong Lee, Ingoo Heo, Yu-Yuan Chen, Ruby Lee, Yunheung Paek. "A hardware-based technique for efficient implicit information flow tracking." in 2016 IEEE/ACM International Conference on Computer-Aided Design (ICCAD). 2016. IEEE.
11 VP Kemerlis, G Portokalidis, K Jee, AD Keromytis. "libdft: Practical dynamic data flow tracking for commodity systems." in Acm Sigplan Notices. 2012. ACM.
12 W Xu, S Bhatkar, R Sekar. "Taint-Enhanced Policy Enforcement: A Practical Approach to Defeat a Wide Range of Attacks." in USENIX Security Symposium. 2006.
13 V Ganesh, T Leek, M Rinard. "Taint-based directed whitebox fuzzing." in Proceedings of the 31st International Conference on Software Engineering. 2009. IEEE Computer Society.
14 TR Leek, GZ Baker, RE Brown, MA Zhivich. "Coverage maximization using dynamic taint tracing." 2007, MASSACHUSETTS INST OF TECH LEXINGTON LINCOLN LAB.
15 R Wang, G Xu, X Zeng, X Li, Z Feng. "TT-XSS: A novel taint tracking based dynamic detection framework for DOM Cross-Site Scripting." Journal of Parallel and Distributed Computing, 2018. 118: p. 100-106.
16 J Clause, W Li, A Orso. "Dytan: a generic dynamic taint analysis framework." in Proceedings of the 2007 international symposium on Software testing and analysis. 2007. ACM.
17 C Cadar, K Sen. "Symbolic execution for software testing: three decades later." Commun. ACM, 2013. 56(2): p. 82-90.
18 S Shen, Shweta Shinde, Soundarya Ramesh, Abhik Roychoudhury, Prateek Saxena. "Neuro-Symbolic Execution: Augmenting Symbolic Execution with Neural Constraints." in NDSS. 2019.
19 Q Yi ; Zijiang Yang ; Shengjian Guo ; Chao Wang ; Jian Liu ; Chen Zhao. "Eliminating path redundancy via postconditioned symbolic execution." IEEE Transactions on Software Engineering, 2017. 44(1): p. 25-43.
20 CS Pasareanu and W. Visser. "A survey of new trends in symbolic execution for software testing and analysis." International journal on software tools for technology transfer, 2009. 11(4): p. 339.
21 E Larson, T Austin. "High Coverage Detection of Input Related Security Faults," 12th USENIX Sec. 2001. Symposium.
22 CS Pasareanu, R Kersten, K Luckow, QS Phan. "Symbolic Execution and Recent Applications to Worst-Case Execution," Load Testing and Security Analysis.
23 C Cadar, P Godefroid, S Khurshid. "Symbolic execution for software testing in practice: preliminary assessment." in 2011 33rd International Conference on Software Engineering (ICSE). 2011. IEEE.
24 R Baldon, iEmilio Coppa, Daniele Cono D'Elia "Assisting malware analysis with symbolic execution: A case study." in International Conference on Cyber Security Cryptography and Machine Learning. 2017. Springer.
25 S Khurshid, C.S. Pasareanu, and W. Visser. "Generalized symbolic execution for model checking and testing." in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2003. Springer.
26 X Deng, J Lee "Bogor/kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems." in 21st IEEE/ACM International Conference on Automated Software Engineering (ASE'06). 2006. IEEE.
27 R Baldoni, E Coppa, DC D'elia, C Demetrescu. "A survey of symbolic execution techniques." ACM Computing Surveys (CSUR), 2018. 51(3): p. 50.
28 H Xu, Z Zhao, Y Zhou, MR Lyu. "Benchmarking the Capability of Symbolic Execution Tools with Logic Bombs." IEEE Transactions on Dependable and Secure Computing, 2018.
29 A Arusoaie, D Lucanu, V Rusu. "Symbolic execution based on language transformation." Computer Languages, Systems & Structures, 2015. 44: p. 48-71.
30 AJ Kahn, Y Drougas, AP Shendarkar. "Symbolic execution for web application firewall performance." 2019, Google Patents.
31 L Arquint, M Schwerhoff. "Profiling Symbolic Execution." 2019.
32 T Kuchta, H Palikareva, C Cadar. "Shadow symbolic execution for testing software patches." ACM Transactions on Software Engineering and Methodology (TOSEM), 2018. 27(3): p. 10.
33 M Liang, Z Li, Q Zeng, Z Fang. "Deobfuscation of Virtualization-Obfuscated Code Through Symbolic Execution and Compilation Optimization." in Information and Communications Security: 19th International Conference, ICICS 2017, Beijing, China, December 6-8, 2017, Proceedings. 2018. Springer.
34 S Guo "Efficient Symbolic Execution of Concurrent Software." 2019, Virginia Tech.
35 G Wang, S Chattopadhyay, AK Biswas, T Mitra. "KLEESPECTRE: Detecting Information Leakage through Speculative Cache Attacks via Symbolic Execution." arXiv preprint arXiv:1909.00647, 2019.
36 C Chen, B Cui, J Ma, R Wu, J Guo, W Liu. "A systematic review of fuzzing techniques." Computers & Security, 2018. 75: p. 118-137.
37 P Godefroid, N. Klarlund, and K. Sen. "DART: directed automated random testing." in ACM Sigplan Notices. 2005. ACM.
38 AJ Offutt, JH Hayes. "A semantic model of program faults." in ACM SIGSOFT Software Engineering Notes. 1996. ACM.
39 K Sen, D Marinov, G Agha "CUTE: a concolic unit testing engine for C." in ACM SIGSOFT Software Engineering Notes. 2005. ACM.
40 R Ahmadi, K Jahed, J Dingel. "mCUTE: A Model-level Concolic Unit Testing Engine for UML State Machines." in 34th IEEE/ACM International Conference on Automated Software Engineering (ASE 2019), Demonstration Track, page to appear. ACM. 2019.
41 K Sen, G Agha. "CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools." in International Conference on Computer Aided Verification. 2006. Springer.
42 C Cadar, V Ganesh, PM Pawlowski, DL Dill. "EXE: automatically generating inputs of death." ACM Transactions on Information and System Security (TISSEC), 2008. 12(2): p. 10.
43 P Godefroid, MY Levin, DA Molnar. "Automated Whitebox Fuzz Testing." in NDSS. 2008. Citeseer.
44 P Godefroid, MY Levin, D Molnar. "SAGE: whitebox fuzzing for security testing." Communications of the ACM, 2012. 55(3): p. 40-44.
45 N Tillmann, J De Halleux. "Pex-white box test generation for. net." in International conference on tests and proofs. 2008. Springer.
46 L De Moura, N Bjorner. "Z3: An efficient SMT solver." in International conference on Tools and Algorithms for the Construction and Analysis of Systems. 2008. Springer.
47 J Jaffar, V Murali, JA Navas, AE Santosa. "TRACER: A symbolic execution tool for verification." in International Conference on Computer Aided Verification. 2012. Springer.
48 D Brumley, I Jager, T Avgerinos. "BAP: A binary analysis platform." in International Conference on Computer Aided Verification. 2011. Springer.
49 T Avgerinos, SK Cha, BLT Hao, D Brumley. "AEG: Automatic exploit generation." 2011.
50 SK Cha, T Avgerinos, A Rebert. "Unleashing mayhem on binary code." in 2012 IEEE Symposium on Security and Privacy. 2012. IEEE.
51 T Avgerinos, A Rebert, SK Cha, D Brumley. "Enhancing symbolic execution with veritesting." in Proceedings of the 36th International Conference on Software Engineering. 2014. ACM.
52 Y Shoshitaishvili, R Wang, C Hauser, C Kruegel. "Firmalice-automatic detection of authentication bypass vulnerabilities in binary firmware." in NDSS. 2015.
53 N Stephens, J Grosen, C Salls, A Dutcher, R Wang. "Driller: Augmenting Fuzzing Through Selective Symbolic Execution." in NDSS. 2016.
Mr. Salahaldeen Duraibi
Computer Science Department, University of Idaho, Moscow, ID, 83844, USA
Computer Science Department, Jazan University, Jazan, 45142, Saudi Arabia - United States of America
Mr. Abdullah Alashjaee
Computer Science Department, University of Idaho, Moscow, ID, 83844, USA
Computer Science Department, Northern Borders University, Arar, 73222, Saudi Arabia - United States of America
Dr. Jia Song
Computer Science Department, University of Idaho, Moscow, ID, 83844, USA - United States of America