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

Формальные модели безопасности OpenClaw (на сегодняшний день TLA+/TLC) предоставляют проверенный машинным способом аргумент в пользу того, что конкретные пути с наивысшим риском — авторизация, изоляция сеансов, ограничение доступа к инструментам и безопасность при неверной конфигурации — обеспечивают соблюдение предусмотренной политики при явно указанных допущениях.

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

Что это такое

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

• Для каждого утверждения предусмотрена запускаемая проверка модели в конечном пространстве состояний.
• Для многих утверждений предусмотрена парная негативная модель, которая создаёт трассу контрпримера для реалистичного класса ошибок.

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

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

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

Ограничения

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

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

Клонируйте репозиторий моделей и запустите TLC:

git clone https://github.com/vignesh07/openclaw-formal-modelscd openclaw-formal-models # Требуется Java 11+ (TLC работает на JVM).# Репозиторий содержит закреплённую версию tla2tools.jar и предоставляет bin/tlc, а также цели Make. make <target>

Интеграции с CI этого репозитория пока нет; в будущей версии можно добавить запуск моделей в CI с общедоступными артефактами (трассами контрпримеров, журналами запусков) или размещённый рабочий процесс «запустить эту модель» для небольших ограниченных проверок.

Утверждения и цели

Доступность Gateway и неверная конфигурация открытого Gateway

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

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

Конвейер выполнения команд Node (возможность с наивысшим риском)

Утверждение: exec host=node требует (а) списка разрешённых команд Node вместе с объявленными командами и (б) оперативного подтверждения, если оно настроено; в модели подтверждения токенизируются для предотвращения повторного воспроизведения.

Хранилище сопряжений (ограничение личных сообщений)

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

Ограничение входящих сообщений (упоминания и обход управляющими командами)

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

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

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

Модели v1++: параллельность, повторные попытки и корректность трассировки

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

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

Утверждение: хранилище сопряжений обеспечивает MaxPending и идемпотентность даже при чередовании операций — последовательность «проверить, затем записать» должна быть атомарной или защищённой блокировкой, а обновление не должно создавать дубликаты. В частности, параллельные запросы не могут превысить MaxPending для канала, а повторные запросы или обновления для одного и того же (channel, sender) не создают дублирующиеся активные строки ожидания.

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

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

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

Утверждение: маршрутизация по умолчанию сохраняет изоляцию сеансов личных сообщений и объединяет их только при явной настройке с учётом приоритета каналов и связей идентичностей. Специфичные для канала переопределения dmScope имеют приоритет над глобальными значениями по умолчанию; identityLinks объединяют сеансы только внутри явно связанных групп, но не между не связанными друг с другом собеседниками.

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

• Модель угроз
• Участие в разработке модели угроз
• Реагирование на инциденты