---
permalink: /security/formal-verification/
read_when:
- Проверка формальных гарантий или ограничений модели безопасности
- Воспроизведение или обновление проверок модели безопасности TLA+/TLC
summary: Машинно-проверяемые модели безопасности для наиболее рискованных путей OpenClaw.
title: Формальная верификация (модели безопасности)
x-i18n:
generated_at: "2026-07-13T18:46:25Z"
model: gpt-5.6
postprocess_version: locale-links-v1
prompt_version: 24
provider: openai
source_hash: 86342f6e2f54c08d5e0f8a08d0d488459650a6ace35e985ff886f847540202c9
source_path: security/formal-verification.md
workflow: 16
---
Формальные модели безопасности OpenClaw (на сегодняшний день TLA+/TLC) предоставляют проверенный машинным способом аргумент в пользу того, что конкретные пути с наивысшим риском — авторизация, изоляция сеансов, ограничение доступа к инструментам и безопасность при неверной конфигурации — обеспечивают соблюдение предусмотренной политики при явно указанных допущениях.
> Примечание: некоторые старые ссылки могут содержать предыдущее название проекта.
## Что это такое
Исполняемый набор регрессионных тестов безопасности, моделирующий действия злоумышленника:
- Для каждого утверждения предусмотрена запускаемая проверка модели в конечном пространстве состояний.
- Для многих утверждений предусмотрена парная негативная модель, которая создаёт трассу контрпримера для реалистичного класса ошибок.
Это **не** доказательство того, что OpenClaw безопасен во всех отношениях, и оно не проверяет полную реализацию на TypeScript.
## Где находятся модели
Модели поддерживаются в отдельном репозитории: [vignesh07/openclaw-formal-models](https://github.com/vignesh07/openclaw-formal-models).
В настоящее время этот репозиторий недоступен (на момент написания GitHub возвращает "Repository not found"). Если он по-прежнему недоступен для вас, уточните его текущее расположение в каналах сопровождающих OpenClaw, прежде чем предполагать, что модели были удалены.
## Ограничения
- Это модели, а не полная реализация на TypeScript, поэтому модель и код могут расходиться.
- Результаты ограничены пространством состояний, исследуемым TLC. Успешный результат не гарантирует безопасность за пределами смоделированных допущений и границ.
- Некоторые утверждения основаны на явных допущениях о среде (например, о правильном развёртывании и корректных входных данных конфигурации).
## Воспроизведение результатов
Клонируйте репозиторий моделей и запустите TLC:
```bash
git clone https://github.com/vignesh07/openclaw-formal-models
cd openclaw-formal-models
# Требуется Java 11+ (TLC работает на JVM).
# Репозиторий содержит закреплённую версию tla2tools.jar и предоставляет bin/tlc, а также цели Make.
make
```
Интеграции с 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` |
## Связанные материалы
- [Модель угроз](/ru/security/THREAT-MODEL-ATLAS)
- [Участие в разработке модели угроз](/ru/security/CONTRIBUTING-THREAT-MODEL)
- [Реагирование на инциденты](/ru/security/incident-response)