Symbolic execution

Символьное исполнение (symbolic execution) — метод анализа программ, при котором вместо конкретных входных данных используются символьные значения. Программа превращается в систему логических формул, связывающих эти значения с результатом. Это позволяет рассуждать сразу о многих случаях работы программы, а не перебирать их по одному.

Метод важен для поиска ошибок и уязвимостей, которых невозможно обнаружить обычным тестированием из-за невообразимого числа комбинаций входных данных. Он лежит в основе современных инструментов автоматического поиска багов, например, в фаззинге и генерации тестов.

Как это работает на интуитивном уровне? Представьте, что вы идёте по лабиринту, где в каждой точке развилка с условием. Символьное исполнение проходит все развилки одновременно, запоминая условия пути. Когда условие противоречиво, путь отбрасывается. Для достижимого пути строится формула, из которой подбираются конкретные числа, приводящие выполнение в нужную точку. Так можно достоверно определить, выполнится ли фрагмент кода и что он сделает.

Пример: в коде просмотрщика PDF есть функция, копирующая данные из файла в буфер. Символьный исполнитель анализирует её, строя формулы для размера данных и границ буфера. Если есть размер, при котором запись выйдет за границу, он найдёт соответствующие значения и сформирует PDF-файл, вызывающий переполнение буфера. Этот файл затем используют, чтобы убедиться в уязвимости.

Итог: символьное исполнение — мощный инструмент для глубокого анализа кода, но он сталкивается с «взрывом путей», когда число ветвлений становится огромным. Поэтому на практике его применяют локально, для критичных участков. Тем не менее это незаменимый помощник в поиске трудноуловимых ошибок и уязвимостей.