Home   >   CSC-OpenAccess Library   >    Manuscript Information
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 
A Arusoaie, D Lucanu, V Rusu. "Symbolic execution based on language transformation." Computer Languages, Systems & Structures, 2015. 44: p. 48-71.
AJ Kahn, Y Drougas, AP Shendarkar. "Symbolic execution for web application firewall performance." 2019, Google Patents.
AJ Offutt, JH Hayes. "A semantic model of program faults." in ACM SIGSOFT Software Engineering Notes. 1996. ACM.
C Cadar, K Sen. "Symbolic execution for software testing: three decades later." Commun. ACM, 2013. 56(2): p. 82-90.
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.
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.
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.
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.
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.
CS Pasareanu, R Kersten, K Luckow, QS Phan. "Symbolic Execution and Recent Applications to Worst-Case Execution," Load Testing and Security Analysis.
D Andriesse. "Practical Binary Analysis", no starch press. 2019.
D Brumley, I Jager, T Avgerinos. "BAP: A binary analysis platform." in International Conference on Computer Aided Verification. 2011. Springer.
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.
E Larson, T Austin. "High Coverage Detection of Input Related Security Faults," 12th USENIX Sec. 2001. Symposium.
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.
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.
GE Suh, JW Lee, D Zhang, S Devadas. "Secure program execution via dynamic information flow tracking." in ACM Sigplan Notices. 2004. ACM.
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.
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.
J Jaffar, V Murali, JA Navas, AE Santosa. "TRACER: A symbolic execution tool for verification." in International Conference on Computer Aided Verification. 2012. Springer.
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.
K Sen, D Marinov, G Agha "CUTE: a concolic unit testing engine for C." in ACM SIGSOFT Software Engineering Notes. 2005. ACM.
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.
L Arquint, M Schwerhoff. "Profiling Symbolic Execution." 2019.
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.
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.
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.
N Stephens, J Grosen, C Salls, A Dutcher, R Wang. "Driller: Augmenting Fuzzing Through Selective Symbolic Execution." in NDSS. 2016.
N Tillmann, J De Halleux. "Pex-white box test generation for. net." in International conference on tests and proofs. 2008. Springer.
P Godefroid, MY Levin, D Molnar. "SAGE: whitebox fuzzing for security testing." Communications of the ACM, 2012. 55(3): p. 40-44.
P Godefroid, MY Levin, DA Molnar. "Automated Whitebox Fuzz Testing." in NDSS. 2008. Citeseer.
P Godefroid, N. Klarlund, and K. Sen. "DART: directed automated random testing." in ACM Sigplan Notices. 2005. ACM.
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.
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.
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.
R Baldoni, E Coppa, DC D'elia, C Demetrescu. "A survey of symbolic execution techniques." ACM Computing Surveys (CSUR), 2018. 51(3): p. 50.
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.
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.
S Guo "Efficient Symbolic Execution of Concurrent Software." 2019, Virginia Tech.
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.
S Shen, Shweta Shinde, Soundarya Ramesh, Abhik Roychoudhury, Prateek Saxena. "Neuro-Symbolic Execution: Augmenting Symbolic Execution with Neural Constraints." in NDSS. 2019.
SK Cha, T Avgerinos, A Rebert. "Unleashing mayhem on binary code." in 2012 IEEE Symposium on Security and Privacy. 2012. IEEE.
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.
T Avgerinos, SK Cha, BLT Hao, D Brumley. "AEG: Automatic exploit generation." 2011.
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.
TR Leek, GZ Baker, RE Brown, MA Zhivich. "Coverage maximization using dynamic taint tracing." 2007, MASSACHUSETTS INST OF TECH LEXINGTON LINCOLN LAB.
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.
VP Kemerlis, G Portokalidis, K Jee, AD Keromytis. "libdft: Practical dynamic data flow tracking for commodity systems." in Acm Sigplan Notices. 2012. ACM.
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.
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.
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.
Y Shoshitaishvili, R Wang, C Hauser, C Kruegel. "Firmalice-automatic detection of authentication bypass vulnerabilities in binary firmware." in NDSS. 2015.
Z Xing, Z Bin, F Chao, Z Quan. "Staticly Detect Stack Overflow Vulnerabilities with Taint Analysis." in ITM Web of Conferences. 2016. EDP Sciences.
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