Control Systems and Computers, N6, 2019, Статья 1
https://doi.org/10.15407/csc.2019.06.005
Летичевський О.О., Гринюк Я.В., Яковлев В.М. Алгебраїчний підхід у формалізації вразливостей в бінарному коді. Control Systems and Computers. 2019. № 6. C. 5-20.
УДК 004.05, 004.4[2+9], 004.94, 519.7
А.А. Летичевский, докто физ.-мат. наук, зав. отделом, Ин-т кибернетики им. В.М. Глушкова НАН Украины, 03187, г. Киев, просп. Акад. Глушкова, 40, Украина, oleksandr.letychevskyi@garuda.ai
Я.В. Гринюк, аспирант, Ин-т кибернетики им. В.М. Глушкова НАН Украины,
03187, г. Киев, просп. Акад. Глушкова, 40, Украина, yaroslav.hryniuk@garuda.ai
В.М. Яковлев, провідний математик, Ін-т кібернетики ім. В.М. Глушкова НАН України, 03187, м. Київ, просп. Акад. Глушкова, 40, Україна, victoryakovlev@ukr.net
АЛГЕБРАИЧЕСКИЙ ПОДХОД К ФОРМАЛИЗАЦИИ
УЯЗВИМОСТЕЙ В БИНАРНОМ КОДЕ
Введение. Безопасность и защита программных ресурсов в настоящее время — одна из наиболее актуальных проблем в ИТ-индустрии. Подходы к моделированию угроз и поиску уязвимостей, основанные на символьных методах, в последнее десятилетие стали весьма популярными и многообещающими. Данная статья описывает подход к поиску уязвимостей в двоичном коде, основанный на формальных методах символьного моделирования и алгебраического сопоставления.
Цель статьи. Хотя символьное моделирование может быть эффективно использовано для поиска уязвимостей в программном коде, соответствующие программные инструменты работают весьма медленно. Кроме того, проблема достижимости при символьном выполнении программ является неразрешимой в общем случае. В статье предлагается формализация представления двоичного кода и уязвимостей на основе алгебры поведений, а также подход, позволяющий ускорить поиск уязвимостей и сократить область символьного моделирования.
Алгебра поведений используется для представления поведения как двоичного кода, так и уязвимости. Однако, хотя получение представления бинарного кода в терминах алгебры поведений может быть автоматизировано, создание описания уязвимостей требует разработки корректной и эффективной методологии. При использовании представлений в терминах алгебры поведений задача поиска уязвимостей может быть решена в два этапа — относительно быстрого алгебраического сопоставления и собственно символьного моделирования на основе данных, полученных на этапе сопоставления.
Методы. Разработка описаний уязвимостей в терминах алгебры поведений и алгоритма алгебраического сопоставления позволяет ускорить алгоритмы поиска уязвимостей в двоичном программном коде.
Результат. Предложена методика разработки описаний уязвимостей двоичного кода в терминах алгебры поведений. Разработан алгоритм алгебраического сопоставления, включенный в научный прототип, который успешно использован для проверки известных уязвимостей в нескольких программах.
Выводы. Преимущество алгебраического подхода состоит в том, что уязвимости в коде могут быть определены более точно, а описание уязвимости в терминах алгебры поведений позволяет учесть ее различные варианты. Кроме того, эксперименты с прототипом показали, что двухуровневая система поиска уязвимостей работает быстрее, чем чистая система символьного моделирования: вначале выполняется быстрый этап сопоставления, а затем медленный этап символьного моделирования на данных, полученных на предыдущем этапе.
Загрузить полный текст в PDF (на украинском).
Ключевые слова: уязвимости программного обеспечения, символьное моделирование, алгебраическое сопоставление, алгебра поведений.
Поступила 14.11.2019
