IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

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

Show full item record

Bookmark or cite this item: http://hdl.handle.net/2142/11148

Files in this item

File Description Format
PDF Concolic Testin ... ing Security Protocols.pdf (277KB) (no description provided) PDF
Title: Concolic Testing of Multithreaded Programs and Its Application to Testing Security Protocols
Author(s): Sen, Koushik; Agha, Gul A.
Subject(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.
Issue Date: 2006-01
Genre: Technical Report
Type: Text
URI: http://hdl.handle.net/2142/11148
Other Identifier(s): UIUCDCS-R-2006-2676
Rights 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).
Date Available in IDEALS: 2009-04-20
 

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 653
  • Downloads this Month: 4
  • Downloads Today: 0

Browse

My Account

Information

Access Key