English简体中文繁體中文日本語EspañolPortuguês (BR)한국어DeutschFrançaisالعربيةItalianoTiếng ViệtNederlandsTürkçeУкраїнськаBahasa IndonesiaPolskiفارسیไทย

Security

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

Ця сторінка відстежує формальні моделі безпеки 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+ 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

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

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

  • Перевизначення dmScope для конкретного каналу мають мати пріоритет над глобальними значеннями за замовчуванням.

  • identityLinks мають зливати лише в межах явно пов’язаних груп, а не між непов’язаними співрозмовниками.

  • Зелені:

    • make routing-precedence
    • make routing-identitylinks

  • Червоні (очікувано):

    • make routing-precedence-negative
    • make routing-identitylinks-negative

Пов’язане