Примечание: некоторые старые ссылки могут содержать предыдущее название проекта.
Что это такое
Исполняемый набор регрессионных тестов безопасности, моделирующий действия злоумышленника:- Для каждого утверждения предусмотрена запускаемая проверка модели в конечном пространстве состояний.
- Для многих утверждений предусмотрена парная негативная модель, которая создаёт трассу контрпримера для реалистичного класса ошибок.
Где находятся модели
Модели поддерживаются в отдельном репозитории: vignesh07/openclaw-formal-models.В настоящее время этот репозиторий недоступен (на момент написания GitHub возвращает “Repository not found”). Если он по-прежнему недоступен для вас, уточните его текущее расположение в каналах сопровождающих OpenClaw, прежде чем предполагать, что модели были удалены.
Ограничения
- Это модели, а не полная реализация на TypeScript, поэтому модель и код могут расходиться.
- Результаты ограничены пространством состояний, исследуемым TLC. Успешный результат не гарантирует безопасность за пределами смоделированных допущений и границ.
- Некоторые утверждения основаны на явных допущениях о среде (например, о правильном развёртывании и корректных входных данных конфигурации).
Воспроизведение результатов
Клонируйте репозиторий моделей и запустите TLC:Утверждения и цели
Доступность Gateway и неверная конфигурация открытого Gateway
Утверждение: привязка не только к loopback-интерфейсу без аутентификации может сделать возможной удалённую компрометацию и увеличить поверхность воздействия; согласно допущениям модели, токен или пароль блокирует неаутентифицированных злоумышленников.
См. также
docs/gateway-exposure-matrix.md в репозитории моделей.
Конвейер выполнения команд Node (возможность с наивысшим риском)
Утверждение:exec host=node требует (а) списка разрешённых команд Node вместе с объявленными командами и (б) оперативного подтверждения, если оно настроено; в модели подтверждения токенизируются для предотвращения повторного воспроизведения.
Хранилище сопряжений (ограничение личных сообщений)
Утверждение: запросы на сопряжение соблюдают TTL и ограничения количества ожидающих запросов.Ограничение входящих сообщений (упоминания и обход управляющими командами)
Утверждение: в групповых контекстах, где требуется упоминание, неавторизованная управляющая команда не может обойти проверку упоминания.Маршрутизация и изоляция ключей сеансов
Утверждение: личные сообщения от разных собеседников не объединяются в один сеанс, если они не были явно связаны или настроены соответствующим образом.Модели v1++: параллельность, повторные попытки и корректность трассировки
Последующие модели, повышающие точность представления реальных режимов отказа: неатомарных обновлений, повторных попыток и разветвления сообщений.Параллельность и идемпотентность хранилища сопряжений
Утверждение: хранилище сопряжений обеспечиваетMaxPending и идемпотентность даже при чередовании операций — последовательность «проверить, затем записать» должна быть атомарной или защищённой блокировкой, а обновление не должно создавать дубликаты. В частности, параллельные запросы не могут превысить MaxPending для канала, а повторные запросы или обновления для одного и того же (channel, sender) не создают дублирующиеся активные строки ожидания.
Корреляция трассировки и идемпотентность входящих сообщений
Утверждение: при приёме сохраняется корреляция трассировки при разветвлении и обеспечивается идемпотентность при повторных попытках со стороны провайдера. Когда одно внешнее событие преобразуется в несколько внутренних сообщений, каждая часть сохраняет одну и ту же идентичность трассы и события; повторные попытки не приводят к двойной обработке; если идентификаторы событий провайдера отсутствуют, дедупликация использует безопасный резервный ключ (например, идентификатор трассы), чтобы не отбрасывать разные события.Приоритет dmScope и identityLinks при маршрутизации
Утверждение: маршрутизация по умолчанию сохраняет изоляцию сеансов личных сообщений и объединяет их только при явной настройке с учётом приоритета каналов и связей идентичностей. Специфичные для канала переопределенияdmScope имеют приоритет над глобальными значениями по умолчанию; identityLinks объединяют сеансы только внутри явно связанных групп, но не между не связанными друг с другом собеседниками.