Ferry: State-Aware Symbolic Execution for Exploring State-Dependent Program Paths


Shunfan Zhou, Zhemin Yang, and Dan Qiao, Fudan University; Peng Liu, The Pennsylvania State University; Min Yang, Fudan University; Zhe Wang and Chenggang Wu, State Key Laboratory of Computer Architecture, Institute of Computing Technology, Chinese Academy of Sciences


Symbolic execution and fuzz testing are effective approaches for program analysis, thanks to their evolving path exploration approaches. The state-of-the-art symbolic execution and fuzzing techniques are able to generate valid program inputs to satisfy the conditional statements. However, they have very limited ability to explore program-state-dependent branches (state-dependent branches in this paper) which depend on earlier program execution instead of the current program inputs.

This paper is the first attempt to thoroughly explore the state-dependent branches in real-world programs. We introduce program-state-aware symbolic execution, a novel technique that guides symbolic execution engines to efficiently explore the state-dependent branches. As we show in this paper, state-dependent branches are prevalent in many important programs because they implement state machines to fulfill their application logic. Symbolically executing arbitrary programs with state-dependent branches is difficult, since there is a lack of unified specifications for their state machine implementation. Faced with this challenging problem, this paper recognizes widely-existing data dependency between current program states and previous inputs in a class of important programs. Our deep insights into these programs help us take a successful first step on this task. We design and implement a tool Ferry, which efficiently guides symbolic execution engine by automatically recognizing program states and exploring state-dependent branches. By applying Ferry to 13 different real-world programs and the comprehensive dataset Google FuzzBench, Ferry achieves higher block and branch coverage than two state-of-the-art symbolic execution engines and three popular fuzzers due to its ability to explore deep program logics, and manages to locate three 0-day vulnerabilities in jhead. Further, we show that Ferry is able to reach more program-state-dependent vulnerabilities than existing symbolic executors and fuzzing approaches with 15 collected state-dependent vulnerabilities and a test suite of six prominent programs. In the end, we test Ferry on LAVA-M dataset to understand its strengths and limitations.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

@inproceedings {277220,
author = {Shunfan Zhou and Zhemin Yang and Dan Qiao and Peng Liu and Min Yang and Zhe Wang and Chenggang Wu},
title = {Ferry: {State-Aware} Symbolic Execution for Exploring {State-Dependent} Program Paths},
booktitle = {31st USENIX Security Symposium (USENIX Security 22)},
year = {2022},
isbn = {978-1-939133-31-1},
address = {Boston, MA},
pages = {4365--4382},
url = {https://www.usenix.org/conference/usenixsecurity22/presentation/zhou-shunfan},
publisher = {USENIX Association},
month = aug

Presentation Video