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

Sen, Koushik; Agha, Gul A.

Permalink

https://hdl.handle.net/2142/11148 Copy

Description

Title

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

Author(s)

• Sen, Koushik
• Agha, Gul A.

Issue Date

2006-01

Keyword(s)

computer science

Abstract

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.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11148

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections