С удовольствием и даже гордостью публикуем эту статью. Во-первых, потому что автор — участница нашей программы Summ3r of h4ck, Nalen98. А во-вторых, потому что это исследовательская работа с продолжением, что вдвойне интереснее. Ссылка на первую часть.

Добрый день!

Прошлогодняя стажировка в Digital Security не оставила меня равнодушной к компании и новым исследованиям, так что в этом году я взялась поработать над проектом так же охотно. Темой летней стажировки «Summer of Hack 2020» для меня стала «Символьное исполнение в Ghidra». Нужно было изучить существующие движки символьного исполнения, выбрать один из них и реализовать его в интерфейсе Ghidra. Казалось бы, зачем, ведь в основном движки представляют собой самостоятельные решения? Этот вопрос будет возникать до тех пор, пока не попробовать то, что автоматизирует действия и сделает их наглядными. Это и стало целью разработки.

Статья в какой-то степени является еще и продолжением статьи моего наставника, Андрея Акимова, о решении Kao’s Toy Project с Triton. Только сейчас нам не придется писать ни строчки кода – решить крякми можно будет практически двумя кликами.

Итак, начнем по порядку.

Пара слов о символьном исполнении

Символьное исполнение представляет собой технику анализа программного обеспечения, которая позволяет найти все наборы входных данных, способствующие выполнению каждого из его возможных путей. Если говорить обобщенно, то во время символьного исполнения производится замена переменных/регистров их символьными значениями. Зависимость между переменной и ее символьным значением называется формулой. Единичные формулы объединяются в более сложные и подаются на вход SMT-решателю. Он, в свою очередь, ищет решение к логической формуле и выдает результат «утверждение удовлетворяется» (satisfied) или «утверждение не удовлетворяется» (unsatisfied). Во время символьного исполнения ветки будут расходиться, и произойдет создание форков и новых ограничений на символьные значения. Экспоненциальный рост числа форков является одной из главных проблем в этой области, поскольку для вычислений растущего числа веток требуются большие мощности.

Если говорить об общей классификации движков символьного исполнения, то среди них выделяют статические символьные движки (SSE, emulated) и динамические символьные движки (DSE, concolic). Достоинством статических движков является поддержка эмуляции как всей программы, так и конкретной ее части. И поскольку не происходит непосредственного запуска на CPU, а лишь эмуляция инструкций, открываются возможности для анализа разнообразных архитектур. Однако, страдает масштабируемость, и могут возникнуть определенные трудности со входами в сторонние библиотеки.

