> ## Documentation Index
> Fetch the complete documentation index at: https://docs2.openclaw.ai/llms.txt
> Use this file to discover all available pages before exploring further.

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

Эта страница отслеживает **формальные модели безопасности** OpenClaw (сейчас TLA+/TLC; далее по мере необходимости).

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

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

**Что это такое (сейчас):** исполняемый, ориентированный на атакующего **набор регрессионных тестов безопасности**:

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

**Чем это не является (пока):** доказательством того, что «OpenClaw безопасен во всех отношениях» или что полная реализация на TypeScript корректна.

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

Модели поддерживаются в отдельном репозитории: [vignesh07/openclaw-formal-models](https://github.com/vignesh07/openclaw-formal-models).

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

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

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

Сегодня результаты воспроизводятся путем локального клонирования репозитория с моделями и запуска TLC (см. ниже). В будущей итерации можно добавить:

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

Начало работы:

```bash theme={"theme":{"light":"min-light","dark":"min-dark"}}
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`

### Приоритет routing dmScope + identityLinks

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

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

* Переопределения dmScope для конкретного канала должны иметь приоритет над глобальными значениями по умолчанию.

* identityLinks должны схлопывать только внутри явно связанных групп, а не между несвязанными собеседниками.

* Зеленые:
  * `make routing-precedence`
  * `make routing-identitylinks`

* Красные (ожидаемые):
  * `make routing-precedence-negative`
  * `make routing-identitylinks-negative`

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

* [Модель угроз](/ru/security/THREAT-MODEL-ATLAS)
* [Участие в разработке модели угроз](/ru/security/CONTRIBUTING-THREAT-MODEL)