Данная работа посвящена исследованию и разработке метода обратного символьного выполнения как метода оптимизации символьного выполнения для поиска ошибок в исполняемом бинарном коде. В основе предложенного метода лежит идея использования символьных переменных, взятая из метода символьного выполнения, и идея выполнения кода от результатов выполнения программы к ее входным данным. В результате была предложена формальная модель системы, проанализированы ее преимущества и недостатки. Также рассмотрены методы ее использования в совокупности с классическим методом символьного выполнения. По результатам анализа был сделан вывод о возможности использования предложенного метода как дополнительного инструмента анализаторов, в основе которых лежит идея символьного выполнения. Областью применения полученных результатов являются системы поиска ошибок и уязвимостей бинарных исполняемых файлов, а также область инструментов для автоматического тестирования программного обеспечения.

This paper investigates and develops the method of reverse symbolic execution as an optimization of the symbolic execution method for finding errors in executable binary code. The proposed method is based on the idea of using symbolic variables, taken from the symbolic execution method, and the idea of executing code from the results of program execution to its input data. As a result, a formal model of the system has been proposed and its advantages and disadvantages were analyzed. The methods for its use in conjunction with the classical symbolic execution method were also considered. Based on the results of the analysis, it was concluded that the proposed method can be used as an additional tool for analyzers that are based on the idea of symbolic execution. The area of application of the results obtained is the search systems for errors and vulnerabilities of binary executable files, as well as the area of tools for automatic testing of software.