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

Формальні моделі безпеки OpenClaw (наразі TLA+/TLC) надають перевірений машиною аргумент, що певні шляхи з найвищим ризиком — авторизація, ізоляція сеансів, контроль доступу до інструментів і безпека в разі неправильної конфігурації — забезпечують дотримання передбаченої політики за явно визначених припущень.

Примітка: деякі старіші посилання можуть містити попередню назву проєкту.

Що це таке

Виконуваний набір регресійних тестів безпеки, керований сценаріями атак:

• Кожне твердження має виконувану перевірку моделі на скінченному просторі станів.
• Багато тверджень мають парну негативну модель, яка створює трасу контрприкладу для реалістичного класу помилок.

Це не є доказом того, що OpenClaw безпечний у всіх аспектах, і не перевіряє повну реалізацію TypeScript.

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

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

Застереження

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

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

Клонуйте репозиторій моделей і запустіть TLC:

git clone https://github.com/vignesh07/openclaw-formal-modelscd openclaw-formal-models # Потрібна Java 11+ (TLC працює на JVM).# Репозиторій містить зафіксовану версію tla2tools.jar і надає bin/tlc та цілі Make. make <target>

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

Твердження та цілі

Доступність Gateway і неправильна конфігурація відкритого Gateway

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

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

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

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

Сховище сполучення (контроль прямих повідомлень)

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

Контроль вхідних повідомлень (згадки та обхід керівними командами)

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

Маршрутизація та ізоляція ключів сеансів

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

Моделі v1++: конкурентність, повторні спроби та коректність трасування

Подальші моделі, що підвищують точність моделювання реальних режимів відмов: неатомарних оновлень, повторних спроб і розгалуження повідомлень.

Конкурентність та ідемпотентність сховища сполучення

Твердження: сховище сполучення забезпечує дотримання MaxPending та ідемпотентність навіть за чергування операцій — перевірка з подальшим записом має бути атомарною або заблокованою, а оновлення не повинно створювати дублікати. Зокрема: конкурентні запити не можуть перевищувати MaxPending для каналу, а повторні запити або оновлення для тієї самої пари (channel, sender) не створюють дублікати активних рядків, що очікують на розгляд.

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

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

Пріоритет dmScope у маршрутизації та identityLinks

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

Пов’язані матеріали

• Модель загроз
• Участь у розробці моделі загроз
• Реагування на інциденти