---
permalink: /security/formal-verification/
read_when:
    - بررسی تضمین‌ها یا محدودیت‌های مدل امنیتی رسمی
    - بازتولید یا به‌روزرسانی بررسی‌های مدل امنیتی TLA+/TLC
summary: مدل‌های امنیتیِ بررسی‌شده به‌صورت ماشینی برای پرخطرترین مسیرهای OpenClaw.
title: راستی‌آزمایی صوری (مدل‌های امنیتی)
x-i18n:
    generated_at: "2026-04-29T23:35:33Z"
    model: gpt-5.5
    provider: openai
    source_hash: 8f50fa9118a80054b8d556cd4f1901b2d5fcb37fb0866bd5357a1b0a46c74116
    source_path: security/formal-verification.md
    workflow: 16
---

این صفحه **مدل‌های امنیتی رسمی** OpenClaw را پیگیری می‌کند (امروز TLA+/TLC؛ موارد بیشتر در صورت نیاز).

> نکته: برخی پیوندهای قدیمی‌تر ممکن است به نام قبلی پروژه اشاره کنند.

**هدف (ستاره شمالی):** ارائه استدلالی بررسی‌شده توسط ماشین که نشان دهد OpenClaw سیاست امنیتی
مورد نظر خود را (مجوزدهی، جداسازی نشست، دروازه‌گذاری ابزار، و
ایمنی در برابر پیکربندی نادرست) تحت فرض‌های صریح اعمال می‌کند.

**این چیست (امروز):** یک **مجموعه رگرسیون امنیتی** اجرایی و مبتنی بر مهاجم:

- هر ادعا یک بررسی مدل قابل اجرا روی یک فضای حالت محدود دارد.
- بسیاری از ادعاها یک **مدل منفی** همراه دارند که برای یک دسته باگ واقع‌بینانه، رد نمونه‌ای تولید می‌کند.

**این چه چیزی نیست (هنوز):** اثباتی بر اینکه «OpenClaw از همه جنبه‌ها امن است» یا اینکه پیاده‌سازی کامل TypeScript درست است.

## مدل‌ها کجا قرار دارند

مدل‌ها در یک مخزن جداگانه نگهداری می‌شوند: [vignesh07/openclaw-formal-models](https://github.com/vignesh07/openclaw-formal-models).

## احتیاط‌های مهم

- این‌ها **مدل** هستند، نه پیاده‌سازی کامل TypeScript. امکان انحراف بین مدل و کد وجود دارد.
- نتایج به فضای حالتی که TLC کاوش کرده محدود هستند؛ «سبز» بودن، امنیت فراتر از فرض‌ها و کران‌های مدل‌شده را نشان نمی‌دهد.
- برخی ادعاها به فرض‌های محیطی صریح تکیه دارند (برای مثال، استقرار درست، ورودی‌های پیکربندی درست).

## بازتولید نتایج

امروز، نتایج با کلون کردن محلی مخزن مدل‌ها و اجرای TLC بازتولید می‌شوند (پایین را ببینید). یک تکرار آینده می‌تواند ارائه کند:

- مدل‌های اجراشده در یکپارچه‌سازی مداوم با مصنوعات عمومی (ردهای رد نمونه، گزارش‌های اجرا)
- یک گردش‌کار میزبانی‌شده «این مدل را اجرا کن» برای بررسی‌های کوچک و محدود

شروع کار:

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

# Java 11+ required (TLC runs on the JVM).
# The repo vendors a pinned `tla2tools.jar` (TLA+ tools) and provides `bin/tlc` + Make targets.

make <target>
```

### در معرض قرار گرفتن Gateway و پیکربندی نادرست Gateway باز

**ادعا:** اتصال فراتر از 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`

### مخزن جفت‌سازی (دروازه‌گذاری پیام مستقیم)

**ادعا:** درخواست‌های جفت‌سازی به TTL و سقف درخواست‌های در انتظار احترام می‌گذارند.

- اجراهای سبز:
  - `make pairing`
  - `make pairing-cap`
- قرمز (مورد انتظار):
  - `make pairing-negative`
  - `make pairing-cap-negative`

### دروازه‌گذاری ورودی (اشاره‌ها + دور زدن فرمان کنترل)

**ادعا:** در زمینه‌های گروهی که به اشاره نیاز دارند، یک «فرمان کنترل» غیرمجاز نمی‌تواند دروازه‌گذاری اشاره را دور بزند.

- سبز:
  - `make ingress-gating`
- قرمز (مورد انتظار):
  - `make ingress-gating-negative`

### جداسازی مسیریابی/کلید نشست

**ادعا:** پیام‌های مستقیم از همتایان متمایز، مگر اینکه صریحا پیوند داده/پیکربندی شده باشند، در همان نشست ادغام نمی‌شوند.

- سبز:
  - `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` (رقابت سقف begin/commit غیراتمی)
  - `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

**ادعا:** مسیریابی باید نشست‌های پیام مستقیم را به‌صورت پیش‌فرض جدا نگه دارد، و فقط زمانی نشست‌ها را ادغام کند که صریحا پیکربندی شده باشد (تقدم کانال + پیوندهای هویت).

معنای آن:

- بازنویسی‌های dmScope مخصوص کانال باید بر پیش‌فرض‌های سراسری مقدم باشند.
- identityLinks باید فقط درون گروه‌های پیوندشده صریح ادغام کند، نه در میان همتایان نامرتبط.

- سبز:
  - `make routing-precedence`
  - `make routing-identitylinks`
- قرمز (مورد انتظار):
  - `make routing-precedence-negative`
  - `make routing-identitylinks-negative`

## مرتبط

- [مدل تهدید](/fa/security/THREAT-MODEL-ATLAS)
- [مشارکت در مدل تهدید](/fa/security/CONTRIBUTING-THREAT-MODEL)
