---
permalink: /security/formal-verification/
read_when:
    - Перегляд гарантій або обмежень формальної моделі безпеки
    - Відтворення або оновлення перевірок моделі безпеки TLA+/TLC
summary: Машинно перевірені моделі безпеки для шляхів OpenClaw з найвищим ризиком.
title: Формальна верифікація (моделі безпеки)
x-i18n:
    generated_at: "2026-04-05T18:17:31Z"
    model: gpt-5.4
    provider: openai
    source_hash: 0f7cd2461dcc00d320a5210e50279d76a7fa84e0830c440398323d75e262a38a
    source_path: security/formal-verification.md
    workflow: 15
---

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

На цій сторінці відстежуються **формальні моделі безпеки** 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

**Твердження:** прив’язка поза loopback без автентифікації може зробити можливим віддалений компроміс / збільшує поверхню доступу; токен/пароль блокує неавторизованих атакувальників (відповідно до припущень моделі).

- Зелені запуски:
  - `make gateway-exposure-v2`
  - `make gateway-exposure-v2-protected`
- Червоний (очікувано):
  - `make gateway-exposure-v2-negative`

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

### Конвеєр виконання вузла (можливість з найвищим ризиком)

**Твердження:** `exec host=node` вимагає (a) allowlist команд вузла плюс оголошені команди і (b) живе схвалення, якщо його налаштовано; схвалення токенізуються, щоб запобігти повторному використанню (у моделі).

- Зелені запуски:
  - `make nodes-pipeline`
  - `make approvals-token`
- Червоний (очікувано):
  - `make nodes-pipeline-negative`
  - `make approvals-token-negative`

### Сховище pairing (обмеження DM)

**Твердження:** запити pairing дотримуються TTL і обмежень на кількість запитів у стані очікування.

- Зелені запуски:
  - `make pairing`
  - `make pairing-cap`
- Червоний (очікувано):
  - `make pairing-negative`
  - `make pairing-cap-negative`

### Обмеження ingress (згадки + обхід команд керування)

**Твердження:** у групових контекстах, де потрібна згадка, неавторизована «команда керування» не може обійти перевірку згадки.

- Зелений:
  - `make ingress-gating`
- Червоний (очікувано):
  - `make ingress-gating-negative`

### Ізоляція маршрутизації/ключів сесії

**Твердження:** DM від різних співрозмовників не зливаються в одну сесію, якщо їх не пов’язано/не налаштовано явним чином.

- Зелений:
  - `make routing-isolation`
- Червоний (очікувано):
  - `make routing-isolation-negative`

## v1++: додаткові обмежені моделі (конкурентність, повторні спроби, коректність сліду)

Це наступні моделі, які підвищують точність щодо реальних режимів відмови (неатомарні оновлення, повторні спроби та fan-out повідомлень).

### Конкурентність / ідемпотентність сховища pairing

**Твердження:** сховище pairing має забезпечувати `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`

### Кореляція слідів / ідемпотентність ingress

**Твердження:** приймання має зберігати кореляцію слідів під час fan-out і бути ідемпотентним за повторних спроб провайдера.

Що це означає:

- Коли одна зовнішня подія перетворюється на кілька внутрішніх повідомлень, кожна частина зберігає ту саму ідентичність сліду/події.
- Повторні спроби не призводять до подвійної обробки.
- Якщо ідентифікатори подій провайдера відсутні, дедуплікація резервно використовує безпечний ключ (наприклад, ідентифікатор сліду), щоб уникнути відкидання різних подій.

- Зелені:
  - `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

**Твердження:** маршрутизація має за замовчуванням зберігати ізоляцію DM-сесій і зливати сесії лише за явного налаштування (пріоритет каналу + посилання ідентичності).

Що це означає:

- Специфічні для каналу перевизначення dmScope мають переважати над глобальними значеннями за замовчуванням.
- identityLinks мають зливати сесії лише в межах явно пов’язаних груп, а не між не пов’язаними співрозмовниками.

- Зелені:
  - `make routing-precedence`
  - `make routing-identitylinks`
- Червоний (очікувано):
  - `make routing-precedence-negative`
  - `make routing-identitylinks-negative`
