---
permalink: /security/formal-verification/
read_when:
    - औपचारिक सुरक्षा मॉडल की गारंटियों या सीमाओं की समीक्षा करना
    - TLA+/TLC सुरक्षा मॉडल जाँचों को पुनरुत्पादित या अपडेट करना
summary: OpenClaw के सर्वाधिक जोखिम वाले पथों के लिए मशीन द्वारा सत्यापित सुरक्षा मॉडल।
title: औपचारिक सत्यापन (सुरक्षा मॉडल)
x-i18n:
    generated_at: "2026-07-27T18:32:31Z"
    model: gpt-5.6
    postprocess_version: locale-links-v1
    prompt_version: 32
    provider: openai
    source_hash: 185ee5c1cff7325f10827330c0c7e55ddc3ca40caf6088d4c930ae5e090d6b27
    source_path: security/formal-verification.md
    workflow: 16
---

OpenClaw के औपचारिक सुरक्षा मॉडल (वर्तमान में TLA+/TLC) मशीन द्वारा जाँचा गया यह तर्क प्रस्तुत करते हैं कि स्पष्ट रूप से बताई गई मान्यताओं के अंतर्गत विशिष्ट सर्वाधिक-जोखिम वाले पथ — प्राधिकरण, सत्र पृथक्करण, टूल गेटिंग और गलत कॉन्फ़िगरेशन से सुरक्षा — अपनी अभिप्रेत नीति लागू करते हैं।

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

## यह क्या है

एक निष्पादन योग्य, हमलावर-संचालित सुरक्षा रिग्रेशन सुइट:

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

यह इस बात का प्रमाण **नहीं** है कि OpenClaw हर दृष्टि से सुरक्षित है, और यह संपूर्ण TypeScript कार्यान्वयन को सत्यापित नहीं करता।

## मॉडल कहाँ स्थित हैं

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

<Note>
यह रेपो वर्तमान में पहुँच योग्य नहीं है (इसे लिखे जाने के समय GitHub "Repository not found" लौटाता है)। यदि यह आपके लिए अब भी अनुपलब्ध है, तो यह मानने से पहले कि मॉडल हटा दिए गए हैं, वर्तमान स्थान के लिए OpenClaw अनुरक्षक चैनलों में पूछें।
</Note>

## सीमाएँ

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

## परिणामों को पुनरुत्पादित करना

मॉडल रेपो को क्लोन करें और TLC चलाएँ:

```bash
git clone https://github.com/vignesh07/openclaw-formal-models
cd openclaw-formal-models

# Java 11+ आवश्यक है (TLC JVM पर चलता है)।
# रेपो में पिन किया हुआ tla2tools.jar शामिल है और यह bin/tlc तथा Make लक्ष्य प्रदान करता है।

make <target>
```

अभी इस रेपो में वापस कोई CI एकीकरण नहीं है; भविष्य के पुनरावर्तन में सार्वजनिक आर्टिफ़ैक्ट (प्रति-उदाहरण ट्रेस, रन लॉग) वाले CI-संचालित मॉडल या छोटे सीमित परीक्षणों के लिए होस्ट किया गया "यह मॉडल चलाएँ" कार्यप्रवाह जोड़ा जा सकता है।

## दावे और लक्ष्य

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

**दावा:** प्रमाणीकरण के बिना लूपबैक से परे बाइंड करने से दूरस्थ समझौता संभव हो सकता है और एक्सपोज़र बढ़ता है; मॉडल की मान्यताओं के अनुसार, टोकन/पासवर्ड अप्रमाणित हमलावरों को रोकता है।

| परिणाम         | लक्ष्य                                                          |
| -------------- | ---------------------------------------------------------------- |
| हरा          | `make gateway-exposure-v2`, `make gateway-exposure-v2-protected` |
| लाल (अपेक्षित) | `make gateway-exposure-v2-negative`                              |

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

### Node निष्पादन पाइपलाइन (सर्वाधिक-जोखिम वाली क्षमता)

