Перейти к основному содержанию
Эта страница отслеживает формальные модели безопасности OpenClaw (сейчас TLA+/TLC; далее по мере необходимости).
Примечание: некоторые старые ссылки могут указывать на прежнее название проекта.
Цель (путеводная звезда): предоставить машинно проверенный аргумент, что OpenClaw обеспечивает свою заданную политику безопасности (авторизация, изоляция сеансов, ограничение инструментов и безопасность при неправильной конфигурации) при явно заданных предположениях. Что это такое (сейчас): исполняемый, ориентированный на атакующего набор регрессионных тестов безопасности:
  • Для каждого утверждения есть запускаемая проверка модели на конечном пространстве состояний.
  • У многих утверждений есть парная негативная модель, которая создает трассу контрпримера для реалистичного класса ошибок.
Чем это не является (пока): доказательством того, что «OpenClaw безопасен во всех отношениях» или что полная реализация на TypeScript корректна.

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

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

​
Важные оговорки

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

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

Сегодня результаты воспроизводятся путем локального клонирования репозитория с моделями и запуска TLC (см. ниже). В будущей итерации можно добавить:
  • модели, запускаемые в CI, с публичными артефактами (трассы контрпримеров, журналы запусков)
  • размещенный workflow «запустить эту модель» для небольших ограниченных проверок
Начало работы: 
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>

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

Утверждение: привязка за пределами local loopback без аутентификации может сделать удаленную компрометацию возможной / увеличивает экспозицию; токен/пароль блокирует неаутентифицированных атакующих (согласно предположениям модели).
  • Зеленые запуски:
    • make gateway-exposure-v2
    • make gateway-exposure-v2-protected
  • Красные (ожидаемые):
    • make gateway-exposure-v2-negative
См. также: docs/gateway-exposure-matrix.md в репозитории моделей.

​
Конвейер exec Node (возможность с наивысшим риском)

Утверждение: exec host=node требует (a) списка разрешенных команд Node плюс объявленных команд и (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 (гонка ограничения begin/commit при неатомарности)
    • make pairing-idempotency-negative
    • make pairing-refresh-negative
    • make pairing-refresh-race-negative

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

Утверждение: прием входящих данных должен сохранять корреляцию трасс при разветвлении и быть идемпотентным при повторах провайдера. Что это означает:
  • Когда одно внешнее событие превращается в несколько внутренних сообщений, каждая часть сохраняет ту же идентичность трассы/события.
  • Повторы не приводят к двойной обработке.
  • Если идентификаторы событий провайдера отсутствуют, дедупликация возвращается к безопасному ключу (например, trace 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
Утверждение: маршрутизация должна по умолчанию сохранять изоляцию сеансов DM и схлопывать сеансы только при явной настройке (приоритет канала + ссылки идентичностей). Что это означает:
  • Переопределения dmScope для конкретного канала должны иметь приоритет над глобальными значениями по умолчанию.
  • identityLinks должны схлопывать только внутри явно связанных групп, а не между несвязанными собеседниками.
  • Зеленые:
    • make routing-precedence
    • make routing-identitylinks
  • Красные (ожидаемые):
    • make routing-precedence-negative
    • make routing-identitylinks-negative

​
Связанные материалы