6 строк кода вместо 4 часов реверса: как символьное исполнение ломает CTF-таски

На CSAW CTF 2015 задача «wyvern» из категории Reversing 500 содержала бинарь с десятками вложенных проверок ввода. Ручной реверс в Ghidra — часы работы. Скрипт на 6 строках angr решил её за 15 минут. Автоматически сгенерировал входные данные, удовлетворяющие каждому условию. Не магия, а математика.

🔬 Суть подхода простая. Вместо конкретных значений на вход подаются символические переменные — абстракции, которые могут быть чем угодно. На каждом ветвлении (if, switch, граница цикла) движок создаёт два состояния и накапливает ограничения. В целевой точке — например, при вызове puts("Access granted") — всё передаётся SMT-солверу Z3, который решает систему уравнений и возвращает конкретный ввод. Никакого перебора — чистая математическая задача.

Если целевой точкой назначить вызов strcpy с контролируемым буфером, солвер найдёт ввод, приводящий к buffer overflow. Это уже не CTF — это автоматический поиск уязвимостей в реальных бинарях.

⚡️ Но есть нюансы. Главный враг — path explosion. Каждое ветвление удваивает число состояний. Цикл на 1000 итераций с условием внутри — теоретически 2^1000 путей. А если проверка включает SHA-256 или другую криптографию, Z3 просто не решит constraints за разумное время. Поэтому символьное исполнение — фильтр, а не серебряная пуля.

Теперь к выбору инструмента. Три основных фреймворка:

• angr — самый зрелый и живой. Поддерживает x86/x64, ARM, MIPS. Еженедельные коммиты, богатая документация, десятки готовых примеров. На FlareOn 2015 Challenge 5 — решение за 2 минуты 10 секунд. ASIS CTF Finals 2015 — 3.6 секунды. Лучший выбор для CTF, пентеста, автоматизации рутинного реверса.

• Manticore — от Trail of Bits. Уникальная фишка — поддержка смарт-контрактов Ethereum. Помог обнаружить CVE-2020-5232 (CVSS 8.7) в Ethereum Name Service. Но разработка фактически остановилась — начинать новый проект на нём рискованно.

• Triton — заточен под динамический анализ. Работает не с абстрактным исполнением всех путей, а с конкретной трассой. Идеален для деобфускации, снятия MBA-выражений, точечного анализа конкретного пути исполнения.

🎯 Простое правило выбора: нужен автоматический обход всех путей — angr. Аудит смарт-контрактов — Manticore (с оговорками). Работа с конкретной трассой и деобфускация — Triton.

В полной статье — рабочий код для каждого фреймворка, decision tree выбора инструмента и честный разбор граничных случаев, где символьное исполнение ломается.

https://codeby.net/threads/simvol-noye-ispolneniye-dlya-poiska-uyazvimostei-angr-manticore-i-triton-na-praktike.92962/