ملاحظة: قد تشير بعض الروابط القديمة إلى الاسم السابق للمشروع.
ما هذا
حزمة تنفيذية لاختبارات انحدار الأمان يقودها المهاجم:- لكل ادعاء فحص نموذج قابل للتشغيل ضمن فضاء حالات محدود.
- للعديد من الادعاءات نموذج سلبي مقابل ينتج مسار مثال مضاد لفئة واقعية من الأخطاء.
مكان وجود النماذج
تُصان النماذج في مستودع منفصل: vignesh07/openclaw-formal-models.يتعذر حاليًا الوصول إلى ذلك المستودع (يعرض GitHub الرسالة “Repository not found” وقت كتابة هذا النص). إذا ظل معطّلًا لديك، فاسأل في قنوات مشرفي OpenClaw عن موقعه الحالي قبل افتراض إزالة النماذج.
محاذير
- هذه نماذج وليست تنفيذ TypeScript الكامل — وقد يحدث انحراف بين النموذج والشفرة.
- تتقيد النتائج بفضاء الحالات الذي يستكشفه TLC. لا تعني النتيجة الناجحة تحقق الأمان خارج الافتراضات والحدود الممثلة في النموذج.
- تعتمد بعض الادعاءات على افتراضات صريحة بشأن البيئة (مثل النشر الصحيح ومدخلات الإعداد الصحيحة).
إعادة إنتاج النتائج
استنسخ مستودع النماذج وشغّل TLC:الادعاءات والأهداف
تعرّض Gateway وسوء إعداد Gateway المفتوح
الادعاء: قد يجعل الربط خارج local loopback من دون مصادقة الاختراق عن بُعد ممكنًا ويزيد نطاق التعرّض؛ ويمنع الرمز المميز أو كلمة المرور المهاجمين غير المصادق عليهم، وفقًا لافتراضات النموذج.
راجع أيضًا
docs/gateway-exposure-matrix.md في مستودع النماذج.
مسار تنفيذ Node (القدرة الأعلى خطورة)
الادعاء: يتطلبexec host=node (أ) قائمة سماح لأوامر Node بالإضافة إلى الأوامر المعلنة، و(ب) موافقة مباشرة عند إعداد ذلك؛ وتُمنح الموافقات رموزًا مميزة لمنع إعادة استخدامها، في النموذج.
مخزن الاقتران (تقييد الرسائل المباشرة)
الادعاء: تراعي طلبات الاقتران مدة الصلاحية وحدود الطلبات المعلقة.تقييد الإدخال (الإشارات وتجاوز أوامر التحكم)
الادعاء: في سياقات المجموعات التي تتطلب إشارة، لا يمكن لأمر تحكم غير مصرح به تجاوز تقييد الإشارات.التوجيه وعزل مفتاح الجلسة
الادعاء: لا تندمج الرسائل المباشرة الواردة من نظراء مختلفين في الجلسة نفسها ما لم تُربط أو تُضبط صراحةً.نماذج v1++: التزامن وإعادة المحاولة وصحة التتبّع
نماذج لاحقة تزيد دقة تمثيل أنماط الفشل الواقعية: التحديثات غير الذرية، وإعادة المحاولة، وتوزيع الرسائل.تزامن مخزن الاقتران وثبات النتائج عند التكرار
الادعاء: يفرض مخزن الاقترانMaxPending وثبات النتائج عند التكرار حتى في ظل تداخل العمليات — إذ يجب أن تكون عملية التحقق ثم الكتابة ذرية أو مقفلة، ويجب ألا ينشئ التحديث نُسخًا مكررة. وبصورة محددة: لا يمكن للطلبات المتزامنة تجاوز MaxPending لقناة ما، ولا تنشئ الطلبات أو عمليات التحديث المتكررة للزوج نفسه (channel, sender) صفوفًا معلقة فعّالة مكررة.
ترابط تتبّع الإدخال وثبات النتائج عند التكرار
الادعاء: تحافظ عملية الإدخال على ترابط التتبّع عبر التوزيع، وتكون ثابتة النتائج عند تكرار موفّر الخدمة للمحاولات. عندما يتحول حدث خارجي واحد إلى عدة رسائل داخلية، يحتفظ كل جزء بهوية التتبّع أو الحدث نفسها؛ ولا تؤدي إعادة المحاولة إلى المعالجة مرتين؛ وإذا كانت معرّفات أحداث موفّر الخدمة مفقودة، يعود إلغاء التكرار إلى مفتاح آمن (مثل معرّف التتبّع) لتجنب إسقاط الأحداث المختلفة.أسبقية dmScope في التوجيه وidentityLinks
الادعاء: يحافظ التوجيه على عزل جلسات الرسائل المباشرة افتراضيًا، ولا يدمج الجلسات إلا عند إعداده صراحةً، من خلال أسبقية القناة وروابط الهويات. تتغلب تجاوزاتdmScope الخاصة بالقناة على الإعدادات الافتراضية العامة؛ ولا تدمج identityLinks الجلسات إلا ضمن المجموعات المرتبطة صراحةً، وليس بين النظراء غير المرتبطين.