
Победитель конкурса плагинов IDA 2016! Символическое исполнение всего в один клик!
Ponce (произносится [ 'poN θe ] пон-тэй ) — это плагин для IDA Pro, который предоставляет пользователям возможность легко и интуитивно выполнять анализ заражения и символическое выполнение бинарных файлов. С помощью Ponce вы в один клик получаете всю мощь передовых методов символического выполнения. Полностью написан на C/C++.
Символическое выполнение — не новое понятие в сообществе по безопасности. Оно существует уже много лет, но только около 2015 года появились такие проекты с открытым исходным кодом, как Triton и Angr, призванные удовлетворить эту потребность. Несмотря на доступность этих проектов, конечным пользователям часто приходится самостоятельно реализовывать конкретные сценарии использования.
Мы решили эти потребности, создав Ponce — плагин для IDA, реализующий символическое выполнение и анализ заражения внутри самого популярного дизассемблера/отладчика для реверс-инженеров.
Ponce работает как с x86, так и с x64 бинарными файлами в любой версии IDA >= 7.0. Установка плагина сводится к копированию соответствующих файлов из последних сборок в папку plugins\ вашего каталога установки IDA.
Убедитесь, что вы используете бинарный файл Ponce, скомпилированный для вашей версии IDA, чтобы избежать несовместимости.
Ponce работает на Windows, Linux и OSX нативно!
Плагин запустится автоматически и проведёт вас через первоначальную настройку при первом запуске. Конфигурация будет сохранена в файл конфигурации, так что вам больше не придётся беспокоиться об окне настроек.
В следующей гифке показано использование автоматического заражения и то, как мы можем отрицать условие и инъецировать его в память во время отладки:
argv.elite, который был инъецирован в память, и, следовательно, достигаем кода Win.Исходный код crackme можно найти здесь

В этом примере мы видим использование движка заражения с cmake. Мы:
fread().
В следующем примере мы используем движок снимков:
fread().
Исходный код примера можно найти здесь
В этом разделе мы перечислим различные опции Ponce, а также сочетания клавиш:













Ponce использует фреймворк Triton для обеспечения семантики, анализа заражения и символического выполнения. Triton — это потрясающий проект с открытым исходным кодом, спонсируемый Quarkslab и поддерживаемый в основном Джонатаном Салваном с богатой библиотекой. Мы хотели бы поблагодарить и одобрить работу Джонатана над Triton. Вы лучший! :)
Начиная с Ponce v0.3 мы перевели процесс сборки на использование CMake. Это позволило унифицировать способ настройки и сборки для Linux, Windows и OSX. Теперь мы поддерживаем отображение обратной связи в псевдокоде о символических или заражённых инструкциях. Для работы этой функции необходимо добавить hexrays.hpp в папку include вашего IDA SDK. hexrays.hpp находится в plugins/hexrays_sdk/ по пути установки IDA. Если вы не приобрели декомпилятор hex-rays, вы всё равно можете собрать Ponce, используя -DBUILD_HEXRAYS_SUPPORT=OFF. Мы используем Github Actions в качестве среды CI. Проверьте файлы действий, если хотите понять, как происходит процесс сборки.
Хуан Понсе де Леон (1474 – июль 1521) был испанским исследователем и конкистадором. Он открыл Флориду в Соединённых Штатах. Плагин IDA поможет вам открывать, исследовать и, надеюсь, завоёвывать различные пути в бинарном файле.
Да, вы можете использовать Ponce нативно в IDA для Windows или удалённо подключиться к Linux или OS X и использовать его. В следующей версии Ponce мы добавим нативную поддержку для версий IDA на Linux и OS X.
В наших тестах мы достигаем обработки 3000 инструкций в секунду. Мы планируем использовать трейсер PIN, который предлагает IDA, для увеличения скорости.
Откройте issue, мы решим это как можно скорее ;)
Конечно! Пожалуйста, делайте pull request’ы и работайте над открытыми issue. Мы отплатим вам пивом за помощь ;)
Конколическое выполнение и Ponce имеют некоторые проблемы:
Символическая загрузка/запись в память: когда индекс, используемый для чтения значения памяти, является символическим, как в x = aray[symbolic_index], возникают проблемы, которые могут привести к потере отслеживания заражённого/символизированного управляемого пользователем ввода.
Triton не очень хорошо работает с инструкциями с плавающей точкой.
Конколическое выполнение анализирует только выполненные инструкции. Это означает, что символическое отслеживание теряется в таких случаях, как следующий:
int check(char myinput) // Input is symbolic/tainted
{
int flag = 0;
if (myinput == 'A') //This condition is symbolic/tainted
flag = 1
else
flag =- 1;
return flag; // flag is not symbolic/tainted!
}