---
permalink: /security/formal-verification/
read_when:
    - Анализ формальных гарантий или ограничений модели безопасности
    - Воспроизведение или обновление проверок модели безопасности TLA+/TLC
summary: Машинно проверенные модели безопасности для наиболее рискованных путей OpenClaw.
title: Формальная верификация (модели безопасности)
x-i18n:
    generated_at: "2026-06-28T23:47:15Z"
    model: gpt-5.5
    postprocess_version: locale-links-v1
    provider: openai
    source_hash: 298b92f27abb8321be807fe4d95c7cd568a0fb8f543d168863b2adb9b3ddcde4
    source_path: security/formal-verification.md
    workflow: 16
---

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```bash
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)