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

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

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

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

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

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

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

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

मॉडल एक अलग रेपो में रखे जाते हैं: vignesh07/openclaw-formal-models।

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

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

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

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

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

शुरू करना:

git clone https://github.com/vignesh07/openclaw-formal-modelscd 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

संबंधित

• थ्रेट मॉडल
• थ्रेट मॉडल में योगदान