State of the art: Dynamic symbolic execution for automated test generation

https://doi.org/10.1016/j.future.2012.02.006Get rights and content

Abstract

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 a previous path constraint by an SMT (Satisfiability Modulo Theories) solver in order to steer next executions toward new program paths. It has been introduced into several applications, such as automated test generation, automated filter generation and malware analysis mainly for its two intrinsic properties: low false positives and high code-coverage. In this paper, we focus on the topics that are closely related to automated test generation. Our contributions are five-fold. First, we summarize the theoretical foundation of dynamic symbolic execution. Second, we highlight the challenges when turning ideas into reality. Besides, we describe the state-of-the-art solutions including advantages and disadvantages for those challenges. In addition, twelve typical tools are analyzed and many properties of those tools are censused. Finally, we outline the prospects of this research field in detail.

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)

  • C. Gil 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...
  • J.C. King

    Symbolic execution and program testing

    Journal of the ACM

    (1976)
  • G.J. Myers

    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...
  • C. Cadar et al.

    Execution generated test cases: how to make systems code crash itself

    Lecture Notes in Computer Science

    (2005)
  • C. Cadar, V. Ganesh, P.M. Pawlowski, D.L. Dill, D.R. Engler, EXE: a system for automatically generating inputs of death...
  • P. Godefroid, N. Klarlund, K. Sen, DART: directed automated random testing, in: Proceedings of the ACM SIGPLAN...
  • K. Sen, D. Marinov, G. Agha, CUTE: a concolic unit testing engine for C, in: Proceedings of the Joint 10th European...
  • J. Newsome, B. Karp, D. Song, Polygraph: automatically generating signatures for polymorphic worms, in: Proceedings of...
  • Z.C. Li, M. Sanghi, Y. Chen, M.Y. Kao, B. Chavez, Hamsa: fast signature generation for zero-day polymorphic worms with...
  • X.S. Zhang et al.

    SISG: self-immune automated signature generation for polymorphic worms

    COMPEL—The International Journal for Computation and Mathematics in Electrical and Electronic Engineering

    (2010)
  • D. Brumley, J. Newsome, D. Song, H. Wang, S. Jha, Towards automatic generation of vulnerability-based signatures, in:...
  • D. Brumley et al.

    Theory and techniques for automatic generation of vulnerability-based signatures

    IEEE Transactions on Dependable and Secure Computing

    (2008)
  • D. Brumley, H. Wang, S. Jha, D. Song, Creating vulnerability signatures using weakest preconditions, in: Proceedings of...
  • Z.K. Liang, R. Sekar, Fast and automated generation of attack signatures: a basis for building self-protecting servers,...
  • J. Newsome, D. Brumley, D. Song, J. Chamcham, X. Kovah, Vulnerability-specific execution filtering for exploit...
  • D. Brumley, C. Hartwig, M.G. Kang, Z.K. Liang, J. Newsome, P. Poosankam, D. Song, Bitscope: automatically dissecting...
  • D. Brumley et al.

    Automatically identifying trigger-based behavior in malware

  • A. Moser, C. Kruegel, E. Kirda, Exploring multiple execution paths for Malware analysis, in: Proceedings of IEEE...
  • D. Song, D. Brumley, Yin Heng, J. Caballero, I. Jager, G.K. Min, Z.K. Liang, J. Newsome, P. Poosankam, P. Saxena,...
  • E.M. Clarke, E.A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, in:...
  • S. Cha et al.

    A safety-focused verification using software fault trees

    Future Generation Computer Systems

    (2011)
  • G. Fraser et al.

    Testing with model checkers: a survey

    Software Testing Verification and Reliability

    (2009)
  • A. Biere, A. Climatti, E.M. Clarke, Y.S. Zhu, Symbolic model checking without BDDs, in: Proceedings of the 5th...
  • P. McMinn

    Search-based software test data generation: a survey

    Software Testing Verification and Reliability

    (2004)
  • M. Harman, Automated test data generation using search based software engineering, in: Proceedings of International...
  • M. Harman, R. Hierons, M. Proctor, A new representation and crossover operator for search-based optimization of...
  • P. Baker, M. Harman, K. Steinhofel, A. Skaliotis, Search based approaches to component selection and prioritization for...
  • S. Bouktif, H. Sahraoui, G. Antoniol, Simulated annealing for improving software quality prediction, in: Proceedings of...
  • P.M.S. Bueno et al.

    Automatic test data generation for program paths using genetic algorithms

    International Journal of Software Engineering and Knowledge Engineering

    (2002)
  • X.B. Wang, N. Su, Automatic test data generation for path testing using genetic algorithms, in: Proceedings of 3rd...
  • P. Joshi, K. Sen, M. Shlimovich, Predictive testing: amplifying the effectiveness of software testing, Technical Report...
  • N. Tillmann, J. De Halleux, Pex-white box test generation for.NET, in: Proceedings of 2nd International Conference on...
  • P. Godefroid, Compositional dynamic test generation, in: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on...
  • S. Anand, P. Godefroid, N. Tillmann, Demand-driven compositional symbolic execution, in: Proceedings of 14th...
  • P. Godefroid, A.V. Nori, S.K. Rajamani, S.D. Tetali, Compositional may-must program analysis: unleashing the power of...
  • P. Godefroid, D. Luchaup, Automatic partial loop summarization in dynamic test generation, in: Proceedings of 2011...
  • P. Godefroid, A. Kiezun, M.Y. Levin, Grammar-based whitebox fuzzing, in: Proceedings of the ACM SIGPLAN Conference on...
  • R. Majumdar, R.G. Xu, Directed test generation using symbolic grammars, in: Proceedings of ACM/IEEE International...
  • R.G. Xu, P. Godefroid, R. Majumdar, Testing for buffer overflows with length abstraction, in: Proceedings of the...
  • R. Majumdar et al.

    Reducing test inputs using information partitions

  • P. Godefroid, J. Kinder, Proving memory safety of floating-point computations by combining static and dynamic program...
  • B. Elkarablieh, P. Godefroid, M.Y. Levin, Precise pointer reasoning for dynamic test generation, in: Proceedings of...
  • M.I. Emmi, R. Majumdar, K. Sen, Dynamic test input generation for database applications, in: Proceedings of ACM...
  • K. Taneja, Y. Zhang, T. Xie, MODA: automated test generation for database applications via mock objects, in:...
  • Cited by (62)

    • Random or heuristic? An empirical study on path search strategies for test generation in KLEE

      2022, Journal of Systems and Software
      Citation 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 Investigation
    • A Systematic Review of Search Strategies in Dynamic Symbolic Execution

      2020, Computer Standards and Interfaces
      Citation 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 Technology
      Citation 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.

    View all citing articles on Scopus

    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.

    View full text