Concolic Testing of Multithreaded Programs and Its Application to Testing Security Protocols

Testing concurrent programs that accept data inputs is notoriously hard because, beside the large number of possible data inputs, nondeterminism results in an exponentially large number of interleavings of concurrent events. We propose a novel testing algorithm for concurrent programs in which our goal is not only to execute all reachable statements 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 relations among events generated during execution) of a concurrent 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. Symbolic values (variables) are replaced by concrete values if the symbolic state is too complex to be handled by a constraint solver. Our algorithm uses the concrete execution to determine the exact causal structure (or the partial order relations among the events in a concurrent execution) of an execution at runtime. We use this structure to provide a novel technique for exploring only distinct causal structures of a concurrent program with complex data inputs. We describe, jCUTE, a tool implementing the testing algorithm together with the results of applying jCUTE to examples of Java code. Finally, we propose a novel framework on top of jCUTE which allows us to easily implement and analyze cryptographic and security-related protocols. Our effort has been successful in finding security bugs in two cryptographic protocols, suggesting the feasibility of this framework