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

Ключевые слова: кибербезопасность программного обеспечения, бинарный анализ, символьное выполнение, символьное моделирование, символьное вычисление, методы поиска уязвимостей.