Security

การพิสูจน์ยืนยันอย่างเป็นทางการ (แบบจำลองความปลอดภัย)

โมเดลความปลอดภัยอย่างเป็นทางการของ OpenClaw (ปัจจุบันใช้ TLA+/TLC) ให้ข้อพิสูจน์ที่ตรวจสอบโดยเครื่องว่าเส้นทางที่มีความเสี่ยงสูงสุดบางรายการ ได้แก่ การอนุญาต การแยกเซสชัน การควบคุมการใช้เครื่องมือ และความปลอดภัยจากการกำหนดค่าผิด บังคับใช้นโยบายตามที่ตั้งใจไว้ ภายใต้สมมติฐานที่ระบุไว้อย่างชัดเจน

หมายเหตุ: ลิงก์เก่าบางรายการอาจอ้างถึงชื่อเดิมของโครงการ

สิ่งนี้คืออะไร

ชุดทดสอบการถดถอยด้านความปลอดภัยที่เรียกใช้งานได้และขับเคลื่อนโดยผู้โจมตี:

แต่ละข้อกล่าวอ้างมีการตรวจสอบโมเดลที่เรียกใช้งานได้บนปริภูมิสถานะจำกัด
ข้อกล่าวอ้างหลายรายการมีโมเดลเชิงลบที่จับคู่กัน ซึ่งสร้างร่องรอยตัวอย่างโต้แย้งสำหรับกลุ่มข้อบกพร่องที่เกิดขึ้นได้จริง

สิ่งนี้ ไม่ใช่ ข้อพิสูจน์ว่า OpenClaw ปลอดภัยในทุกด้าน และไม่ได้ตรวจสอบการใช้งานจริงด้วย TypeScript ทั้งหมด

ตำแหน่งของโมเดล

โมเดลได้รับการดูแลในรีโพแยกต่างหาก: vignesh07/openclaw-formal-models

ข้อควรระวัง

สิ่งเหล่านี้เป็นโมเดล ไม่ใช่การใช้งานจริงด้วย TypeScript ทั้งหมด จึงอาจเกิดความคลาดเคลื่อนระหว่างโมเดลกับโค้ดได้
ผลลัพธ์ถูกจำกัดด้วยปริภูมิสถานะที่ TLC สำรวจ ผลลัพธ์สีเขียวไม่ได้หมายความว่าจะปลอดภัยนอกเหนือจากสมมติฐานและขอบเขตที่สร้างโมเดลไว้
ข้อกล่าวอ้างบางรายการอาศัยสมมติฐานด้านสภาพแวดล้อมที่ระบุไว้อย่างชัดเจน (เช่น การปรับใช้อย่างถูกต้องและอินพุตการกำหนดค่าที่ถูกต้อง)

การทำซ้ำผลลัพธ์

โคลนรีโพโมเดลและเรียกใช้ TLC:

bash

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 แบบเปิดที่ไม่ถูกต้อง

ข้อกล่าวอ้าง: การผูกกับอินเทอร์เฟซนอกเหนือจากลูปแบ็กโดยไม่มีการยืนยันตัวตนอาจทำให้การเจาะระบบจากระยะไกลเป็นไปได้และเพิ่มการเปิดเผย ส่วนโทเค็น/รหัสผ่านจะป้องกันผู้โจมตีที่ไม่ได้ยืนยันตัวตน ตามสมมติฐานของโมเดล

