Security
การตรวจสอบยืนยันเชิงรูปนัย (แบบจำลองความปลอดภัย)
แบบจำลองความปลอดภัยอย่างเป็นทางการของ 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 โดยไม่มีการยืนยันตัวตนอาจเปิดโอกาสให้ถูกเจาะระบบจากระยะไกลและเพิ่มพื้นผิวการเปิดเผย ส่วนโทเค็น/รหัสผ่านจะป้องกันผู้โจมตีที่ไม่ได้ยืนยันตัวตน ตามสมมติฐานของแบบจำลอง
| ผลลัพธ์ | เป้าหมาย |
|---|---|
| ผ่าน | 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++: การทำงานพร้อมกัน การลองใหม่ และความถูกต้องของร่องรอย
แบบจำลองต่อยอดที่เพิ่มความเที่ยงตรงสำหรับโหมดความล้มเหลวในโลกจริง ได้แก่ การอัปเดตที่ไม่เป็นอะตอม การลองใหม่ และการกระจายข้อความ
การทำงานพร้อมกันและภาวะทำซ้ำแล้วได้ผลเดิมของที่เก็บการจับคู่
ข้ออ้าง: ที่เก็บการจับคู่บังคับใช้ MaxPending และภาวะทำซ้ำแล้วได้ผลเดิมแม้ในการสลับลำดับการทำงาน โดยการตรวจสอบก่อนเขียนต้องเป็นแบบอะตอมหรือมีการล็อก และการรีเฟรชต้องไม่สร้างรายการซ้ำ กล่าวอย่างเจาะจงคือ คำขอที่เกิดขึ้นพร้อมกันต้องไม่ทำให้จำนวนเกิน 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 |
ความสัมพันธ์ของร่องรอยขาเข้าและภาวะทำซ้ำแล้วได้ผลเดิม
ข้ออ้าง: การรับข้อมูลเข้ารักษาความสัมพันธ์ของร่องรอยตลอดการกระจายข้อความ และมีภาวะทำซ้ำแล้วได้ผลเดิมเมื่อผู้ให้บริการลองใหม่ เมื่อเหตุการณ์ภายนอกหนึ่งรายการกลายเป็นข้อความภายในหลายรายการ ทุกส่วนจะคงอัตลักษณ์ของร่องรอย/เหตุการณ์เดียวกัน การลองใหม่จะไม่ทำให้ประมวลผลซ้ำ และหากไม่มีรหัสเหตุการณ์จากผู้ให้บริการ การขจัดรายการซ้ำจะใช้คีย์สำรองที่ปลอดภัย (ตัวอย่างเช่น รหัสร่องรอย) เพื่อหลีกเลี่ยงการทิ้งเหตุการณ์ที่แตกต่างกัน
| ผลลัพธ์ | เป้าหมาย |
|---|---|
| ผ่าน | 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
ข้ออ้าง: การกำหนดเส้นทางจะแยกเซสชัน DM ตามค่าเริ่มต้น และจะรวมเซสชันเฉพาะเมื่อกำหนดค่าไว้อย่างชัดเจน ผ่านลำดับความสำคัญของช่องทางและลิงก์อัตลักษณ์ ค่า dmScope เฉพาะช่องทางมีลำดับความสำคัญเหนือค่าเริ่มต้นส่วนกลาง ส่วน identityLinks จะรวมเซสชันเฉพาะภายในกลุ่มที่เชื่อมโยงไว้อย่างชัดเจนเท่านั้น ไม่รวมคู่สนทนาที่ไม่เกี่ยวข้องกัน
| ผลลัพธ์ | เป้าหมาย |
|---|---|
| ผ่าน | make routing-precedence, make routing-identitylinks |
| ไม่ผ่าน (คาดไว้) | make routing-precedence-negative, make routing-identitylinks-negative |
