Global InformationConcolic testing information
Concolic testing (a portmanteau of concrete and symbolic, also known as dynamic symbolic execution) is a hybrid software verification technique that performs symbolic execution, a classical technique that treats program variables as symbolic variables, along a concrete execution (testing on particular inputs) path. Symbolic execution is used in conjunction with an automated theorem prover or constraint solver based on constraint logic programming to generate new concrete inputs (test cases) with the aim of maximizing code coverage. Its main focus is finding bugs in real-world software, rather than demonstrating program correctness.
A description and discussion of the concept was introduced in "DART: Directed Automated Random Testing" by Patrice Godefroid, Nils Klarlund, and Koushik Sen.[1] The paper "CUTE: A concolic unit testing engine for C",[2] by Koushik Sen, Darko Marinov, and Gul Agha, further extended the idea to data structures, and first coined the term concolic testing. Another tool, called EGT (renamed to EXE and later improved and renamed to KLEE), based on similar ideas was independently developed by Cristian Cadar and Dawson Engler in 2005, and published in 2005 and 2006.[3] PathCrawler[4][5] first proposed to perform symbolic execution along a concrete execution path, but unlike concolic testing PathCrawler does not simplify complex symbolic constraints using concrete values. These tools (DART and CUTE, EXE) applied concolic testing to unit testing of C programs and concolic testing was originally conceived as a white box improvement upon established random testing methodologies. The technique was later generalized to testing multithreaded Java programs with jCUTE,[6] and unit testing programs from their executable codes (tool OSMOSE).[7] It was also combined with fuzz testing and extended to detect exploitable security issues in large-scale x86 binaries by Microsoft Research's SAGE.[8][9]
The concolic approach is also applicable to model checking. In a concolic model checker, the model checker traverses states of the model representing the software being checked, while storing both a concrete state and a symbolic state. The symbolic state is used for checking properties on the software, while the concrete state is used to avoid reaching unreachable state. One such tool is ExpliSAT by Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening and Ishai Rabinovitz[10]
- ^ Patrice Godefroid; Nils Klarlund; Koushik Sen (2005). "DART: Directed Automated Random Testing" (PDF). Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation. New York, NY: ACM. pp. 213–223. ISSN 0362-1340. Archived from the original (PDF) on 2008-08-29. Retrieved 2009-11-09.
- ^ Koushik Sen; Darko Marinov; Gul Agha (2005). "CUTE: a concolic unit testing engine for C" (PDF). Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering. New York, NY: ACM. pp. 263–272. ISBN 1-59593-014-0. Archived from the original (PDF) on 2010-06-29. Retrieved 2009-11-09.
- ^ Cristian Cadar; Vijay Ganesh; Peter Pawloski; David L. Dill; Dawson Engler (2006). "EXE: Automatically Generating Inputs of Death" (PDF). Proceedings of the 13th International Conference on Computer and Communications Security (CCS 2006). Alexandria, VA, USA: ACM.
- ^ Nicky Williams; Bruno Marre; Patricia Mouy (2004). "On-the-Fly Generation of K-Path Tests for C Functions". Proceedings of the 19th IEEE International Conference on Automated Software Engineering (ASE 2004), 20–25 September 2004, Linz, Austria. IEEE Computer Society. pp. 290–293. ISBN 0-7695-2131-2.
- ^ Nicky Williams; Bruno Marre; Patricia Mouy; Muriel Roger (2005). "PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis". Dependable Computing - EDCC-5, 5th European Dependable Computing Conference, Budapest, Hungary, April 20–22, 2005, Proceedings. Springer. pp. 281–292. ISBN 3-540-25723-3.
- ^ Koushik Sen; Gul Agha (August 2006). "CUTE and jCUTE : Concolic Unit Testing and Explicit Path Model-Checking Tools". Computer Aided Verification: 18th International Conference, CAV 2006, Seattle, WA, USA, August 17–20, 2006, Proceedings. Springer. pp. 419–423. ISBN 978-3-540-37406-0. Archived from the original on 2010-06-29. Retrieved 2009-11-09.
- ^ Sébastien Bardin; Philippe Herrmann (April 2008). "Structural Testing of Executables" (PDF). Proceedings of the 1st IEEE International Conference on Software Testing, Verification, and Validation (ICST 2008), Lillehammer, Norway. IEEE Computer Society. pp. 22–31. ISBN 978-0-7695-3127-4.,
- ^ Patrice Godefroid; Michael Y. Levin; David Molnar (2007). Automated Whitebox Fuzz Testing (PDF) (Technical report). Microsoft Research. TR-2007-58.
- ^ Patrice Godefroid (2007). "Random testing for security: blackbox vs. whitebox fuzzing" (PDF). Proceedings of the 2nd international workshop on Random testing: co-located with the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007). New York, NY: ACM. p. 1. ISBN 978-1-59593-881-7. Retrieved 2009-11-09.
- ^ Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening, Ishai Rabinovitz: ExpliSAT: Guiding SAT-Based Software Verification with Explicit States. Haifa Verification Conference 2006: 138-154