У вашего набора тестов 94% покрытия и ноль падений. Движок символического исполнения находит краш в вашем коде менее чем за три секунды.

Тесты не сломаны. Метрика покрытия не врёт. Проблема в том, что тестирование проверяет поведение в конкретных точках. Символическое исполнение проверяет поведение целыми регионами пространства входных данных. Не имеет значения, сколько примеров вы напишете, если баг живёт в промежутке между двумя из них.

Что на самом деле делает символическое исполнение

Символическое исполнение — это техника анализа программ, которая запускает ваш код на символических переменных вместо конкретных значений. Обычный тест передаёт x = 5 в функцию. Движок символического исполнения передаёт x = α, где α представляет каждое возможное целое число.

По мере выполнения кода движок отслеживает ограничения. Когда он попадает на ветвление вроде if (x > 0), он не выбирает направление. Он разветвляет исполнение. Один путь несёт ограничение α > 0. Другой — α ≤ 0. Оба пути продолжаются независимо.

Когда путь достигает assertion, обращения к памяти или потенциального места краша, движок задаёт SMT solver простой вопрос: «Существует ли какое-либо значение α, которое удовлетворяет всем ограничениям на этом пути и также нарушает это свойство безопасности?» Если solver отвечает да, он выдаёт конкретный контрпример. Теперь у вас есть конкретный ввод, который вызывает баг, тест для которого вы никогда не писали.

Баг, который ваши юнит-тесты не поймают

Рассмотрим функцию, которая проверяет границы массива перед копированием:

int copy_slice(const char *src, size_t src_len,
               size_t offset, size_t count) {
    if (offset > src_len) return -1;
    if (count > 1024) return -1;

    size_t end = offset + count;
    if (end > src_len) return -1;

    char dst[1024];
    memcpy(dst, src + offset, count);
    return 0;
}

Ваш набор тестов выглядит разумно:

void test_copy_slice_normal() {
    assert(copy_slice("hello", 5, 1, 3) == 0);
}

void test_copy_slice_too_long() {
    assert(copy_slice("hi", 2, 0, 1025) == -1);
}

void test_copy_slice_bad_offset() {
    assert(copy_slice("hi", 2, 5, 1) == -1);
}

Всё зелёно. Но offset и count — это size_t, беззнаковые целые. На 64-битной системе offset + count может обернуться к маленькому числу, если оба велики. Если offset = 0xFFFFFFFFFFFFFFFF и count = 1, то end = 0, что не больше src_len. Проверка границ проходит. memcpy читает по невалидному адресу.

Ни один разумный разработчик не напишет тест-кейс с offset = 2^64 - 1. Пространство входных данных невообразимо велико. Символическое исполнение не требует от вас угадывать плохой ввод. Оно исследует путь, где происходит оборачивание, и просит solver найти значения, удовлетворяющие ограничению end ≤ src_len, при этом offset + count переполняется. Solver возвращает контрпример за миллисекунды.

Как движок исследует пути

Основной механизм — сбор ограничений и разветвление путей. Каждое условное выражение в вашем коде становится точкой ветвления. Движок поддерживает ограничение пути — булеву формулу, представляющую все условия, которые должны быть истинны, чтобы исполнение достигло текущей точки.

На каждом ветвлении движок запрашивает solver:

  1. Выполнимо ли текущее ограничение пути плюс условие true-ветви?
  2. Выполнимо ли текущее ограничение пути плюс условие false-ветви?

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

Когда путь достигает краша, выхода за границы или провалившегося assertion, движок просит solver выдать удовлетворяющее назначение символических входов под текущим ограничением пути. Это назначение — ваш ввод, вызывающий баг.

Вы можете увидеть шаг решения ограничений напрямую с Z3, SMT solver’ом, который питает многие движки символического исполнения:

from z3 import Solver, BitVec, UGT, ULT, ULE, simplify

solver = Solver()

# Model 32-bit unsigned size_t values
offset = BitVec('offset', 32)
count = BitVec('count', 32)
src_len = BitVec('src_len', 32)

# Path constraints: offset <= src_len, count <= 1024
solver.add(ULE(offset, src_len))
solver.add(ULE(count, 1024))

# We want to find a case where offset + count wraps around
# and the end check passes incorrectly
end = offset + count
solver.add(UGT(end, src_len))  # This should trigger the return -1

# But what if we look for the overflow case where end wraps?
solver2 = Solver()
solver2.add(ULE(offset, src_len))
solver2.add(ULE(count, 1024))
solver2.add(ULT(offset + count, offset))  # unsigned overflow
solver2.add(ULE(offset + count, src_len))  # bogus check passes

if solver2.check() == solver2.sat:
    model = solver2.model()
    print(f"offset={model[offset]}, count={model[count]}")
    # offset=4294967295, count=1 on a 32-bit model

