---
permalink: /security/formal-verification/
read_when:
    - بررسی تضمین‌ها یا محدودیت‌های مدل امنیتی رسمی
    - بازتولید یا به‌روزرسانی بررسی‌های مدل امنیتی TLA+/TLC
summary: مدل‌های امنیتیِ بررسی‌شده به‌صورت ماشینی برای پرخطرترین مسیرهای OpenClaw.
title: راستی‌آزمایی صوری (مدل‌های امنیتی)
x-i18n:
    generated_at: "2026-05-06T09:42:17Z"
    model: gpt-5.5
    provider: openai
    source_hash: 298b92f27abb8321be807fe4d95c7cd568a0fb8f543d168863b2adb9b3ddcde4
    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 بازتولید می‌شوند (پایین را ببینید). یک تکرار آینده می‌تواند موارد زیر را ارائه کند:

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

شروع:

```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`

### ذخیره‌گاه جفت‌سازی (گیتینگ 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` (رقابت سقف 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

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

معنای آن:

- بازنویسی‌های 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)