---
permalink: /security/formal-verification/
read_when:
    - Огляд формальних гарантій або обмежень моделі безпеки
    - Відтворення або оновлення перевірок моделі безпеки TLA+/TLC
summary: Машинно перевірені моделі безпеки для шляхів OpenClaw із найвищим ризиком.
title: Формальна верифікація (моделі безпеки)
x-i18n:
    generated_at: "2026-05-06T03:31:00Z"
    model: gpt-5.5
    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+ required (TLC runs on the JVM).
# The repo vendors a pinned `tla2tools.jar` (TLA+ tools) and provides `bin/tlc` + Make targets.

make <target>
```

### Експозиція 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`

### Сховище спарювання (контроль доступу 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`

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

**Твердження:** приймання вхідних подій має зберігати кореляцію трас під час 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`

## Пов’язане

- [Модель загроз](/uk/security/THREAT-MODEL-ATLAS)
- [Як долучитися до моделі загроз](/uk/security/CONTRIBUTING-THREAT-MODEL)