Search Strategies in Dynamic Symbolic Execution

PhD Thesis Proposal Defence


Title: "Search Strategies in Dynamic Symbolic Execution"

by

Mr. Hyunmin SEO


Abstract:

One of the biggest challenges in Dynamic Symbolic Execution (DSE), an 
automatic test generation technique based on symbolic execution, is its 
huge search space. DSE generates next inputs by selecting branches from 
previous execution paths, but a large number of candidate branches makes a 
simple exhaustive search infeasible, which often leads to poor test 
coverage. Several search strategies have been proposed to explore 
high-priority branches only. Each strategy applies different criteria to 
the branch selection process but most do not consider context, how we got 
to the branch, in the selection process. In this work, we introduce a 
context-guided search (CGS) strategy. CGS looks at preceding branches in 
execution paths and selects a branch in a new context for the next input. 
We evaluate CGS with two publicly available concolic testing tools, CREST 
and CarFast, on six C subjects and six Java subjects. The experimental 
results show that CGS achieves the highest coverage of all twelve subjects 
and reaches target coverage with a much smaller number of iterations on 
most subjects than other strategies. This work has been accepted in FSE 
2014.

Although CSG achieves higher coverage with a smaller number of inputs, it 
may still suffer from UNSAT results from the SMT solvers. A branch 
selected by a strategy may only be covered from specific execution paths 
only but search strategies do not know this information and may result in 
continuously selecting a branch until it is covered wasting a large 
portion of testing budget. To address this problem, we propose a technique 
combining static analysis results based on abstract interpretation with 
DSE. Abstract interpretation is a theory of sound approximation of the 
semantics of computer programs. We define domains for the possible values 
of variables in a program and run a pre-analysis and exploit this 
information in the branch selection process. This technique can be 
combined with search strategies to improve coverage in general or to guide 
the execution toward specific code area to test recently changed code such 
as software patches.


Date:			Thursday, 3 July 2014

Time:                   9:30am - 11:30am

Venue:                  Room 3501
                         lifts 25/26

Committee Members:	Dr. Sunghun Kim (Supervisor)
 			Dr. Charles Zhang (Chairperson)
 			Prof. Shing-Chi Cheung
 			Dr. Lei Chen


**** ALL are Welcome ****