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

​
التحقق الشكلي (نماذج الأمان)

تتتبع هذه الصفحة نماذج الأمان الشكلية الخاصة بـ 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+ required (TLC runs on the JVM).
# The repo vendors a pinned `tla2tools.jar` (TLA+ tools) and provides `bin/tlc` + Make targets.

make <target>

​
تعريض البوابة وسوء إعداد البوابة المفتوحة

الادعاء: يمكن أن يؤدي الربط خارج local loopback من دون مصادقة إلى جعل الاختراق عن بُعد ممكنًا / زيادة التعرض؛ ويمنع الرمز/كلمة المرور المهاجمين غير المصادقين (وفقًا لافتراضات النموذج).
  • التشغيلات الخضراء:
    • make gateway-exposure-v2
    • make gateway-exposure-v2-protected
  • الأحمر (متوقع):
    • make gateway-exposure-v2-negative
راجع أيضًا: docs/gateway-exposure-matrix.md في مستودع النماذج.

​
مسار تنفيذ العقدة (أعلى القدرات خطورة)

الادعاء: يتطلب exec host=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 (سباق حد أقصى غير ذري بين begin/commit)
    • 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 بالدمج فقط داخل المجموعات المرتبطة صراحة، وليس عبر أقران غير ذوي صلة.
  • الأخضر:
    • make routing-precedence
    • make routing-identitylinks
  • الأحمر (متوقع):
    • make routing-precedence-negative
    • make routing-identitylinks-negative