التحقق الرسمي (نماذج الأمان)

تتتبع هذه الصفحة نماذج الأمان الرسمية لـ 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+ مطلوب (TLC يعمل على JVM).
# المستودع يوفر نسخة مثبتة من `tla2tools.jar` (أدوات TLA+) ويوفر `bin/tlc` + أهداف Make.

make <target>

تعرض البوابة والتكوين الخاطئ للبوابة المفتوحة

المطالبة: الربط خارج النطاق المحلي بدون مصادقة يمكن أن يجعل الاختراق عن بُعد ممكنًا / يزيد التعرض؛ الرمز المميز / كلمة المرور تمنع المهاجمين غير المصرح لهم (حسب افتراضات النموذج).

• عمليات تشغيل خضراء:
  • make gateway-exposure-v2
  • make gateway-exposure-v2-protected
• أحمر (متوقع):
  • make gateway-exposure-v2-negative

انظر أيضًا: docs/gateway-exposure-matrix.md في مستودع النماذج.

خط أنابيب Nodes.run (القدرة الأكثر خطورة)

المطالبة: nodes.run يتطلب (أ) قائمة السماح لأوامر العقدة بالإضافة إلى الأوامر المعلنة و (ب) موافقة مباشرة عند التكوين؛ يتم تحويل الموافقات إلى رموز مميزة لمنع إعادة الاستخدام (في النموذج).

• عمليات تشغيل خضراء:
  • 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

عزل التوجيه / مفتاح الجلسة

المطالبة: الرسائل المباشرة من أقران مختلفين لا تندمج في نفس الجلسة إلا إذا تم ربطها / تكوينها صراحةً.

• أخضر:
  • 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

TailscaleREADME