راستی‌آزمایی صوری (مدل‌های امنیتی)

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

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

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

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

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

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

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

مدل‌ها در یک مخزن جداگانه نگهداری می‌شوند: vignesh07/openclaw-formal-models.

# هشدارهای مهم

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

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

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

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

شروع:

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

# مرتبط

• مدل تهدید
• مشارکت در مدل تهدید