CREST

Concolic test generation tool for C

View project on GitHub

CREST is an automatic test generation tool for C.

CREST works by inserting instrumentation code (using CIL) into a target program to perform symbolic execution concurrently with the concrete execution. The generated symbolic constraints are solved (using Yices) to generate input that drive the test execution down new, unexplored program paths.

CREST currently only reasons symbolically about linear, integer arithmetic. CREST should be usable on any modern Linux or Mac OS X system. For further building and usage information, see the README file. You may also want to check out the FAQ.

Further questions? Please e-mail the CREST-users mailing list (CREST-users at googlegroups.com, searchable at https://groups.google.com/forum/#!forum/crest-users).

A short paper and technical report about the search strategies in CREST are available at the homepage of Jacob Burnim.

News: CREST 0.1.2 is now available. It can be downloaded at https://github.com/jburnim/crest/releases/tag/v0.1.2. This is a bug fix release -- several build issues are fixed, as well as a bug in instrumenting unary expressions.

News: Heechul Yun has extended CREST to support non-linear arithmetic (using Z3). For more information, see: https://github.com/heechul/crest-z3 and https://github.com/heechul/crest-z3/blob/master/README-z3.

Publications

Many research groups have built on top of CREST. If you would like your paper added to the list below, please contact [email protected].

  1. Analysis and Detection of SQL Injection Vulnerabilities via Automatic Test Case Generation of Programs
    M Ruse, T Sarkar, S Basu
    IEEE/IPSJ International Symposium on Applications and the Internet (SAINT), 2010

    1. ParSym: Parallel Symbolic Execution
      Junaid Haroon Siddiqui, Sarfraz Khurshid
      IEEE International Conference on Software Technology and Engineering (ICSTE), 2010

    2. Directed Test Suite Augmentation: Techniques and Tradeoffs
      Zhihong Xu, Yunho Kim, Moonzoo Kim, Gregg Rothermel, Myra Cohen
      ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE), 2010

    3. Striking a New Balance Between Program Instrumentation and Debugging Time
      Olivier Crameri, Ricardo Bianchini, Willy Zwaenepoel
      ACM EuroSys Conference on Computer Systems (EuroSys), 2011

    4. Toward Online Testing of Federated and Heterogeneous Distributed Systems
      Marco Canini, Vojin Jovanovic, Daniele Venzano, Boris Spasojevic, Olivier Crameri, and Dejan Kostic
      USENIX Annual Technical Conference (ATC), 2011

    5. Online testing of federated and heterogeneous distributed systems
      Marco Canini, Vojin Jovanović, Daniele Venzano, Dejan Novaković, Dejan Kostić
      ACM SIGCOMM Conference, 2011

    6. SCORE: a Scalable Concolic Testing Tool for Reliable Embedded Software
      Yunho Kim, Moonzoo Kim
      Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), 2011

    7. MAGIC: Path-Guided Concolic Testing
      Zhanqi Cui, Wei Le, Mary Lou Soffa, Linzhang Wang, Xuandong Li
      University of Virginia Dept. of Computer Science Tech Report, 2011

    8. Extracting and verifying cryptographic models from C protocol code by symbolic execution
      Aizatulin, Gordon, Jürjens
      ACM SIGSAC Conference on Computer and Communications Security (CCS), 2011

    9. Enhancing structural software coverage by incrementally computing branch executability
      Mauro Baluda, Pietro Braione, Giovanni Denaro, Mauro Pezzè
      Software Quality Journal, December 2011

    10. A Scalable Distributed Concolic Testing Approach: An Empirical Evaluation
      Moonzoo Kim, Yunho Kim, Gregg Rothermel
      IEEE International Conference on Software Testing, Verification and Validation (ICST), 2012

    11. Industrial Application of Concolic Testing on Embedded Software: Case Studies
      Moonzoo Kim, Yunho Kim, Yoonkyu Jang
      IEEE International Conference on Software Testing, Verification and Validation (ICST), 2012

    12. Industrial Application of Concolic Testing Approach: A Case Study on libexif by Using CREST-BV and KLEE
      Y Kim, M Kim, YJ Kim, Y Jang
      ACM/IEEE International Conference on Software Engineering (ICSE), 2012

    13. Dynamic Symbolic Execution Guided by Data Dependency Analysis for High Structural Coverage
      TheAnh Do, A.C.M. Fong, Russel Pears, International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE), 2012

    14. Using Concolic Testing to Refine Vulnerability Profiles in FUZZBUSTER
      David J. Musliner, Jeffrey M. Rye, Tom Marble
      IEEE International Conference on Self-Adaptive and Self-Organizing Systems (SASO), 2012

    15. FoREnSiC - An Automatic Debugging Environment for C Programs
      Roderick Bloem, Rolf Drechsler, Goerschwin Fey, Alexander Finder, Georg Hofferek, Robert Koenighofer, Jaan Raik, Urmas Repinski, Andre Suelflow
      International Haifa Verification Conference (HVC), 2012

    16. Feedback-Directed Unit Test Generation for C/C++ using Concolic Execution
      Pranav Garg, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta
      ACM/IEEE International Conference on Software Engineering (ICSE), 2013

    17. Con2colic Testing
      Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith
      Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), 2013

    18. Meta-control for Adaptive Cybersecurity in FUZZBUSTER
      David J. Musliner, Scott E. Friedman, Jeffrey M. Rye
      IEEE International Conference on Self-Adaptive and Self-Organizing Systems (SASO), 2013

    19. CCCD: Concolic Code Clone Detection
      Daniel E. Krutz, Emad Shihab
      IEEE Working Conference on Reverse Engineering (WCRE), 2013

    20. Improving Automated Cybersecurity by Generalizing Faults and Quantifying Patch Performance
      Scott E. Friedman, David J. Musliner, Jeffrey Rye
      International Journal on Advances in Security, 2014

    21. Software testing with code-based test generators: data and lessons learned from a case study with an industrial software component
      Pietro Braione, Giovanni Denaro, Andrea Mattavelli, Mattia Vivanti, Ali Muhammad
      Software Quality Journal, 2014

    22. How We Get There: A Context-Guided Search Strategy in Concolic Testing
      Hyunmin Seo, Sunghun Kim
      ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE), 2014

    23. PBCOV: a property-based coverage criterion
      Kassem Fawaz, Fadi Zaraket, Wes Masri, Hamza Harkous
      Software Quality Journal, March 2015

    24. Directed test suite augmentation: an empirical investigation
      Zhihong Xu, Yunho Kim, Moonzoo Kim, Myra B. Cohen, Gregg Rothermel
      Software Testing, Verification and Reliability, March 2015

    25. Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven
      Yongbae Park, Shin Hong, Moonzoo Kim, Dongju Lee, Junhee Cho
      ACM/IEEE International Conference on Software Engineering (ICSE), 2015

    26. Reusing constraint proofs in program analysis
      Andrea Aquino, Francesco A. Bianchi, Meixian Chen, Giovanni Denaro, Mauro Pezzè
      ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2015

    27. Abstraction-driven Concolic Testing
      Przemysław Daca, Ashutosh Gupta, Thomas A. Henzinger International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2016

    28. CLORIFI: software vulnerability discovery using code clone verification
      Hongzhe Li, Hyuckmin Kwon, Jonghoon Kwon, Heejo Lee
      Concurrency and Computation: Practice and Experience, 2016

    29. PAC learning-based verification and model synthesis
      Yu-Fang Chen, Chiao Hsieh, Ondřej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, Bow-Yaw Wang
      ACM/IEEE International Conference on Software Engineering (ICSE), 2016

    30. Design of a Modified Concolic Testing Algorithm with Smaller Constraints
      Yavuz Koroglu, Alper Sen
      International Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA), 2016