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 و پیوندهای هویتی بهصورت قطعی رفتار میکنند: دامنه پیشفرض main یک نشست چرخشی را میان پیامهای خصوصی یک مالک واحد به اشتراک میگذارد (پیشفرض عامل شخصی)، درحالیکه هر دامنه جداساز پیکربندیشده (per-peer، per-channel-peer، per-account-channel-peer) نشستهای پیام خصوصی را کاملاً جدا نگه میدارد. بازنویسیهای مختص کانال در dmScope بر پیشفرضهای سراسری اولویت دارند؛ identityLinks نشستها را فقط درون گروههای صریحاً پیوندخورده ادغام میکنند، نه میان همتایان نامرتبط. انتظار میرود صندوقهای ورودی چندکاربره یک دامنه جداساز را انتخاب کنند (ممیزی امنیتی زمان اجرا، هنگام تشخیص ترافیک پیام خصوصی چندکاربره، این کار را توصیه میکند).
| نتیجه | اهداف |
|---|---|
| سبز | make routing-precedence, make routing-identitylinks |
| قرمز (مورد انتظار) | make routing-precedence-negative, make routing-identitylinks-negative |
