RUS  ENG
Full version
JOURNALS // Proceedings of the Institute for System Programming of the RAS // Archive

Proceedings of ISP RAS, 2017 Volume 29, Issue 6, Pages 151–162 (Mi tisp278)

This article is cited in 2 papers

Building security predicates for some types of vulnerabilities

A. N. Fedotova, V. V. Kaushana, S. S. Gaissaryanabcd, Sh. F. Kurmangaleeva

a Ivannikov Institute for System Programming of the Russian Academy of Sciences
b Lomonosov Moscow State University
c National Research University Higher School of Economics (HSE)
d Moscow Institute of Physics and Technology (State University)

Abstract: Approaches for code execution using program vulnerabilities are considered in this paper. Particularly, ways of code execution using buffer overflow on stack and on heap, using use-after-free vulnerabilities and format string vulnerabilities are examined in section 2. Methods for automatic generation input data, leading to code execution are described in section 3. This methods are based on dynamic symbolic execution. Dynamic symbolic execution allows to gain input data, which leads program along the path of triggering vulnerability. The security predicate is an extra set of symbolic formulas, describing program's state in which code execution is possible. To get input data, leading to code execution, path and security predicates need to be united, and then the whole system should be solved. Security predicates for pointer overwrite, function pointer overwrite and format string vulnerability, that leads to stack buffer overflow are presented in the paper. Represented security predicates were used in method for software defect severity estimation. The method was applied to several binaries from Darpa Cyber Grand Challenge. Testing security predicate for format string vulnerability, that leads to buffer overflow was conducted on vulnerable version of Ollydbg. As a result of testing it was possible to obtain input data that leads to code execution.

Keywords: software bugs, symbolic execution, security predicates, binary analysis, dynamic analysis.

DOI: 10.15514/ISPRAS-2017-29(6)-8



Bibliographic databases:


© Steklov Math. Inst. of RAS, 2024