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 المفتوح
الادعاء: قد يجعل الربط خارج local 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 |
مخزن الاقتران (تقييد الرسائل المباشرة)
الادعاء: تراعي طلبات الاقتران مدة الصلاحية وحدود الطلبات المعلقة.
| النتيجة | الأهداف |
|---|---|
| ناجح | 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 |
