> ## Documentation Index
> Fetch the complete documentation index at: https://docs2.openclaw.ai/llms.txt
> Use this file to discover all available pages before exploring further.

# औपचारिक सत्यापन (सुरक्षा मॉडल)

यह पृष्ठ OpenClaw के **औपचारिक सुरक्षा मॉडल** को ट्रैक करता है (आज TLA+/TLC; आवश्यकता अनुसार और भी)।

> नोट: कुछ पुराने लिंक पिछले प्रोजेक्ट नाम का संदर्भ दे सकते हैं।

**लक्ष्य (मुख्य दिशा):** स्पष्ट मान्यताओं के अंतर्गत यह मशीन-जाँचा तर्क देना कि OpenClaw अपनी
अभिप्रेत सुरक्षा नीति (प्राधिकरण, सत्र पृथक्करण, टूल गेटिंग, और
गलत कॉन्फिगरेशन से सुरक्षा) लागू करता है।

**यह क्या है (आज):** एक निष्पादन योग्य, हमलावर-चालित **सुरक्षा रिग्रेशन सूट**:

* प्रत्येक दावे में सीमित अवस्था-स्थान पर चलाने योग्य मॉडल-जाँच है।
* कई दावों के साथ एक युग्मित **नकारात्मक मॉडल** है, जो यथार्थवादी बग वर्ग के लिए प्रति-उदाहरण ट्रेस उत्पन्न करता है।

**यह क्या नहीं है (अभी):** यह प्रमाण नहीं कि "OpenClaw हर दृष्टि से सुरक्षित है" या कि पूरा TypeScript कार्यान्वयन सही है।

## मॉडल कहाँ रहते हैं

