1 Анализ бинарного кода (в сравнении с исходным кодом) может быть более предпочтительным (абстракция языка высокого уровня может скрывать особенности работы, важные для выявления ошибок) to thesis. Вообще, при символьном выполнении можно как ветвиться и строить разные наборы условий (предикаты пути), так и строить один общий набор условий (например, с использованием ITE) — не предикат пути. Но только при условии развёртки циклов. 2 Эксплойт — набор данных, эксплуатирующих уязвимость. Они получают трассы машинных инструкций из полносистемного эмулятора. Некая среда анализа бинарного кода выделяет алгоритмы из бинарного кода и повышает уровень их представления. Из трассы выделяются только те инструкции, которые относятся к обработке входных данных с момента их получения до падения (с помощью слайсинга с taint-анализом). IR — Pivot (SSA).

Рассматривается переполнение буфера на стеке. 3 Это может привести к перезаписи адреса возврата и аргументов функции. Адрес возврата можно заменить на переход на вредоносный код. Если включён DEP (защита от выполнения кода в стеке), можно использовать ROP для составления полезной нагрузки из существующего кода. От ASLR могут помочь трамплины. Шелл-код — код полезной нагрузки.

Основная схема:

• выделение подтрассы,
• построение предиката пути,
• поиск трамплинов,
• построение экспойта.

Слайсинг удаляет непомеченные инструкции из трассы. 4 Начальный буфер со входными данными задаёт аналитик (обычно — результаты вызовов read()). Потом нужно найти инструкцию, которая перезаписывает одну из ячеек с адресом возврата, и шаг с переходом по перезаписанному адресу.

В трассе ищутся прерывания, после которых был вызван код обработчика исключения. Выясняется, было ли нарушено выполнение.

5 Слайс трассы транслируется в Pivot IR, а Pivot IR в SMT-LIB формулу. Вместо непомеченных ячеек подставляются конкретные значения. Если конкретное значение восстановить не удалось, она считается символьной. Вычисление флагов ленивое. Можно это же добавить в Triton? Регистр счётчика команд не символьный.

6 Для поиска области памяти под шелл-код и передача управления в область также задаётся с помощью уравнений.

9 pages

Sergey Vartanov, 2007–2020