Символическое выполнение в IDA: Ponce

Символическое выполнение (или symbolic execution) постепенно становится трендом современной отладки приложений. Появляются и совершенствуются инструменты для удобного анализа поведения и его изменения. В 2016 году на Hex-Rays Plugin Contest Альберто Гарсия Иллера и Ока Франциско представили плагин для самого популярного дизассемблера  -- IDA, который позволяет проводить символическое выполнение в несколько кликов.

Символическое выполнение?

При "обычном" выполнении программы мы даем ей данные и ожидаем какого-то результата алгоритма.

При символическом выполнении мы даем программе понять, что какие-то данные являются символами. Символ обозначает множество значений переменной из области определения. Программа должна знать, что будет выполняться при определенном значении символа. То есть мы формально запускаем программу на всехдопустимых тестовых значениях. Данная техника позволяет, например, понять, что для того, чтобы попасть в положение TRUE,необходимо, чтобы переменная A была больше 1, а B равна 'k'.

Ponce и IDA

Установка Ponce

Установить плагин очень просто: достаточно скопировать файлы, соответствующие установленной версии IDA из Git'a плагина (https://github.com/illera88/Ponce/tree/master/latest_builds) в папку "/plugins".

Использование Ponce

Я буду использовать простой пример на C++

Запускаем отладку приложения

При включенном отладчике идем в Edit->Plugins->Ponce и запускаем Ponce

При включении Ponce он предложит создать снапшот базы IDA, соглашаемся.

 Идем по адресу переменных, значения которых использует программа (2 раза кликаем)

В открывшемся окне находим переменную, копируем ее адрес.

Далее ПКМ->Symbolic->Symbolize_Memory. 

Пишем адрес переменной и ее размер, подтверждаем.

В логах IDA можно видеть что-то вроде такого: 

На каком-либо условии можно заметить, что мигает ответвление, которое будет выполнено при неизменном значении переменной.

Чтобы пойти в другую ветку, можно нажать ПКМ->SMT->Negate&Inject. 

При этом начнет мигать стрелка в другую ветку, а в логах IDA отобразится, какое значение должно быть у символической переменной, чтобы программа попала в данную ветвь. В данном примере нам предложили значение 0x04или 4.

Применив SMT ко второму условию, увидим, что предложенные значения такие: A=0x04, B=0x6B.

Попробуем запустить программу с предложенными значениями. Успех!

Снапшоты выполнения

Среди полезных функций Ponce стоит также отметить снапшот выполнения. Можно сохранить текущее состояние выполнения, и в любой момент вернуться именно к этому состоянию.

Итак?

Символическое выполнение сильно упрощает отладку программ, создание эксплойтов и решение задач на reverse в CTF. Ponce в связке с IDA -- это отличный инструмент, который буквально в несколько кликов делает крутые вещи, и делает все интерактивно.

Ссылки

https://github.com/illera88/Ponce https://www.cs.umd.edu/~mwh/se-tutorial/symbolic-exec.pdf