Перейти до основного вмісту

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

На цій сторінці відстежуються формальні моделі безпеки OpenClaw (сьогодні це TLA+/TLC; за потреби буде більше).
Примітка: деякі старіші посилання можуть посилатися на попередню назву проєкту.
Мета (північна зірка): надати машинно перевірений аргумент, що OpenClaw забезпечує задуману політику безпеки (авторизацію, ізоляцію сесій, обмеження інструментів і безпечність конфігурації за помилкових налаштувань) за явних припущень. Що це таке (сьогодні): виконуваний, керований атакувальником набір регресійних перевірок безпеки:
  • Для кожного твердження є виконувана перевірка моделі на скінченному просторі станів.
  • Для багатьох тверджень є парна негативна модель, яка породжує слід контрприкладу для реалістичного класу помилок.
Чим це поки не є: доказом того, що «OpenClaw безпечний у всіх аспектах» або що повна реалізація на TypeScript є коректною.

​
Де розміщені моделі

Моделі підтримуються в окремому репозиторії: vignesh07/openclaw-formal-models.

​
Важливі застереження

  • Це моделі, а не повна реалізація на TypeScript. Можливі розбіжності між моделлю та кодом.
  • Результати обмежені простором станів, який досліджує TLC; «зелений» результат не означає безпеку поза межами змодельованих припущень і обмежень.
  • Деякі твердження спираються на явні припущення про середовище (наприклад, правильне розгортання, коректні вхідні дані конфігурації).

​
Відтворення результатів

Сьогодні результати відтворюються шляхом локального клонування репозиторію моделей і запуску TLC (див. нижче). У майбутній ітерації можуть з’явитися:
  • моделі, що запускаються в CI, із публічними артефактами (слідами контрприкладів, журналами запусків)
  • розміщений workflow «запустити цю модель» для малих, обмежених перевірок
Початок роботи: 
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
Твердження: маршрутизація має за замовчуванням зберігати ізоляцію DM-сесій і зливати сесії лише за явного налаштування (пріоритет каналу + посилання ідентичності). Що це означає:
  • Специфічні для каналу перевизначення dmScope мають переважати над глобальними значеннями за замовчуванням.
  • identityLinks мають зливати сесії лише в межах явно пов’язаних груп, а не між не пов’язаними співрозмовниками.
  • Зелені:
    • make routing-precedence
    • make routing-identitylinks
  • Червоний (очікувано):
    • make routing-precedence-negative
    • make routing-identitylinks-negative