> ## 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 безопасен во всех отношениях, и оно не проверяет полную реализацию на TypeScript.

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

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

> [!NOTE]
>
> В настоящее время этот репозиторий недоступен (на момент написания GitHub возвращает "Repository not found"). Если он по-прежнему недоступен для вас, уточните его текущее расположение в каналах сопровождающих OpenClaw, прежде чем предполагать, что модели были удалены.

## Ограничения

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

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

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

```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 и предоставляет bin/tlc, а также цели Make.

make <target>
```

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

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

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

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

| Результат | Цели |
| - | - |
| Успешно | `make gateway-exposure-v2`, `make gateway-exposure-v2-protected` |
| Ошибка (ожидаемая) | `make gateway-exposure-v2-negative` |

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

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

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

| Результат | Цели |
| - | - |
| Успешно | `make nodes-pipeline`, `make approvals-token` |
| Ошибка (ожидаемая) | `make nodes-pipeline-negative`, `make approvals-token-negative` |

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

**Утверждение:** запросы на сопряжение соблюдают 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` |

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

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

| Результат | Цели |
| - | - |
| Успешно | `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` имеют приоритет над глобальными значениями по умолчанию; `identityLinks` объединяют сеансы только внутри явно связанных групп, но не между не связанными друг с другом собеседниками.

| Результат | Цели |
| - | - |
| Успешно | `make routing-precedence`, `make routing-identitylinks` |
| Ошибка (ожидаемая) | `make routing-precedence-negative`, `make routing-identitylinks-negative` |

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

* [Модель угроз](https://docs2.openclaw.ai/ru/security/THREAT-MODEL-ATLAS.md)
* [Участие в разработке модели угроз](https://docs2.openclaw.ai/ru/security/CONTRIBUTING-THREAT-MODEL.md)
* [Реагирование на инциденты](https://docs2.openclaw.ai/ru/security/incident-response.md)