State of the art: Dynamic symbolic execution for automated test generation
Highlights
► We summarize the theoretical foundation of dynamic symbolic execution. ► Several challenges of this research field are highlighted. ► We describe state-of-the-art solutions for those challenges. ► Twelve typical dynamic symbolic execution tools are analyzed and compared. ► We outline the prospects of this research field in detail.
Introduction
Dynamic Symbolic Execution (DSE) for automated test generation consists of instrumenting and running a program while collecting path constraint on inputs from predicates encountered in branch instructions, and of deriving new inputs from the previous path constraint by an SMT (Satisfiability Modulo Theories) solver in order to steer next executions toward new program paths. DSE has become an attractive technique in the software engineering research for its two intrinsic properties. First, DSE does not suffer from significant false positives because the executing program affords enough runtime information. Typical DSE tools such as Fuzzgrind [1] and SAGE [2] produce alarms only when software exceptions are occurred in runtime. Second, in general, each new input generated by a solver is able to exercise new path, thus DSE leads to high code-coverage by traversing all program paths.
Symbolic execution has been studied since 70’s [3], [4]. But in the past 30 years, effective solutions and tools have proven elusive for several insurmountable technical challenges at that time. In recent years, thanks to powerful modern computers, potent symbolic execution engines, excellent constraint solvers, practical software model checkers, efficient theorem provers and precise yet scalable static analysis tools, symbolic execution has developed a lot. Now DSE becomes one of the hottest spots in the software engineering research. For instance, three papers in 2010 IEEE Symposium on Security and Privacy focused on this technique [5], [6], [7]. Quite a few applications utilize DSE and here are some examples.
Automated test generation. DSE is introduced in automated test generation for its low false positives and high code-coverage. This technique is now the foundation of several vulnerability discovery tools [2], [8], [9], [10], [11], [12]. The majority of these tools are capable of automatically finding well-defined bugs, such as buffer overflows, divisions by zero, NULL pointer dereferences, etc.
Automated filter generation. Intrusion Detection/Prevention System (IDS/IPS) and anti-virus software always take advantage of input filters to block inputs that trigger bugs and vulnerabilities. A few years ago, input filters could only be produced by manual work. In order to contain fast spreading malcode, several automated input filters generation tools which aim at finding common byte sequences in different copies of one malcode are proposed [13], [14], [15]. Recently DSE has been absorbed into this research branch so as to find vulnerability signatures—a vulnerability signature is used to detect/prevent all kinds of attacks that target the specified vulnerability [16], [17], [18], [19], [20].
Malware analysis. Automated reverse-engineering techniques for malware analysis have employed DSE these years. Hence, the ability of analyzing how information flows through a malware binary and exploring behaviors to trigger malware is remarkably raised [21], [22], [23], [24].
In this paper, we only focus on the topics that are closely related to DSE based automated test generation. We feel necessary to clarify that two research fields—model checking based and search based test generation which seem to be close to DSE are out of the range of this article. Model checking [25], [26] is a widely-accepted verification technique which takes a temporal logic property and analyzes the model in order to determine whether the model violates the property or not. A nature feature of model checking is the ability to generate witnesses and counter-examples for property satisfaction or violation respectively [27], [28]. From software testing aspect, the counter-examples can be interpreted as test cases. DSE and model checking based test generation vary a lot in terms of methodology by their definitions even though they have similar purpose. Actually, these two research branches overlap to some extent and their collaboration will be described in more detail in Section 7.
Test generation could be considered as an optimization question that finding solutions to the test criteria via search based algorithms [29], [30]. There is a significant discrepancy between DSE and search based test generation that the former uses an SMT solver to obtain solutions directly while the latter utilizes search algorithms such as hill climbing [31], simulated annealing [32], [33], [34], genetic algorithms [35], [36] etc. to approach solutions. In Section 7, we will see that those two techniques could be integrated in order to cope with more complicate programs and get higher code coverage with fewer test cases.
Our contributions are five-fold. First, we summarize the theoretic foundation of DSE, including formal representation and conceptual descriptions. Second, we underline the challenges when turning ideas into reality. In addition to above two, we describe the up-to-date solutions. We have to note here that existing solutions can only partially address those challenges and the ideal alternatives are still in the research. Here, we briefly list all challenges and related solutions referred in this paper in Table 1.
The fourth contribution is that we compare and analyze twelve typical DSE tools in Section 6. Many features such as platform, instrumentation tools, SMT solvers etc. are compared in detail. Researchers and practitioners will benefit from this section to choose proper DSE tools for their own purposes or make decision to develop new DSE tools if current ones cannot meet their requirements. Moreover, we discuss the prospects of DSE for automated test generation in detail. Here, we just briefly list the trend: new techniques to figure out path explosion, more powerful SMT solvers, particular security tools for particular applications, manageable summary database and parallel DSE.
The remainder of this paper is organized as follows. Section 2 summarizes the theoretic foundation of DSE and then we present a simple example to illustrate how to generate tests automatically by means of DSE. Section 3 explains why we need DSE, i.e., we present the drawbacks of static techniques and black-box fuzzing as well as the advantages of DSE. Section 4 focuses on the challenges when turning ideas into reality and then we introduce several state-of-the-art solutions against those challenges. Section 5 describes some popular techniques that aim at improving efficiency of DSE. Section 6 compares and analyzes twelve typical DSE tools from many aspects. Section 7 mainly discusses the prospects of DSE for automated test generation in detail. Section 8 concludes this paper.
Section snippets
Definition of DSE
In this section, we first summarize the theoretic foundation of DSE, including formal representation and conceptual descriptions. Then we give a simple example to illustrate how to generate tests automatically by means of DSE.
We present the widely accepted definition by quite a few subsequent studies [24], [39], [51] of DSE which is first proposed in DART [11]. Equivalent definition in an abstract imperative programming language can be found in [45], [46], [52].
DSE consists of running the
Remarkable advantages of DSE
Before people are aware of the advantages of DSE, static techniques and black-box fuzzing are the mainstream that have been used in many security tools, e.g., [59], [60], [61]. Now, DSE is becoming a hot research point. The reason lies in that DSE is far more accurate than static analysis and it has a better code coverage compared to black-box fuzzing.
Static test generation is often ineffective.
The major difference between static test generation and DSE lies in that static techniques analyze a
Challenges and solutions
To the best of our knowledge, mature tools based on dynamic symbolic execution for commercial use do not exist yet, though this technique has been investigated for a few years. The majority of current DSE tools such as Fuzzgrind [1], KLEE [8], EXE [10], DART [11], CUTE [12] are only for research purpose. SAGE [2], a commercial tool, which is developed by Microsoft, is not available outside of Microsoft Corporation. Pex [38], a DSE tool for unit testing which works as a plug-in component
Other techniques to improve DSE
Many researchers agree that for the whole cost of DSE, the cost of constraint solving dominates everything else since constraint solving is a NP-complete problem [8] whose algorithmic solutions are currently believed to have exponential worst case complexity [76]. In order to apply symbolic execution technique in real complex programs, several methods [8], [10], [12] that aim at simplifying constraint expressions or reducing queries to SMT solvers have been proposed in recent years.
Comparison and analysis of typical DSE tools
In this section, we compare and analyze twelve typical DSE tools from many aspects. Researchers and practitioners can indeed benefit from this section for choosing proper DSE tools for their own purposes, if they exist. Otherwise, this section helps people build novel DSE tools by referring exist tools. Detailed comparison results are presented in Table 2.
One thing we have to point out is that the tools listed here are not complete, actually only twelve well-known tools are presented.
Prospects of DSE
In recent years, dynamic symbolic execution has been intensively researched mainly for its two inherent merits: low false positives and high code-coverage. However, hitherto this technique is not competent to handle the real complex programs for the challenges mentioned above. Unfortunately, until now, several challenges e.g., path explosion, floating-point computations and environmental interaction have not been settled properly. Needless to say, these unsolved problems are certain to be the
Conclusion
Dynamic symbolic execution for automated test generation consists of instrumenting and running a program while collecting path constraint on inputs from predicates encountered in branch instructions, and of deriving new inputs from previous path constraint by an SMT solver in order to steer next executions toward new program paths. DSE has been introduced into several applications, such as automated test generation, automated filter generation and malware analysis mainly for two intrinsic
Ting Chen received the BS degree in mathematics from University of Electronic and Technology of China (UESTC), Chengdu, in 2007, and the MS degree in computer science from UESTC in 2010. Now he is pursuing his Ph.D. degree at UESTC. He has published several articles in prestigious journals and conferences in the fields of malware analysis, intrusion detection and software testing. He has obtained several Chinese patents with regard to computer security. His current research includes software
References (107)
- et al.
Annealing-based heuristics and genetic algorithms for circuit partitioning in parallel test generation
Future Generation Computer Systems
(1998) - Fuzzgrind an automatic fuzzing tool Fuzzgrind....
- P. Godefroid, M. Levin, D. Molnar, Automated whitebox fuzz testing, in: Proceedings of the Network and Distributed...
Symbolic execution and program testing
Journal of the ACM
(1976)The Art of Software Testing
(1979)- E.J. Schwartz, T. Avgerinos, D. Brumley, All you ever wanted to know about dynamic taint analysis and forward symbolic...
- P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, D. Song, A symbolic execution framework for JavaScript, in:...
- T.L. Wang, T. Wei, G.F. Gu, W. Zou, TaintScope: a checksum-aware directed fuzzing tool for automatic software...
- C. Cadar, D. Dunbar, D. Engler, Klee: unassisted and automatic generation of high-coverage tests for complex systems...
- et al.
Execution generated test cases: how to make systems code crash itself
Lecture Notes in Computer Science
(2005)
SISG: self-immune automated signature generation for polymorphic worms
COMPEL—The International Journal for Computation and Mathematics in Electrical and Electronic Engineering
Theory and techniques for automatic generation of vulnerability-based signatures
IEEE Transactions on Dependable and Secure Computing
Automatically identifying trigger-based behavior in malware
A safety-focused verification using software fault trees
Future Generation Computer Systems
Testing with model checkers: a survey
Software Testing Verification and Reliability
Search-based software test data generation: a survey
Software Testing Verification and Reliability
Automatic test data generation for program paths using genetic algorithms
International Journal of Software Engineering and Knowledge Engineering
Reducing test inputs using information partitions
Cited by (62)
Effuzz: Efficient fuzzing by directed search for smart contracts
2023, Information and Software TechnologyMonitoring machine learning models: a categorization of challenges and methods
2022, Data Science and ManagementRandom or heuristic? An empirical study on path search strategies for test generation in KLEE
2022, Journal of Systems and SoftwareCitation Excerpt :During DSE, random path search strategies, such as random-path or random-state (Cadar et al., 2008a), are the simplest and most intuitive strategies for path searching. It has two significant advantages: One is that it favors paths with fewer constraints and so it has greater freedom to hit uncovered code (Chen et al., 2013); another is that random strategies could avoid starvation during symbolic execution, because execution paths with large numbers of branches are not able to predominate execution chances with the random selection (Chen et al., 2013). Since the potential risk of path explosion, some heuristic path search strategies, such as graph and coverage-optimized search approach, have been proposed used in DSE in recent years.
Seance: Divination of tool-breaking changes in forensically important binaries
2021, Forensic Science International: Digital InvestigationA Systematic Review of Search Strategies in Dynamic Symbolic Execution
2020, Computer Standards and InterfacesCitation Excerpt :Furthermore, it appears that in the proposed search strategies, achieving high code coverage (specially branch coverage) with less efforts is the most demanding testing goal. In the literature, there are various surveys on symbolic and also dynamic symbolic execution with the focus on software testing (e.g., [31,45–49]). However, none of them give an in-depth overview of search strategies.
FSCT: A new fuzzy search strategy in concolic testing
2019, Information and Software TechnologyCitation Excerpt :This process continues until the desired coverage is achieved. Despite the success of concolic testing in finding bugs and improving quality of code, it suffers from the so-called path explosion problem [18,20,21] which poses a threat to its scalability. The number of paths within the SUT grows exponentially with the increase of the number of branch conditions encountered during the execution, and exhaustively exploring all these paths is infeasible for any nontrivial program.
Ting Chen received the BS degree in mathematics from University of Electronic and Technology of China (UESTC), Chengdu, in 2007, and the MS degree in computer science from UESTC in 2010. Now he is pursuing his Ph.D. degree at UESTC. He has published several articles in prestigious journals and conferences in the fields of malware analysis, intrusion detection and software testing. He has obtained several Chinese patents with regard to computer security. His current research includes software reliability, software test case generation and software verification.
Xiao-song Zhang graduated with a BS degree in dynamics engineering from Shanghai Jiaotong University, Shanghai, in 1990, and an MS and Ph.D. degree in computer science from UESTC, Chengdu, in 2011. Now he is a Professor in computer science at UESTC. He has worked on numerous projects in both research and development roles. These projects include device security, intrusion detection, malware analysis, software testing and software verification. He has coauthored a number of research papers on computer security. His current research involves in software reliability, software vulnerability discovering, software test case generation and reverse engineering.
Shi-ze Guo is a Professor in Beijing University of Posts and Telecommunications. He has served as research scientist at Institute of North Electronic Equipment. His current research is relevant to software engineering and formal methods.
Hong-yuan Li received the BS degree in computer science from UESTC, Chengdu, in 2010. Now he is pursuing his MS degree in computer science at UESTC. His current research includes malware detection on smart phone and software reliability analysis.
Yue Wu is a Professor in UESETC. He had severed as Dean of School of Computer Science and Engineering in UESTC from 2001 to 2006. He was the Dean of School of Information and Software Engineering in UESTC from 2002 to 2006. He worked as the Dean of School of Software in Chengdu College of UESTC from 2002 to 2004. He is a committee member of several journals including Journal of UESTC, Journal of Computer Applications, Software World. He has presided over a number of international conferences such as CIDE 2005 and ISNN 2006. He has published more than 70 research papers and authored 3 books. His current research focuses on grid computing, database systems and data mining.