الانتقال إلى المحتوى الرئيسي

الأمان

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

تتتبع هذه الصفحة نماذج الأمان الرسمية لـ 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