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

Эта страница отслеживает формальные модели безопасности 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>

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

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

  • Зелёные запуски:
    • 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

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

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

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

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

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

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

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

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

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

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

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

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

  • Красные (ожидаемые):

    • make pairing-race-negative (неатомарная гонка начало/коммит лимита)
    • 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
← Назад к документации