---
permalink: /security/formal-verification/
read_when:
    - การทบทวนการรับประกันหรือข้อจำกัดของแบบจำลองความปลอดภัยอย่างเป็นทางการ
    - การทำซ้ำหรืออัปเดตการตรวจสอบโมเดลความปลอดภัย TLA+/TLC
summary: โมเดลความปลอดภัยที่ตรวจสอบด้วยเครื่องสำหรับเส้นทางที่มีความเสี่ยงสูงสุดของ OpenClaw
title: การพิสูจน์ยืนยันอย่างเป็นทางการ (แบบจำลองความปลอดภัย)
x-i18n:
    generated_at: "2026-07-19T08:01:41Z"
    model: gpt-5.6
    postprocess_version: locale-links-v1
    prompt_version: 32
    provider: openai
    source_hash: 185ee5c1cff7325f10827330c0c7e55ddc3ca40caf6088d4c930ae5e090d6b27
    source_path: security/formal-verification.md
    workflow: 16
---

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

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

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

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

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

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

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

โมเดลได้รับการดูแลในรีโพแยกต่างหาก: [vignesh07/openclaw-formal-models](https://github.com/vignesh07/openclaw-formal-models)

<Note>
ขณะนี้ไม่สามารถเข้าถึงรีโพนั้นได้ (GitHub แสดงข้อความ "Repository not found" ณ เวลาที่เขียน) หากฝั่งคุณยังเข้าถึงไม่ได้เช่นกัน โปรดสอบถามตำแหน่งปัจจุบันในช่องทางของผู้ดูแล OpenClaw ก่อนสันนิษฐานว่าโมเดลถูกนำออกแล้ว
</Note>

## ข้อควรระวัง

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

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

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

```bash
git clone https://github.com/vignesh07/openclaw-formal-models
cd 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` |

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

- [โมเดลภัยคุกคาม](/th/security/THREAT-MODEL-ATLAS)
- [การมีส่วนร่วมในโมเดลภัยคุกคาม](/th/security/CONTRIBUTING-THREAT-MODEL)
- [การตอบสนองต่อเหตุการณ์](/th/security/incident-response)