मॉडल एक अलग रेपो में रखे जाते हैं: [vignesh07/openclaw-formal-models](https://github.com/vignesh07/openclaw-formal-models)।

## महत्वपूर्ण सावधानियाँ

* ये **मॉडल** हैं, पूरा TypeScript कार्यान्वयन नहीं। मॉडल और कोड के बीच विचलन संभव है।
* परिणाम TLC द्वारा खोजे गए अवस्था-स्थान तक सीमित हैं; "हरा" मॉडल की गई मान्यताओं और सीमाओं से परे सुरक्षा का संकेत नहीं देता।
* कुछ दावे स्पष्ट परिवेशीय मान्यताओं पर निर्भर करते हैं (जैसे, सही डिप्लॉयमेंट, सही कॉन्फिगरेशन इनपुट)।

## परिणाम दोहराना

आज, परिणाम स्थानीय रूप से मॉडल रेपो क्लोन करके और TLC चलाकर दोहराए जाते हैं (नीचे देखें)। भविष्य का संस्करण यह दे सकता है:

* सार्वजनिक आर्टिफैक्ट्स (प्रति-उदाहरण ट्रेस, रन लॉग) के साथ CI-चलित मॉडल
* छोटे, सीमित चेक के लिए होस्ट किया गया "यह मॉडल चलाएँ" वर्कफ़्लो

शुरू करना:

```bash theme={"theme":{"light":"min-light","dark":"min-dark"}}
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>
```

### Gateway एक्सपोज़र और खुले Gateway का गलत कॉन्फिगरेशन

**दावा:** प्रमाणीकरण के बिना loopback से आगे bind करने से दूरस्थ समझौता संभव हो सकता है / एक्सपोज़र बढ़ता है; token/password अनधिकृत हमलावरों को रोकते हैं (मॉडल की मान्यताओं के अनुसार)।

* सफल रन:
  * `make gateway-exposure-v2`
  * `make gateway-exposure-v2-protected`
* असफल (अपेक्षित):
  * `make gateway-exposure-v2-negative`

यह भी देखें: मॉडल रेपो में `docs/gateway-exposure-matrix.md`।

### Node exec पाइपलाइन (सबसे अधिक जोखिम वाली क्षमता)

**दावा:** `exec host=node` के लिए (a) node कमांड allowlist और घोषित कमांड, तथा (b) कॉन्फिगर किए जाने पर लाइव अनुमोदन आवश्यक है; अनुमोदनों को replay रोकने के लिए tokenized किया जाता है (मॉडल में)।

* सफल रन:
  * `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`

### Ingress गेटिंग (mentions + control-command bypass)

**दावा:** mention की आवश्यकता वाले समूह संदर्भों में, अनधिकृत "control command" mention गेटिंग को bypass नहीं कर सकता।

* सफल:
  * `make ingress-gating`
* असफल (अपेक्षित):
  * `make ingress-gating-negative`

### रूटिंग/सत्र-कुंजी पृथक्करण

**दावा:** अलग-अलग peers से आने वाले DMs उसी सत्र में collapse नहीं होते, जब तक कि उन्हें स्पष्ट रूप से linked/configured न किया गया हो।

* सफल:
  * `make routing-isolation`
* असफल (अपेक्षित):
  * `make routing-isolation-negative`

## v1++: अतिरिक्त सीमित मॉडल (concurrency, retries, trace correctness)

ये follow-on मॉडल हैं, जो वास्तविक दुनिया के failure modes (non-atomic updates, retries, और message fan-out) के आसपास fidelity को कसते हैं।

### पेयरिंग स्टोर concurrency / idempotency

**दावा:** पेयरिंग स्टोर को interleavings के तहत भी `MaxPending` और idempotency लागू करनी चाहिए (अर्थात, "check-then-write" atomic / locked होना चाहिए; refresh से duplicates नहीं बनने चाहिए)।

इसका अर्थ:

* concurrent requests के तहत, आप किसी channel के लिए `MaxPending` से अधिक नहीं जा सकते।

* उसी `(channel, sender)` के लिए repeated requests/refreshes से duplicate live pending rows नहीं बनने चाहिए।

* सफल रन:
  * `make pairing-race` (atomic/locked cap check)
  * `make pairing-idempotency`
  * `make pairing-refresh`
  * `make pairing-refresh-race`

* असफल (अपेक्षित):
  * `make pairing-race-negative` (non-atomic begin/commit cap race)
  * `make pairing-idempotency-negative`
  * `make pairing-refresh-negative`
  * `make pairing-refresh-race-negative`

### Ingress trace correlation / idempotency

**दावा:** ingestion को fan-out के दौरान trace correlation बनाए रखना चाहिए और provider retries के तहत idempotent होना चाहिए।

इसका अर्थ:

* जब एक external event कई internal messages बनता है, तो हर भाग वही trace/event identity बनाए रखता है।

* retries से double-processing नहीं होती।

* यदि provider event IDs अनुपस्थित हैं, तो अलग-अलग events को drop करने से बचने के लिए dedupe सुरक्षित key (जैसे, trace ID) पर fallback करता है।

* सफल:
  * `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`

### Routing dmScope precedence + identityLinks

**दावा:** routing को default रूप से DM sessions को isolated रखना चाहिए, और sessions को केवल स्पष्ट रूप से configured होने पर collapse करना चाहिए (channel precedence + identity links)।

इसका अर्थ:

* Channel-specific dmScope overrides को global defaults पर प्राथमिकता मिलनी चाहिए।

* identityLinks को केवल स्पष्ट linked groups के भीतर collapse करना चाहिए, unrelated peers के बीच नहीं।

* सफल:
  * `make routing-precedence`
  * `make routing-identitylinks`

* असफल (अपेक्षित):
  * `make routing-precedence-negative`
  * `make routing-identitylinks-negative`

## संबंधित

* [थ्रेट मॉडल](/hi/security/THREAT-MODEL-ATLAS)
* [थ्रेट मॉडल में योगदान](/hi/security/CONTRIBUTING-THREAT-MODEL)