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

pip install z3-solver

TaintPropagator (enable_symbolic_execution=True)
    │
    ├─ find_taint_paths()  →  необработанные пути
    │
    └─ PathConstraintTracker.filter_infeasible_paths()
        │
        ├─ _collect_constraints(start, end)
        │   ├─ Обход рёбер CFG, извлечение условий из CDG
        │   └─ _determine_branch_direction() через преемников CFG
        │
        ├─ _parse_condition(code, z3_vars, state)
        │   └─ Рекурсивный спуск: or → and → not → comparison → additive → atom
        │       ├─ Переменные: z3.Int('x')
        │       ├─ Функции: strlen(s) → новая Int с ограничениями домена
        │       └─ NULL: z3.Bool('ptr_is_null')
        │
        └─ z3.Solver().check()  (с таймаутом)
            ├─ sat     → путь реализуем (достоверность 0.9)
            ├─ unsat   → путь нереализуем, ОТФИЛЬТРОВАТЬ (достоверность 0.95)
            └─ unknown → консервативно, сохранить путь (достоверность 0.4)

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

@dataclass
class SymbolicExecutionConfig:
    enabled: bool = True
    max_constraints: int = 20
    solver_timeout_ms: int = 500        # Запросы QF_LIA
    solver_timeout_uf_ms: int = 2000    # Запросы с неинтерпретируемыми функциями
    max_parse_depth: int = 10           # Ограничение глубины рекурсивного спуска
    enable_function_models: bool = True # Модели strlen, sizeof, len
    enable_arithmetic: bool = True      # +, -, * в условиях

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

    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: список объектов путей (должны иметь атрибут .path_nodes —
                   список ID узлов; первый элемент = источник, последний = приёмник)
            min_confidence: минимальная достоверность (по умолчанию: 0.8)

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

    def get_statistics(self) -> Dict[str, Any]:
        """
        Получить статистику решателя.

        Возвращает:
            Словарь с ключами:
            - z3_available (bool): установлен ли Z3
            - max_constraints (int): максимум ограничений на путь
            - solver_timeout_ms (int): таймаут LIA-запросов
            - solver_timeout_uf_ms (int): таймаут UF-запросов
            - enable_function_models (bool): модели функций включены
            - enable_arithmetic (bool): арифметика включена
            - supported_functions (list): известные модели функций
        """

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_analysis import TaintPropagator

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

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

symbolic_execution:
  enabled: true
  max_constraints: 20
  solver_timeout_ms: 500
  solver_timeout_uf_ms: 2000
  max_parse_depth: 10
  enable_function_models: true
  enable_arithmetic: true