Формальная верификация (Formal Verification) (модели безопасности)

Эта страница отслеживает формальные модели безопасности OpenClaw (сегодня TLA+/TLC; по мере необходимости будет больше).

Примечание: некоторые старые ссылки могут относиться к предыдущему названию проекта.

Цель (Полярная звезда): предоставить проверенный машиной аргумент, что OpenClaw обеспечивает свою предполагаемую политику безопасности (авторизация, изоляция сессий, ограничение инструментов и безопасность неправильной конфигурации) при явных предположениях.

Что это есть (сегодня)

Исполняемый набор регрессии безопасности, управляемый атакующим:

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

Что это НЕ есть (пока)

Доказательство того, что "OpenClaw безопасен во всех отношениях" или что полная реализация TypeScript корректна.

Где находятся модели

Модели поддерживаются в отдельном репозитории: vignesh07/openclaw-formal-models.

Важные предостережения

  • Это модели, а не полная реализация TypeScript. Возможно расхождение между моделью и кодом.
  • Результаты ограничены пространством состояний, исследованным TLC; "зеленый" не означает безопасность за пределами смоделированных предположений и границ.
  • Некоторые утверждения полагаются на явные предположения окружения (например, правильное развертывание, правильные входные данные конфигурации).

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

Сегодня результаты воспроизводятся путем клонирования репозитория моделей локально и запуска TLC (см. ниже). Будущая итерация может предложить:

  • CI-запускаемые модели с публичными артефактами (трассировки контрпримеров, логи запусков)
  • размещенный рабочий процесс "запустить эту модель" для небольших ограниченных проверок

Начало работы:

git clone https://github.com/vignesh07/openclaw-formal-models
cd openclaw-formal-models

# Требуется Java 11+ (TLC работает на JVM).
# Репозиторий содержит закрепленный `tla2tools.jar` (инструменты TLA+) и предоставляет `bin/tlc` + цели Make.

make <target>

Экспозиция шлюза и неправильная конфигурация открытого шлюза

Утверждение: привязка за пределами обратной петли без аутентификации может сделать возможной удаленную компрометацию / увеличивает экспозицию; токен/пароль блокирует неавторизованных атакующих (по предположениям модели).

  • Зеленые запуски:
    • make gateway-exposure-v2
    • make gateway-exposure-v2-protected
  • Красный (ожидается):
    • make gateway-exposure-v2-negative

См. также: docs/gateway-exposure-matrix.md в репозитории моделей.

Конвейер Nodes.run (самая рискованная возможность)

Утверждение: nodes.run требует (a) список разрешенных команд узла плюс объявленные команды и (b) живое одобрение при настройке; одобрения токенизированы для предотвращения повторного воспроизведения (в модели).

  • Зеленые запуски:
    • make nodes-pipeline
    • make approvals-token
  • Красный (ожидается):
    • make nodes-pipeline-negative
    • make approvals-token-negative

Хранилище сопряжения (ограничение DM)

Утверждение: запросы на сопряжение соблюдают TTL и лимиты ожидающих запросов.

  • Зеленые запуски:
    • make pairing
    • make pairing-cap
  • Красный (ожидается):
    • make pairing-negative
    • make pairing-cap-negative

Ограничение входа (упоминания + обход команды управления)

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

  • Зеленый:
    • make ingress-gating
  • Красный (ожидается):
    • make ingress-gating-negative

Маршрутизация/изоляция ключей сессий

Утверждение: личные сообщения от разных пиров не сворачиваются в одну и ту же сессию, если явно не связаны/настроены.

  • Зеленый:
    • make routing-isolation
  • Красный (ожидается):
    • make routing-isolation-negative

v1++: дополнительные ограниченные модели (параллелизм, повторы, корректность трассировки)

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

Параллелизм / идемпотентность хранилища сопряжения

Утверждение: хранилище сопряжения должно обеспечивать MaxPending и идемпотентность даже при чередовании (т.е. "проверка-затем-запись" должна быть атомарной/заблокированной; обновление не должно создавать дубликаты).

Что это означает:

  • При параллельных запросах вы не можете превысить MaxPending для канала.

  • Повторяющиеся запросы/обновления для одного и того же (канал, отправитель) не должны создавать дублирующиеся активные ожидающие строки.

  • Зеленые запуски:

    • make pairing-race (атомарная/заблокированная проверка cap)
    • make pairing-idempotency
    • make pairing-refresh
    • make pairing-refresh-race

  • Красный (ожидается):

    • make pairing-race-negative (неатомарная гонка cap begin/commit)
    • make pairing-idempotency-negative
    • make pairing-refresh-negative
    • make pairing-refresh-race-negative

Корреляция трассировки входа / идемпотентность

Утверждение: прием должен сохранять корреляцию трассировки при разветвлении и быть идемпотентным при повторах провайдера.

Что это означает:

  • Когда одно внешнее событие становится несколькими внутренними сообщениями, каждая часть сохраняет одну и ту же идентичность трассировки/события.

  • Повторы не приводят к двойной обработке.

  • Если ID событий провайдера отсутствуют, дедупликация возвращается к безопасному ключу (например, ID трассировки), чтобы избежать удаления различных событий.

  • Зеленый:

    • make ingress-trace
    • make ingress-trace2
    • make ingress-idempotency
    • make ingress-dedupe-fallback

  • Красный (ожидается):

    • make ingress-trace-negative
    • make ingress-trace2-negative
    • make ingress-idempotency-negative
    • make ingress-dedupe-fallback-negative

Приоритет dmScope маршрутизации + identityLinks

Утверждение: маршрутизация должна сохранять изоляцию DM-сессий по умолчанию и сворачивать сессии только при явной конфигурации (приоритет канала + ссылки идентичности).

Что это означает:

  • Переопределения dmScope для конкретных каналов должны побеждать глобальные настройки по умолчанию.

  • identityLinks должны сворачиваться только в пределах явно связанных групп, а не между несвязанными пирами.

  • Зеленый:

    • make routing-precedence
    • make routing-identitylinks

  • Красный (ожидается):

    • make routing-precedence-negative
    • make routing-identitylinks-negative
← Назад к документации