Formal Verification (Mô hình bảo mật)

Trang này theo dõi các mô hình bảo mật chính thức của OpenClaw (hiện tại dùng TLA+/TLC; sẽ bổ sung thêm nếu cần).

Lưu ý: một số link cũ có thể vẫn dùng tên dự án trước đây.

Mục tiêu (north star): cung cấp một lập luận được kiểm tra tự động rằng OpenClaw thực thi đúng chính sách bảo mật dự định (phân quyền, cách ly session, kiểm soát công cụ, và an toàn cấu hình sai), dưới các giả định rõ ràng.

Đây là gì (hiện tại): một bộ kiểm tra hồi quy bảo mật có thể chạy được, hướng theo kịch bản tấn công:

  • Mỗi khẳng định có một model-check có thể chạy trên không gian trạng thái hữu hạn.
  • Nhiều khẳng định có mô hình phủ định đi kèm để tạo ra trace phản ví dụ cho một lớp lỗi thực tế.

Đây không phải là gì (chưa): một chứng minh rằng “OpenClaw an toàn ở mọi khía cạnh” hoặc rằng toàn bộ implementation TypeScript là đúng.

Nơi lưu trữ các mô hình

Các mô hình được duy trì trong một repo riêng: vignesh07/openclaw-formal-models.

Những lưu ý quan trọng

  • Đây là các mô hình, không phải toàn bộ implementation TypeScript. Có thể có sự khác biệt giữa mô hình và code.
  • Kết quả bị giới hạn bởi không gian trạng thái mà TLC khám phá; “green” không có nghĩa là an toàn vượt ra ngoài các giả định và giới hạn đã mô hình hóa.
  • Một số khẳng định dựa trên các giả định môi trường rõ ràng (ví dụ: triển khai đúng, đầu vào cấu hình đúng).

Tái tạo kết quả

Hiện tại, kết quả được tái tạo bằng cách clone repo mô hình về máy và chạy TLC (xem bên dưới). Phiên bản tương lai có thể cung cấp:

  • Các mô hình chạy trên CI với artifacts công khai (trace phản ví dụ, log chạy)
  • một workflow “chạy mô hình này” được host cho các kiểm tra nhỏ, có giới hạn

Bắt đầu:

git clone https://github.com/vignesh07/openclaw-formal-models
cd openclaw-formal-models

# Cần Java 11+ (TLC chạy trên JVM).
# Repo này đi kèm một `tla2tools.jar` đã được pin (công cụ TLA+) và cung cấp `bin/tlc` + các target Make.

make <target>

Gateway exposure và cấu hình sai open gateway

Khẳng định: binding vượt ra ngoài loopback mà không có auth có thể khiến remote compromise trở nên khả thi / tăng exposure; token/password chặn các attacker không có auth (theo giả định của mô hình).

  • Green runs:
    • make gateway-exposure-v2
    • make gateway-exposure-v2-protected
  • Red (mong đợi):
    • make gateway-exposure-v2-negative

Xem thêm: docs/gateway-exposure-matrix.md trong repo mô hình.

Nodes.run pipeline (khả năng có rủi ro cao nhất)

Khẳng định: nodes.run yêu cầu (a) allowlist lệnh node cộng với các lệnh đã khai báo và (b) phê duyệt trực tiếp khi được cấu hình; các phê duyệt được tokenize để ngăn replay (trong mô hình).

  • Green runs:
    • make nodes-pipeline
    • make approvals-token
  • Red (mong đợi):
    • make nodes-pipeline-negative
    • make approvals-token-negative

Pairing store (DM gating)

Khẳng định: các yêu cầu pairing tuân thủ TTL và giới hạn pending-request.

  • Green runs:
    • make pairing
    • make pairing-cap
  • Red (mong đợi):
    • make pairing-negative
    • make pairing-cap-negative

Ingress gating (mentions + control-command bypass)

Khẳng định: trong các ngữ cảnh nhóm yêu cầu mention, một “control command” không được phép không thể bypass mention gating.

  • Green:
    • make ingress-gating
  • Red (mong đợi):
    • make ingress-gating-negative

Routing/session-key isolation

Khẳng định: các DM từ các peer khác nhau không bị gộp vào cùng một session trừ khi được liên kết/cấu hình rõ ràng.

  • Green:
    • make routing-isolation
  • Red (mong đợi):
    • make routing-isolation-negative

v1++: các mô hình có giới hạn bổ sung (concurrency, retries, trace correctness)

Đây là các mô hình tiếp theo giúp tăng độ chính xác xung quanh các chế độ lỗi thực tế (cập nhật không atomic, retry, và message fan-out).

Pairing store concurrency / idempotency

Khẳng định: một pairing store nên thực thi MaxPending và idempotency ngay cả dưới các interleaving (tức là, “check-then-write” phải atomic / locked; refresh không nên tạo duplicate).

Ý nghĩa:

  • Dưới các request đồng thời, bạn không thể vượt quá MaxPending cho một channel.

  • Các request/refresh lặp lại cho cùng một (channel, sender) không nên tạo các hàng pending live trùng lặp.

  • Green runs:

    • make pairing-race (kiểm tra cap atomic/locked)
    • make pairing-idempotency
    • make pairing-refresh
    • make pairing-refresh-race

  • Red (mong đợi):

    • make pairing-race-negative (race cap begin/commit không atomic)
    • make pairing-idempotency-negative
    • make pairing-refresh-negative
    • make pairing-refresh-race-negative

Ingress trace correlation / idempotency

Khẳng định: ingestion nên bảo toàn trace correlation qua fan-out và idempotent dưới các retry của provider.

Ý nghĩa:

  • Khi một sự kiện bên ngoài trở thành nhiều message nội bộ, mọi phần đều giữ cùng trace/event identity.

  • Các retry không dẫn đến xử lý hai lần.

  • Nếu thiếu provider event ID, dedupe sẽ fallback về một key an toàn (ví dụ: trace ID) để tránh bỏ qua các sự kiện khác nhau.

  • Green:

    • make ingress-trace
    • make ingress-trace2
    • make ingress-idempotency
    • make ingress-dedupe-fallback

  • Red (mong đợi):

    • make ingress-trace-negative
    • make ingress-trace2-negative
    • make ingress-idempotency-negative
    • make ingress-dedupe-fallback-negative

Routing dmScope precedence + identityLinks

Khẳng định: routing phải giữ các DM session cách ly theo mặc định, và chỉ gộp các session khi được cấu hình rõ ràng (channel precedence + identity links).

Ý nghĩa:

  • Các override dmScope cụ thể cho channel phải thắng các giá trị mặc định toàn cục.

  • identityLinks chỉ nên gộp trong các nhóm được liên kết rõ ràng, không phải qua các peer không liên quan.

  • Green:

    • make routing-precedence
    • make routing-identitylinks

  • Red (mong đợi):

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