ผลลัพธ์	เป้าหมาย
เขียว	`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++: ภาวะพร้อมกัน การลองซ้ำ และความถูกต้องของร่องรอย

โมเดลต่อยอดที่เพิ่มความเที่ยงตรงให้กับโหมดความล้มเหลวในโลกจริง ได้แก่ การอัปเดตที่ไม่เป็นอะตอม การลองซ้ำ และการกระจายข้อความ

ภาวะพร้อมกันและความเป็นไอดempotentของที่เก็บการจับคู่

ข้อกล่าวอ้าง: ที่เก็บการจับคู่บังคับใช้ MaxPending และความเป็นไอดempotentแม้ภายใต้การสลับลำดับการทำงาน โดยการตรวจสอบแล้วเขียนต้องเป็นอะตอมหรือถูกล็อก และการรีเฟรชต้องไม่สร้างรายการซ้ำ กล่าวอย่างเป็นรูปธรรมคือ คำขอที่เกิดพร้อมกันต้องไม่เกิน MaxPending สำหรับช่องทางหนึ่ง และคำขอ/การรีเฟรชซ้ำสำหรับ (channel, sender) เดียวกันต้องไม่สร้างแถวรอดำเนินการที่ยังใช้งานอยู่ซ้ำกัน

ผลลัพธ์	เป้าหมาย
เขียว	`make pairing-race` (การตรวจสอบขีดจำกัดแบบอะตอมหรือมีการล็อก), `make pairing-idempotency`, `make pairing-refresh`, `make pairing-refresh-race`
แดง (ตามคาด)	`make pairing-race-negative` (ภาวะแข่งขันของขีดจำกัดระหว่างเริ่มต้น/คอมมิตที่ไม่เป็นอะตอม), `make pairing-idempotency-negative`, `make pairing-refresh-negative`, `make pairing-refresh-race-negative`

การเชื่อมโยงร่องรอยขาเข้าและความเป็นไอดempotent

ข้อกล่าวอ้าง: การนำเข้าจะรักษาการเชื่อมโยงร่องรอยระหว่างการกระจาย และมีความเป็นไอดempotentเมื่อผู้ให้บริการลองซ้ำ เมื่อเหตุการณ์ภายนอกหนึ่งรายการกลายเป็นข้อความภายในหลายรายการ ทุกส่วนจะเก็บเอกลักษณ์ของร่องรอย/เหตุการณ์เดียวกันไว้ การลองซ้ำจะไม่ประมวลผลซ้ำสองครั้ง และหากไม่มี ID เหตุการณ์ของผู้ให้บริการ การขจัดรายการซ้ำจะใช้คีย์สำรองที่ปลอดภัย (เช่น ID ร่องรอย) เพื่อหลีกเลี่ยงการทิ้งเหตุการณ์ที่แตกต่างกัน

ผลลัพธ์	เป้าหมาย
เขียว	`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`

ลำดับความสำคัญของ dmScope ในการกำหนดเส้นทางและ identityLinks

ข้อกล่าวอ้าง: ลำดับความสำคัญของ dmScope และลิงก์เอกลักษณ์ทำงานอย่างกำหนดแน่นอน: ขอบเขตเริ่มต้น main ใช้เซสชันต่อเนื่องหนึ่งเซสชันร่วมกันระหว่าง DM ของเจ้าของคนเดียว (ค่าเริ่มต้นของเอเจนต์ส่วนบุคคล) ส่วนขอบเขตแบบแยกที่กำหนดค่าไว้ (per-peer, per-channel-peer, per-account-channel-peer) จะแยกเซสชัน DM ออกจากกันอย่างเคร่งครัด การแทนที่ dmScope เฉพาะช่องทางมีลำดับความสำคัญเหนือค่าเริ่มต้นส่วนกลาง ส่วน identityLinks จะรวมเซสชันเฉพาะภายในกลุ่มที่เชื่อมโยงไว้อย่างชัดเจนเท่านั้น ไม่รวมข้ามคู่สนทนาที่ไม่เกี่ยวข้อง กล่องข้อความที่มีผู้ใช้หลายคนควรเลือกใช้ขอบเขตแบบแยก (การตรวจสอบความปลอดภัยของรันไทม์จะแนะนำเช่นนี้เมื่อตรวจพบการรับส่ง DM ของผู้ใช้หลายคน)

ผลลัพธ์	เป้าหมาย
เขียว	`make routing-precedence`, `make routing-identitylinks`
แดง (ตามคาด)	`make routing-precedence-negative`, `make routing-identitylinks-negative`

ที่เกี่ยวข้อง

Was this useful?