Примітка: деякі старіші посилання можуть містити попередню назву проєкту.
Що це таке
Виконуваний набір регресійних тестів безпеки, керований сценаріями атак:- Кожне твердження має виконувану перевірку моделі на скінченному просторі станів.
- Багато тверджень мають парну негативну модель, яка створює трасу контрприкладу для реалістичного класу помилок.
Де розміщено моделі
Моделі підтримуються в окремому репозиторії: vignesh07/openclaw-formal-models.Наразі цей репозиторій недоступний (на момент написання GitHub повертає «Repository not found»). Якщо він усе ще недоступний для вас, перш ніж вважати, що моделі видалено, запитайте про їхнє поточне розташування в каналах супровідників OpenClaw.
Застереження
- Це моделі, а не повна реалізація TypeScript — між моделлю та кодом можуть виникати розбіжності.
- Результати обмежені простором станів, який досліджує TLC. Успішний результат не гарантує безпеки поза межами змодельованих припущень і обмежень.
- Деякі твердження спираються на явні припущення щодо середовища (наприклад, правильне розгортання та коректні вхідні дані конфігурації).
Відтворення результатів
Клонуйте репозиторій моделей і запустіть TLC:Твердження та цілі
Доступність Gateway і неправильна конфігурація відкритого Gateway
Твердження: прив’язування не лише до local loopback без автентифікації може зробити можливою віддалену компрометацію та збільшити поверхню атаки; токен або пароль блокує неавтентифікованих зловмисників відповідно до припущень моделі.
Див. також
docs/gateway-exposure-matrix.md у репозиторії моделей.
Конвеєр виконання Node (можливість із найвищим ризиком)
Твердження:exec host=node вимагає (а) списку дозволених команд Node разом із задекларованими командами та (б) підтвердження в реальному часі, якщо це налаштовано; у моделі підтвердження токенізовано для запобігання повторному використанню.
Сховище сполучення (контроль прямих повідомлень)
Твердження: запити на сполучення дотримуються TTL та обмежень кількості запитів, що очікують на розгляд.Контроль вхідних повідомлень (згадки та обхід керівними командами)
Твердження: у групових контекстах, де потрібна згадка, неавторизована керівна команда не може обійти контроль згадок.Маршрутизація та ізоляція ключів сеансів
Твердження: прямі повідомлення від різних співрозмовників не об’єднуються в один сеанс, якщо їх явно не пов’язано або не налаштовано відповідним чином.Моделі v1++: конкурентність, повторні спроби та коректність трасування
Подальші моделі, що підвищують точність моделювання реальних режимів відмов: неатомарних оновлень, повторних спроб і розгалуження повідомлень.Конкурентність та ідемпотентність сховища сполучення
Твердження: сховище сполучення забезпечує дотриманняMaxPending та ідемпотентність навіть за чергування операцій — перевірка з подальшим записом має бути атомарною або заблокованою, а оновлення не повинно створювати дублікати. Зокрема: конкурентні запити не можуть перевищувати MaxPending для каналу, а повторні запити або оновлення для тієї самої пари (channel, sender) не створюють дублікати активних рядків, що очікують на розгляд.
Кореляція трасування та ідемпотентність вхідних повідомлень
Твердження: приймання зберігає кореляцію трасування під час розгалуження та є ідемпотентним за повторних спроб постачальника. Коли одна зовнішня подія перетворюється на кілька внутрішніх повідомлень, кожна частина зберігає ту саму ідентичність траси або події; повторні спроби не призводять до подвійного опрацювання; якщо ідентифікатори подій постачальника відсутні, усунення дублікатів використовує безпечний запасний ключ (наприклад, ідентифікатор траси), щоб уникнути відкидання різних подій.Пріоритет dmScope у маршрутизації та identityLinks
Твердження: маршрутизація за замовчуванням зберігає ізоляцію сеансів прямих повідомлень і об’єднує сеанси лише за явного налаштування через пріоритет каналів і зв’язки ідентичностей. Специфічні для каналу перевизначення dmScope мають пріоритет над глобальними значеннями за замовчуванням; identityLinks об’єднують сеанси лише в межах явно пов’язаних груп, а не між непов’язаними співрозмовниками.