DSE, в отличие от SSE, исполняет каждую ветку отдельно, и по своей сути он быстрее, поскольку символизирует не все подряд, а только входные данные пользователя (источник – книга "Practical Binary Analysis" by Dennis Andriesse").

Современные движки могут работать в нескольких режимах в зависимости от предпочтений, так что следующая задача – определиться, какой из движков выбрать.

Выбор символьного движка

Первым наставники посоветовали изучить Triton. С ним хорошо получилось изучить теорию символьного исполнения. Движок может работать как в режиме SSE, так и в режиме DSE. Однако у него ограниченное количество поддерживаемых архитектур (x86, x86-64, ARM32, Arch64), и мне сложно было представить, каким образом можно реализовать его API в контексте интерфейса Ghidr-ы. Так что Triton пришлось отложить и ресерчить дальше.

Следующим подопытным стал KLEE. Он, несомненно, является самым мощным движком символьного исполнения, с его помощью можно работать с по-настоящему серьезными проектами и исследованиями. В контексте реализации архитектуры плагина здесь основной проблемой выступила генерация llvm-биткода. А все потому, что для полноценной работы KLEE необходимо подавать скомпилированные clang-ом в llvm-биткод (.bc) файлы исходников. Были идеи по передачи бинаря llvm-лифтеру (их ассортимент можно увидеть тут), однако ни один из этих вариантов не сработал, и KLEE выдавал ошибки. Говоря о наработках в области трансляции Pcode в llvm, есть лишь один Ghidra-to-LLVM. В рамках ресерча пришлось протестировать и его. Как оказалось, он не работает с 32-битными бинарями, и если и удавалось получить результат в виде .ll-файла, то после обработки llvm-ассемблером llvm-as и получения llvm-биткода KLEE все равно не хотел работать с подобным самопалом и выдавал ошибки. Так что KLEE также пришлось оставить, несмотря на его широкие возможности по символьному исполнению.

Наставники также посоветовали изучить движок S2E. Он расширяет возможности QEMU по трансляции бинарных инструкций в TCG и также транслирует сам TCG в LLVM. Это была заманчивая идея, однако для работы с ним требуется Python3. И, как известно, Ghidra использует старый Jython 2.x, что, казалось бы, полностью перекрывает поток возможностей по интеграции современных инструментов в Ghidr-у. Движок, который был выбран в итоге, тоже работает только с Python3, но в случае с ним возможно было придумать обходной вариант через системный интерпретатор. А поскольку S2E работает как отдельный инструмент, его использование из Ghidr-ы не представляется возможным.

На момент написания статьи вышел еще один движок символьного исполнения SymCC. Точнее, правильно его назвать оберткой компилятора для C-кода. Представьте: у вас на руках исходники, вы компилируете исполняемый файл, как в случае с KLEE и clang-ом, только здесь с SymCC. Компилятор интегрирует необходимый для символьного исполнения код и библиотеки в новоиспеченный исполняемый файл. После запуска получаем директорию с кейсами, сгенерированными во время выполнения. Все классно, но привязать такое к Ghidr-е невозможно, так как у нас на руках не исходники проекта, а результат дизассемблирования и декомпиляции.

Финальным выбором стал angr. Он популярен, у него доступный и подробно задокументированный API, и интегрировать данный движок было действительно реально. Конечно, как уже отмечалось, без Python3 никуда, в Ghidra его поддержка отсутствует, но в случае с angr-ом мне показалось возможным написать универсальный скрипт, который смог бы запускаться на системном интерпретаторе, решать заданный бинарь и передавать результат обратно в Ghidr-у. Вот такой был план.

Сердито. «Костыльно». Канонично

Реализовать получилось так: графический интерфейс плагина получает необходимую информацию от пользователя, создается буферный JSON-файл, куда записывается необходимая конфигурация для работы «универсального angr-скрипта», плагин запускает скрипт на системном интерпретаторе, скрипт передает найденное решение обратно в графический интерфейс.

Если изучить принцип работы декомпилятора в Ghidra и его взаимодействие с GUI, то можно понять, что основе лежит схожий костыльный алгоритм. Дело в том, что Ghidra работает с декомпилятором через stdin и stdout потоки, используя классы DecompileProcess и DecompInterface. Так что архитектуру плагина можно считать вполне каноничной в контексте Ghidra.

На написание логики скрипта не ушло много времени. Он, по сути, собирает в себя базовые возможности angr-a по символьному исполнению ~~для решения ctf-тасков~~. На графический интерфейс пришлось потратить львиную долю времени, и его разработку не могу назвать захватывающей. Как и Ghidra, графический интерфейс плагина написан на Java, в роли IDE по традиции выступил Eclipse.

Для GUI плагина было создано 4 файла:

AngryGhidraPlugin.java – в файле указывается основная информация о плагине и происходит его инициализация.
AngryGhidraProvider.java – самый объемный файл, который инициализирует компоненты графического интерфейса основного окна плагина; здесь прописана логика создания файла конфигурации для скрипта, происходят запуск скрипта и чтение результатов, их передача в интерфейс.
AngryGhidraPopupMenu.java – здесь прописаны дополнительные параметры контекстного меню окна дизассемблера Ghidr-ы. Благодаря этому файлу можно задавать необходимые адреса прямиком из окна дизассемблера, а также внедрять пропатченные байты памяти в контекст работы angr-а.
HookCreation.java – инициализирует окно создания хуков.

Итак, пара слов о функциональных возможностях плагина.

Auto load libs – определяет работу загрузчика необходимых библиотек для исполняемого файла. Пользователь определяет, нужна ему эта опция или нет.
Find Address – адрес, куда вы хотите попасть во время выполнения программы (например, на адрес вывода строки «License key is validated!»).
Blank State – адрес, с которого вы начинаете исполнение. Если не добавлять дополнительных параметров в дальнейшем, то по умолчанию все регистры и память обнулены. Удобно назначать на адресе точки входа или на адресе вызова функции проверки, если вы знаете ее расположение в коде и хотите ускорить процесс работы angr-a.
Avoid addresses – адрес/адреса, которые в ходе символьного исполнения нужно избежать. При их нахождении angr автоматически отметет соответствующие им ветки с меткой «avoid» и не пройдет дальше. Чем больше таких адресов указать, тем чаще angr будет отбрасывать ненужные ветки кода и найдет решение быстрее (если это решение существует).
Arguments – аргументы, поставляемые на вход программе (argv[1], argv[2] и т.д.). Иногда значение, которое необходимо сделать символьным, передается через аргумент(-ы) к программе.
Hooks – хуки позволяют перехватить указанные инструкции и внести определенные значения в регистры. Например, когда необходимо записать в регистры символьные вектора, это будет продемонстрировано в дальнейшем решении Kao’s Toy Project.
Store symbolic vector – если необходимо создать символьный вектор в адресном пространстве определенной длины, а потом, например, поместить его в регистр. Если плагин найдет решение, он выведет содержимое созданного символьного вектора.

Write to memory – иногда бывает необходимо, чтобы определенные участки памяти были заполнены конкретными значениями. Например, в случае Kao’s Toy Project, это значение Installation ID, которое инициализируется по адресу 0x4093a8. Это поле окна плагина можно заполнить патчингом из Ghidr-ы, для этого необходимо пропатчить нужные вам байты, выделить их и открыть контекстное меню дизассемблера AngryGhidraPlugin -> Apply patched bytes.
Registers – те значения регистров, которые вы самостоятельно инициализируете при запуске исполнения с заданного адреса. Здесь также можно создать и сохранить символьные вектора нужной длины.

После успешной работы «универсального» скрипта и нахождения решения плагин выделит цветом всю трассу инструкций, по которой прошла программа чтобы достигнуть желаемого адреса.

Продолжаем хорошую традицию

Наконец, решим Kao’s Toy Project плагином AngryGhidra.

Первое, что сделаем – запустим toyproject.exe в любом отладчике и отследим, по какому адресу записываются байты Installation ID.

Взглянем на байты по адресу 0x4093a8, это и есть наш Installation ID.

Нужно учитывать тот факт, что отладчик в Ghidra отсутствует, а angr осуществляет исполнение бинаря (за это отвечают компоненты PyVEX и SimEngine). Это значит, что значение Installation ID инициализировано не будет, нам нужно сделать это самостоятельно. Наш ход – патчинг байтов в Ghidra.

Найдем адрес 0x4093a8 и запатчим нулевые значения байтами Installation ID, выделим их и выберем в контекстном меню AngryGhidraPlugin -> ApplyPatchedBytes:

Теперь решим вопрос с адресами – куда хотим попасть, чего следует избегать и с чего вообще начнем.

Строка Congratulations! Now write a keygen and tutorial! однозначно для нас искомая, так что адресом для поиска станет адрес помещения в стек этой строки для вызова окна с сообщением. Выберем адрес 0x40123b, для этого можно вписать его в поле Find Address или, открыв контекстное меню, выбрать AngryGhidraPlugin -> Set -> Find Address. Теперь адрес будет перекрашен в зеленый цвет.

Строка That is just wrong. Try harder! говорит о неверном введенном ключе, так что отметим адрес 0x401250 в качестве Avoid Address. Теперь он будет красным в окне дизассемблера.

Чтобы сократить время поиска решения будет удобно выбрать начальное состояние (Blank State) по адресу, где вызывается функция проверки введенного ключа. Это функция 0x4010ec. Выделим адрес вызова этой функции в качестве Blank State Address, и он перекрасится в голубой цвет.

С назначением адресов мы закончили:

Остался последний момент. Заглянем в функцию проверки ключа по адресу 0x4010ec и изучим, каким образом нам стоит передать две части ключа в плагин.

Как можно увидеть, две части ключа передаются в функцию проверки в качестве аргументов. Поскольку наше начальное состояние не предусматривает наличия аргументов, мы должны перехватить момент записи этих аргументов в регистры EDX и EBX и внести символьные значения самостоятельно. Но что они из себя представляют? Вернемся в основную функцию программы и изучим этот момент.

Можно заметить, что первоначально введенные две части ключа обрабатываются функцией по адресу 0x40109d:

Таким образом, каждая часть ключа имеет длину 4 байта, причем второй аргумент для функции проверки будет являться результатом xor-а первой и второй части ключа.

Откроем окно AngryGhidraPlugin и создадим хук по адресу 0x4010ff, чтобы заполнить значения регистров EDX и EBX символьными векторами длиной по 4 байта.

Теперь все готово к запуску, жмем Run и получаем результат!

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

И проверяем:

Ключ подошел! И ни строчки кода! Плагин AngryGhidra сделал все за нас.

Большое спасибо компании Digital Security за интересную стажировку, которая прошла для меня в удаленном формате, наставникам — Андрею (@e13fter) и Саше (@dura_lex), отдельная благодарность за поддержку Виктору Склярову и Борису Рютину (dukebarman)!

Плагин на Github: AngryGhidra.

Укрощение Горыныча 2, или Символьное исполнение в Ghidra