Concolic testing of multithreaded programs and its application to testing security protocols

Testing concurrent programs that accept data inputs is no-toriously hard because, besides the large number of possi-ble data inputs, nondeterminism results in an exponentially large number of interleavings of concurrent events. We pro-pose a novel testing algorithm for concurrent programs in which our goal is not only to execute all reachable state-ments of a program, but to detect all possible data races, and deadlock states. The algorithm uses a combination of symbolic and concrete execution (called concolic execution) to explore all distinct causal structures (or partial order re-lations among events generated during execution) of a con-current program. The idea of concolic testing is to use the symbolic execution to generate inputs that direct a program to alternate paths, and to use the concrete execution to guide the symbolic execution along a concrete path. Our algorithm uses the concrete execution to compute the exact race conditions between the events of an execution at run-time. Subsequently, we systematically re-order or permute the events involved in these races by generating new thread schedules as well as generate new test inputs. This way we explore at least one representative from each partial order. We describe jCUTE, a tool implementing the testing algo-rithm together with the results of applying jCUTE to real-world multithreaded Java applications and libraries. In one of our case studies, we discovered several undocumented po-tential concurrency-related bugs in the widely used Java col-lection framework distributed with the Sun Microsystems’ JDK 1.4. 1