Символьное выполнение (Z3 SMT Solver)

Символьное выполнение (Z3 SMT Solver)

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

Обзор

Когда анализ помеченных данных (анализ заражения данных) находит путь от источника к приёмнику, путь может проходить через ветвления с противоречивыми условиями (например, if (x > 10) и далее if (x < 5) для той же переменной). Символьное выполнение проверяет реализуемость таких путей, кодируя условия ветвлений как ограничения Z3 и вызывая решатель.

Ключевые характеристики: - Опциональный компонент — корректно деградирует при отсутствии Z3 - Дополнительные затраты: ~20% времени, ~25% памяти - Максимум 20 ограничений на путь (настраивается) - Поддержка целочисленных сравнений, проверок NULL, простой арифметики

Установка

pip install z3-solver

Z3 включён в requirements.txt. Если Z3 недоступен во время выполнения, система записывает предупреждение и возвращает консервативные оценки (все пути считаются реализуемыми).

Архитектура

TaintPropagator (enable_symbolic_execution=True)
    │
    ├─ find_taint_paths()  →  необработанные пути
    │
    └─ PathConstraintTracker.filter_infeasible_paths()
        │
        ├─ _collect_constraints(start, end)
        │   └─ Обход рёбер CFG, извлечение условий из CDG
        │
        ├─ _parse_constraint_to_z3(constraint, z3_vars)
        │   └─ Преобразование "x > 100" → z3.Int('x') > 100
        │
        └─ z3.Solver().check()
            ├─ sat     → путь реализуем (достоверность 0.9)
            ├─ unsat   → путь нереализуем, ОТФИЛЬТРОВАТЬ (достоверность 0.95)
            └─ unknown → консервативно, сохранить путь (достоверность 0.4)

Справочник API

PathConstraint

@dataclass
class PathConstraint:
    node_id: int       # ID узла CPG (точка ветвления)
    condition: str     # Выражение условия (например, "x > 100")
    location: str      # Расположение файл:строка
    negated: bool      # True для else-ветки

PathConstraintTracker

class PathConstraintTracker:
    def __init__(self, cpg_service, max_constraints: int = 20):
        """
        Аргументы:
            cpg_service: экземпляр CPGQueryService для запросов к графу
            max_constraints: максимум ограничений на путь (по умолчанию: 20).
                Пути с большим числом ограничений считаются реализуемыми.
        """

    def is_path_feasible(self, start_node: int, end_node: int) -> Tuple[bool, float]:
        """
        Проверить реализуемость пути между двумя узлами.

        Возвращает:
            (is_feasible, confidence) — достоверность от 0.0 до 1.0
        """

    def filter_infeasible_paths(
        self, paths: List[Any], min_confidence: float = 0.8
    ) -> List[Any]:
        """
        Отфильтровать нереализуемые пути из списка.

        Аргументы:
            paths: список объектов путей (должны иметь .source_id и .sink_id)
            min_confidence: минимальная достоверность (по умолчанию: 0.8)

        Возвращает:
            Отфильтрованный список — только реализуемые пути
        """

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

Прямой вызов API

from src.analysis.dataflow.symbolic_execution import PathConstraintTracker

tracker = PathConstraintTracker(cpg_service, max_constraints=20)

# Проверка одного пути
is_feasible, confidence = tracker.is_path_feasible(node_123, node_456)
if not is_feasible and confidence > 0.9:
    print("Путь нереализуем — вероятно ложное срабатывание")

# Фильтрация пакета путей
feasible_paths = tracker.filter_infeasible_paths(all_paths, min_confidence=0.8)

Интеграция с анализом помеченных данных

from src.analysis.dataflow.taint import TaintPropagator

propagator = TaintPropagator(
    cpg_service,
    enable_symbolic_execution=True  # Включает Z3-фильтрацию
)

# Символьное выполнение применяется автоматически
paths = propagator.find_taint_paths(
    sources=["recv", "getenv"],
    sinks=["strcpy", "sprintf"]
)
# paths уже отфильтрованы — нереализуемые пути удалены

Поддерживаемые типы ограничений

Ограничение Пример Кодирование в Z3
Целочисленное сравнение x > 100 z3.Int('x') > 100
Равенство x == 0 z3.Int('x') == 0
Неравенство x != 5 z3.Int('x') != 5
Проверка NULL ptr == NULL z3.Int('ptr') == 0
Проверка nullptr ptr != nullptr z3.Int('ptr') != 0
Простая арифметика x + y > z z3.Int('x') + z3.Int('y') > z3.Int('z')

Не поддерживается: вызовы функций в условиях, сложные выражения, числа с плавающей точкой, строковые операции.

Уровни достоверности

Результат решателя Реализуем? Достоверность Действие
sat Да 0.9 Сохранить путь
unsat Нет 0.95 Удалить (ложное срабатывание)
unknown Предположительно да 0.4 Сохранить (консервативно)
Z3 недоступен Предположительно да 0.5 Сохранить (деградированный режим)
Слишком много ограничений Предположительно да 0.5 Сохранить (пропуск анализа)

Влияние на производительность

Метрика Без Z3 С Z3 Разница
Время анализа Базовое +20% Нагрузка решателя
Память Базовая +25% Внутренние структуры Z3
Ложные срабатывания ~12% ~5-8% Нереализуемые пути удалены

Ограничения

  1. Облегчённый анализ — не полноценный символьный исполнитель; отслеживает только условия ветвлений
  2. Только целые числа — нет поддержки чисел с плавающей точкой и строк
  3. Максимум 20 ограничений — длинные пути считаются реализуемыми
  4. Без межпроцедурного анализа — ограничения собираются в пределах одной функции
  5. Разбор по шаблонам — условия анализируются через регулярные выражения, не полный AST

Связанная документация

Модуль: src/analysis/dataflow/symbolic_execution.py Последнее обновление: февраль 2026