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

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

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

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

• Зелёные:
  • 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 трассировки), чтобы не отбрасывать различные события.
• Зелёные:
  • 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

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

• Переопределения dmScope для конкретного канала должны иметь приоритет над глобальными значениями по умолчанию.
• Связи идентификаторов должны объединять сессии только внутри явно связанных групп, а не между несвязанными участниками.
• Зелёные:
  • make routing-precedence
  • make routing-identitylinks
• Красные (ожидаемо):
  • make routing-precedence-negative
  • make routing-identitylinks-negative

TailscaleREADME