DeepFuzz: Triggering Vulnerabilities Deeply Hidden in Binaries
We introduce a new method for triggering vulnerabilities in deep layers of binary executables and facilitate their exploitation. In our approach we combine dynamic symbolic execution with fuzzing techniques. To maximize both the execution path depth and t
- PDF / 278,846 Bytes
- 10 Pages / 439.37 x 666.142 pts Page_size
- 42 Downloads / 199 Views
Abstract. We introduce a new method for triggering vulnerabilities in deep layers of binary executables and facilitate their exploitation. In our approach we combine dynamic symbolic execution with fuzzing techniques. To maximize both the execution path depth and the degree of freedom in input parameters for exploitation, we define a novel method to assign probabilities to program paths. Based on this probability distribution we apply new path exploration strategies. This facilitates payload generation and therefore vulnerability exploitation.
Keywords: Concolic execution
1
· Fuzzing · Random testing
Introduction
As ubiquitous software is ever increasing in size and complexity, we face the severe challenge to validate and maintain the systems that surround us. Software testing has come a long way from its origins to the recent developments of sophisticated validation techniques. In this paper we introduce a new method combining symbolic execution and random testing. Our goals are (1) code coverage in deep layers of targeted binaries which are unreachable by current technologies and (2) maximal degree of freedom in the input variables when discovering a program error. Before we present the main idea of our approach and the summary of our contributions, we give some background on concolic execution and fuzzing. We especially highlight limitations of concolic execution and fuzzing when applied isolated and motivate a combination of both as a promising new strategy. Concolic Execution. The main idea of symbolic execution is to assign symbolic representations to input variables of a program and generate formulas over the symbols according to the transformations in the program execution. Reasoning about a program on the bases of such symbolic representations of execution paths can provide new insight into the behavior of the program. Besides program c Springer International Publishing Switzerland 2016 J. Caballero et al. (Eds.): DIMVA 2016, LNCS 9721, pp. 25–34, 2016. DOI: 10.1007/978-3-319-40667-1 2
26
K. B¨ ottinger and C. Eckert
verification, symbolic execution nowadays has its biggest impact in program testing. The original idea was extended over the years and developed into concrete symbolic (concolic) execution. The program is initially executed with arbitrary concrete input values and symbolic constraints over the symbols are generated along the program execution path. Next, one of the collected branch conditions is negated and together with the remaining constraints given to an SMT solver. The solution (also called model ) generated by the SMT solver is injected as new input into the program, which now takes the branch alternative when executed. This is because the SMT solver just calculated the solution of the negation of the former branch constraint so that the newly generated input follows the alternative path. This procedure is iteratively repeated until a halt condition is reached. In the best case the reached halt condition resembles full path coverage of all alternative paths of the program, in the
Data Loading...
