---
permalink: /security/formal-verification/
read_when:
    - مراجعة ضمانات أو حدود نموذج الأمان الشكلي
    - إعادة إنتاج أو تحديث عمليات التحقق من نماذج الأمان باستخدام TLA+/TLC
summary: نماذج أمان متحقق منها آليًا للمسارات الأعلى خطورة في OpenClaw.
title: التحقق الشكلي (نماذج الأمان)
x-i18n:
    generated_at: "2026-04-05T12:56:18Z"
    model: gpt-5.4
    provider: openai
    source_hash: 0f7cd2461dcc00d320a5210e50279d76a7fa84e0830c440398323d75e262a38a
    source_path: security/formal-verification.md
    workflow: 15
---

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

تتتبع هذه الصفحة **نماذج الأمان الشكلية** الخاصة بـ OpenClaw ‏(TLA+/TLC حاليًا؛ والمزيد حسب الحاجة).

> ملاحظة: قد تشير بعض الروابط الأقدم إلى الاسم السابق للمشروع.

**الهدف (البوصلة الأساسية):** تقديم حجة متحقق منها آليًا تفيد بأن OpenClaw يفرض
سياسة الأمان المقصودة لديه (التفويض، وعزل الجلسات، وتقييد الأدوات، وسلامة
سوء الإعداد)، وذلك ضمن افتراضات صريحة.

**ما الذي يمثله هذا (حاليًا):** **حزمة انحدار أمان** تنفيذية يقودها المهاجم:

- لكل ادعاء فحص نموذج قابل للتشغيل على فضاء حالات محدود.
- لدى العديد من الادعاءات **نموذج سلبي** مقترن ينتج مسار مثال مضاد لفئة أخطاء واقعية.

**ما ليس عليه هذا (حتى الآن):** برهانًا على أن “OpenClaw آمن من جميع النواحي” أو أن تنفيذ TypeScript الكامل صحيح.

## مكان وجود النماذج

تُدار النماذج في مستودع منفصل: [vignesh07/openclaw-formal-models](https://github.com/vignesh07/openclaw-formal-models).

## تنبيهات مهمة

- هذه **نماذج** وليست تنفيذ TypeScript الكامل. ومن الممكن حدوث انحراف بين النموذج والشفرة.
- النتائج مقيدة بفضاء الحالات الذي يستكشفه TLC؛ فالحالة “الخضراء” لا تعني الأمان خارج حدود الافتراضات والقيود المصاغة في النموذج.
- تعتمد بعض الادعاءات على افتراضات بيئية صريحة (مثل النشر الصحيح، وصحة مدخلات الإعدادات).

## إعادة إنتاج النتائج

حاليًا، تُعاد النتائج عبر استنساخ مستودع النماذج محليًا وتشغيل TLC (انظر أدناه). وقد يوفّر إصدار مستقبلي:

- نماذج تعمل ضمن CI مع عناصر منشورة علنًا (مسارات الأمثلة المضادة، وسجلات التشغيل)
- سير عمل مستضاف من نوع “شغّل هذا النموذج” لعمليات التحقق الصغيرة والمحدودة

للبدء:

```bash
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

**الادعاء:** يجب أن يحافظ التوجيه على عزل جلسات الرسائل الخاصة افتراضيًا، وألا يدمج الجلسات إلا عند ضبط ذلك صراحةً (أسبقية القناة + روابط الهوية).

ما الذي يعنيه ذلك:

- يجب أن تتغلب تجاوزات dmScope الخاصة بالقناة على الإعدادات الافتراضية العامة.
- يجب أن تقوم identityLinks بالدمج فقط داخل المجموعات المرتبطة صراحة، وليس عبر أقران غير ذوي صلة.

- الأخضر:
  - `make routing-precedence`
  - `make routing-identitylinks`
- الأحمر (متوقع):
  - `make routing-precedence-negative`
  - `make routing-identitylinks-negative`