**दावा:** मॉडल में `exec host=node` के लिए (a) घोषित कमांड के साथ Node कमांड अनुमति-सूची और (b) कॉन्फ़िगर होने पर लाइव अनुमोदन आवश्यक हैं; दोबारा उपयोग रोकने के लिए अनुमोदनों को टोकनयुक्त किया जाता है।

| परिणाम         | लक्ष्य                                                         |
| -------------- | --------------------------------------------------------------- |
| हरा          | `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` |

### इनग्रेस गेटिंग (उल्लेख और नियंत्रण-कमांड बायपास)

**दावा:** उल्लेख आवश्यक करने वाले समूह संदर्भों में, कोई अनधिकृत नियंत्रण कमांड उल्लेख गेटिंग को बायपास नहीं कर सकता।

| परिणाम         | लक्ष्य                        |
| -------------- | ------------------------------ |
| हरा          | `make ingress-gating`          |
| लाल (अपेक्षित) | `make ingress-gating-negative` |

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

**दावा:** अलग-अलग पीयर से प्राप्त DM एक ही सत्र में तब तक नहीं मिलते, जब तक उन्हें स्पष्ट रूप से लिंक या कॉन्फ़िगर न किया गया हो।

| परिणाम         | लक्ष्य                           |
| -------------- | --------------------------------- |
| हरा          | `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` |

### इनग्रेस ट्रेस सहसंबंध और आइडेम्पोटेंसी

**दावा:** इनजेशन पूरे फैन-आउट में ट्रेस सहसंबंध बनाए रखता है और प्रदाता के पुनः प्रयासों के दौरान आइडेम्पोटेंट रहता है। जब एक बाहरी घटना कई आंतरिक संदेश बन जाती है, तो हर भाग समान ट्रेस/घटना पहचान बनाए रखता है; पुनः प्रयास से दोहरा प्रसंस्करण नहीं होता; यदि प्रदाता घटना ID अनुपलब्ध हों, तो अलग-अलग घटनाओं को हटने से बचाने के लिए डीडुप्लिकेशन किसी सुरक्षित कुंजी (उदाहरण के लिए ट्रेस ID) का उपयोग करता है।

| परिणाम         | लक्ष्य                                                                                                                                     |
| -------------- | ------------------------------------------------------------------------------------------------------------------------------------------- |
| हरा          | `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` प्राथमिकता और पहचान लिंक नियतात्मक रूप से व्यवहार करते हैं: डिफ़ॉल्ट `main` स्कोप एकल स्वामी के DM के बीच एक क्रमिक सत्र साझा करता है (व्यक्तिगत-एजेंट डिफ़ॉल्ट), जबकि कॉन्फ़िगर किया गया कोई भी पृथक्कारी स्कोप (`per-peer`, `per-channel-peer`, `per-account-channel-peer`) DM सत्रों को सख्ती से अलग रखता है। चैनल-विशिष्ट `dmScope` ओवरराइड वैश्विक डिफ़ॉल्ट पर प्राथमिकता पाते हैं; `identityLinks` सत्रों को केवल स्पष्ट रूप से लिंक किए गए समूहों के भीतर मिलाते हैं, असंबंधित पीयर के बीच नहीं। बहु-उपयोगकर्ता इनबॉक्स से किसी पृथक्कारी स्कोप को चुनने की अपेक्षा की जाती है (बहु-उपयोगकर्ता DM ट्रैफ़िक का पता चलने पर रनटाइम सुरक्षा ऑडिट इसकी अनुशंसा करता है)।

| परिणाम         | लक्ष्य                                                                   |
| -------------- | ------------------------------------------------------------------------- |
| हरा          | `make routing-precedence`, `make routing-identitylinks`                   |
| लाल (अपेक्षित) | `make routing-precedence-negative`, `make routing-identitylinks-negative` |

## संबंधित

- [खतरा मॉडल](/hi/security/THREAT-MODEL-ATLAS)
- [खतरा मॉडल में योगदान देना](/hi/security/CONTRIBUTING-THREAT-MODEL)
- [घटना प्रतिक्रिया](/hi/security/incident-response)