Proceedings of ISP RAS

Building security predicates for some types of vulnerabilities

Fedotov A.N. (ISP RAS, Moscow, Russia)
Kaushan V.V. (ISP RAS, Moscow, Russia)
Gaissaryan S.S. (ISP RAS, Moscow, Russia; MSU, Moscow, Russia; MIPT, Dolgoprudny, Moscow Region, Russia; HSE, Moscow, Russia)
Kurmangaleev Sh.F. (ISP RAS, Moscow, Russia)


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.


software bugs; symbolic execution; security predicates; binary analysis; dynamic analysis


Proceedings of the Institute for System Programming, vol. 29, issue 6, 2017, pp. 151-162.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

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

Full text of the paper in pdf (in Russian) Back to the contents of the volume