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 باز
ادعا: طبق فرضهای مدل، اتصال به نشانیهایی فراتر از 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 (رقابت غیراتمی سقف در آغاز/ثبت)، 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 |