Solver возвращает конкретные значения, удовлетворяющие ограничению переполнения. Это математическое ядро символического исполнения. Движок делает это автоматически через каждое ветвление в вашей программе.

Трейдоффы, которые не позволяют ему заменить ваш набор тестов

Символическое исполнение не бесплатно. Есть три издержки, которые ограничивают, где оно практично.

Взрыв путей. Каждый оператор if удваивает число путей. Функция с 20 независимыми ветвлениями имеет более миллиона путей. Большинство движков сдаются после таймаута или исчерпания бюджета путей. Циклы усугубляют это. Цикл, который итерируется символически по неограниченному диапазону, создаёт бесконечно много путей. Движки обычно разворачивают циклы фиксированное число раз и двигаются дальше.

Внешнее состояние и системные вызовы. Символическое исполнение лучше всего работает на чистых функциях. Когда ваш код читает из файла, делает сетевой запрос или запрашивает базу данных, движок понятия не имеет, какое значение вернётся. Некоторые инструменты моделируют распространённые вызовы библиотек эвристически. Другие требуют от вас писать mock-модели. Это утомительно и чревато ошибками.

Таймауты solver’а. Формулы ограничений для реального кода сложны. Массивы, битовые векторы, арифметика с плавающей точкой и нелинейная математика могут втолкнуть SMT solver в экспоненциальное время. Путь, который занимает микросекунды при конкретном исполнении, может занять минуты при символическом. Движки отбрасывают эти пути и помечают их как нерешённые.

Из-за этих ограничений символическое исполнение — это дополнение к тестированию, а не замена. Оно находит глубокие угловые случаи. Ваши тесты проверяют распространённые случаи и интеграционное поведение.

Три способа попробовать это на реальном коде

Вам не нужна степень PhD, чтобы запускать символическое исполнение. Современные инструменты скрывают большую часть сложности.

Для C/C++: KLEE. KLEE — это классический open-source движок символического исполнения, построенный на LLVM. Вы компилируете свой код в LLVM bitcode с помощью clang -emit-llvm, затем запускаете klee на результате. KLEE находил серьёзные баги в GNU coreutils, SQLite и других широко используемых codebase’ах на C.

clang -emit-llvm -c -g copy_slice.c -o copy_slice.bc
klee --max-time=60 copy_slice.bc

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

Для Python и бинарников: angr. angr — это Python-фреймворк для символического исполнения, бинарного анализа и реверс-инжиниринга. Он работает на скомпилированных бинарниках, так что вам не нужен исходный код. Вы пишете Python-скрипт для настройки символических регистров и памяти, затем даёте angr исследовать.

import angr

proj = angr.Project("./copy_slice")
state = proj.factory.entry_state()
sm = proj.factory.simulation_manager(state)
sm.explore(find=lambda s: b"crash" in s.posix.dumps(1))

angr медленнее KLEE, но работает с реальными бинарниками со всеми их запутанными соглашениями о вызовах и зависимостями библиотек.

Для Rust: Kani. Kani — это верификатор для Rust, построенный на CBMC. Вы аннотируете функцию с помощью #[kani::proof] и запускаете cargo kani. Он проверяет арифметические переполнения, выход за границы и провалы assertion’ов, используя под капотом символическое исполнение.

#[kani::proof]
fn check_copy_slice() {
    let src = kani::any_slice::<u8, 1024>();
    let offset: usize = kani::any();
    let count: usize = kani::any();
    kani::assume(count <= 1024);
    let _ = copy_slice(src, src.len(), offset, count);
}

Kani — это самый простой вход, если вы уже в экосистеме Rust. Он интегрируется с cargo и выдаёт трейсы ошибок в знакомом формате.

Часто задаваемые вопросы

Заменяет ли символическое исполнение фаззинг?

Нет. Фаззинг генерирует случайные входные данные и наблюдает за крашами. Символическое исполнение рассуждает о путях и находит входные данные, удовлетворяющие конкретным ограничениям. Фаззинг масштабируется на большие программы и долгие прогоны. Символическое исполнение находит более глубокие баги в меньших регионах. Две техники хорошо работают вместе. Инструменты вроде Driller и QSYM комбинируют их, используя фаззинг для покрытия и символическое исполнение для труднодоступных ветвей.

Может ли символическое исполнение доказать, что в моём коде нет багов?

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

Как долго это работает?

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

Начните с одной функции

Вам не нужно символически исполнять весь codebase. Выберите одну функцию, где баг причинил бы боль. Парсер. Проверку авторизации. Копирование буфера.

Напишите harness для KLEE, скрипт для angr или proof для Kani. Запустите. Посмотрите, как он находит ввод, для которого вы бы никогда не написали тест. Исправьте баг. Спите спокойнее.

Цель — не заменить ваши тесты. Цель — перестать притворяться, что 94% покрытия означают 94% безопасности. Символическое исполнение находит пробелы. Ваши тесты никогда не найдут.