location: Current position: Home >> Scientific Research >> Paper Publications

A Branch History Directed Heuristic Search for Effective Binary Level Dynamic Symbolic Execution

Hits:

Indexed by:期刊论文

Date of Publication:2017-01-01

Journal:IEEE ACCESS

Included Journals:SCIE、EI

Volume:5

Page Number:8752-8762

ISSN No.:2169-3536

Key Words:Dynamic symbolic execution; branch history; test case generation; heuristic search; cyber-physical system

Abstract:Heuristic search is an important part of modern dynamic symbolic execution (DSE) tools, as heuristic search can be used to effectively explore the large program input space. Searching task remains one of several research challenges due to the fact that the input space grows exponentially with the increase of program size, and different programs may have very different structures. The challenge is compounded in a cyber-physical system or cloud-based Internet of Things environment. In this paper, we propose a novel heuristic search algorithm, which analyzes the program execution history and uses the refined history information to inform the search. This paper is based on the observation that the branch and input history generated during dynamic symbolic execution can help memorize the explored input space, and infer the partial structure of the program. With a summarized branch history, the proposed heuristic search makes informed (and better) decisions about which input area to search next for better efficiency. To evaluate the search algorithm, we implement the core DSE engine, integrated with modules to perform execution history collection and analysis. To make our method practical, we incorporate taint analysis and constraint solving statistics to guide the search algorithm. Experimental results demonstrate that with the rich history information, the newsearch algorithm can explore the input space more effectively, thus resulting in detecting software defects faster.

Pre One:Performance Evaluation for Interrupt-Driven Embedded Software Based on EDSPN

Next One:Garakabu2: an SMT-based bounded model checker for HSTM designs in ZIPC