मुख्य सामग्री पर जाएं
यह पृष्ठ 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>

​
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 को 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

​
संबंधित