Chuyển đến nội dung chính
Các mô hình bảo mật chính thức của OpenClaw (hiện nay là TLA+/TLC) cung cấp một lập luận được máy kiểm tra rằng các đường dẫn cụ thể có rủi ro cao nhất — ủy quyền, cô lập phiên, kiểm soát công cụ và an toàn trước cấu hình sai — thực thi chính sách dự kiến của chúng theo các giả định đã được nêu rõ.
Lưu ý: một số liên kết cũ có thể đề cập đến tên trước đây của dự án.

​
Đây là gì

Một bộ kiểm thử hồi quy bảo mật có thể thực thi, được định hướng bởi kẻ tấn công:
  • Mỗi tuyên bố đều có một phép kiểm tra mô hình có thể chạy trên một không gian trạng thái hữu hạn.
  • Nhiều tuyên bố có một mô hình âm đi kèm, tạo ra dấu vết phản ví dụ cho một lớp lỗi thực tế.
Đây không phải là bằng chứng rằng OpenClaw an toàn về mọi mặt và không xác minh toàn bộ phần triển khai TypeScript.

​
Vị trí của các mô hình

Các mô hình được duy trì trong một kho lưu trữ riêng: vignesh07/openclaw-formal-models.
Kho lưu trữ đó hiện không thể truy cập được (GitHub trả về “Repository not found” tại thời điểm viết bài này). Nếu bạn vẫn không thể truy cập, hãy hỏi trong các kênh dành cho người bảo trì OpenClaw về vị trí hiện tại trước khi cho rằng các mô hình đã bị xóa.

​
Lưu ý

  • Đây là các mô hình, không phải toàn bộ phần triển khai TypeScript — có thể xảy ra sai lệch giữa mô hình và mã.
  • Kết quả bị giới hạn bởi không gian trạng thái mà TLC khám phá. Trạng thái xanh không hàm ý tính bảo mật vượt ngoài các giả định và giới hạn được mô hình hóa.
  • Một số tuyên bố phụ thuộc vào các giả định rõ ràng về môi trường (ví dụ: triển khai đúng và đầu vào cấu hình đúng).

​
Tái tạo kết quả

Sao chép kho lưu trữ mô hình và chạy TLC:
Chưa có tích hợp CI trở lại kho lưu trữ này; một phiên bản trong tương lai có thể bổ sung các mô hình chạy bằng CI cùng những thành phần tạo tác công khai (dấu vết phản ví dụ, nhật ký chạy) hoặc một quy trình “chạy mô hình này” được lưu trữ cho các phép kiểm tra có giới hạn nhỏ.

​
Tuyên bố và mục tiêu

​
Mức độ phơi bày của Gateway và cấu hình sai Gateway mở

Tuyên bố: việc liên kết ngoài loopback mà không có xác thực có thể khiến hành vi xâm phạm từ xa trở thành khả thi và làm tăng mức độ phơi bày; theo các giả định của mô hình, token/mật khẩu sẽ chặn những kẻ tấn công chưa được xác thực. Xem thêm docs/gateway-exposure-matrix.md trong kho lưu trữ mô hình.

​
Pipeline thực thi Node (khả năng có rủi ro cao nhất)

Tuyên bố: exec host=node yêu cầu (a) danh sách cho phép lệnh Node cùng các lệnh đã khai báo và (b) phê duyệt trực tiếp khi được cấu hình; trong mô hình, các phê duyệt được mã hóa bằng token để ngăn phát lại.

​
Kho ghép nối (kiểm soát DM)

Tuyên bố: các yêu cầu ghép nối tuân thủ TTL và giới hạn số yêu cầu đang chờ xử lý.

​
Kiểm soát đầu vào (đề cập và bỏ qua lệnh điều khiển)

Tuyên bố: trong ngữ cảnh nhóm yêu cầu đề cập, một lệnh điều khiển không được phép không thể bỏ qua cơ chế kiểm soát đề cập.

​
Định tuyến và cô lập khóa phiên

Tuyên bố: DM từ các đối tác khác nhau không bị gộp vào cùng một phiên, trừ khi được liên kết hoặc cấu hình rõ ràng.

​
Các mô hình v1++: tính đồng thời, thử lại, độ chính xác của dấu vết

Các mô hình tiếp nối giúp nâng cao độ trung thực đối với những chế độ lỗi trong thực tế: cập nhật không nguyên tử, thử lại và phân tán thông điệp.

​
Tính đồng thời và tính lũy đẳng của kho ghép nối

Tuyên bố: kho ghép nối thực thi MaxPending và tính lũy đẳng ngay cả khi các thao tác xen kẽ — thao tác kiểm tra rồi ghi phải mang tính nguyên tử/được khóa và thao tác làm mới không được tạo bản sao. Cụ thể: các yêu cầu đồng thời không thể vượt quá MaxPending đối với một kênh và các yêu cầu/lần làm mới lặp lại cho cùng một (channel, sender) không tạo ra các hàng đang chờ xử lý còn hiệu lực bị trùng lặp.

​
Tương quan dấu vết và tính lũy đẳng của đầu vào

Tuyên bố: quá trình tiếp nhận duy trì tương quan dấu vết trong toàn bộ quá trình phân tán và có tính lũy đẳng khi nhà cung cấp thử lại. Khi một sự kiện bên ngoài trở thành nhiều thông điệp nội bộ, mọi phần đều giữ nguyên danh tính dấu vết/sự kiện; các lần thử lại không xử lý hai lần; nếu thiếu ID sự kiện của nhà cung cấp, cơ chế loại bỏ trùng lặp sẽ dùng một khóa an toàn làm phương án dự phòng (ví dụ: ID dấu vết) để tránh loại bỏ các sự kiện khác nhau. Tuyên bố: thứ tự ưu tiên dmScope và các liên kết danh tính hoạt động một cách xác định: phạm vi main mặc định chia sẻ một phiên liên tục cho các DM của một chủ sở hữu duy nhất (mặc định của tác nhân cá nhân), trong khi mọi phạm vi cô lập đã cấu hình (per-peer, per-channel-peer, per-account-channel-peer) giữ các phiên DM tách biệt hoàn toàn. Các giá trị ghi đè dmScope dành riêng cho từng kênh được ưu tiên hơn các giá trị mặc định toàn cục; identityLinks chỉ gộp các phiên trong những nhóm được liên kết rõ ràng, không gộp giữa các đối tác không liên quan. Các hộp thư đến nhiều người dùng được kỳ vọng sẽ chọn một phạm vi cô lập (quy trình kiểm tra bảo mật thời gian chạy khuyến nghị điều này khi phát hiện lưu lượng DM nhiều người dùng).

​
Liên quan