Security
औपचारिक सत्यापन (सुरक्षा मॉडल)
OpenClaw के औपचारिक सुरक्षा मॉडल (वर्तमान में TLA+/TLC) मशीन द्वारा जाँचा गया यह तर्क प्रस्तुत करते हैं कि स्पष्ट रूप से बताई गई मान्यताओं के अंतर्गत विशिष्ट सर्वाधिक-जोखिम वाले पथ — प्राधिकरण, सत्र पृथक्करण, टूल गेटिंग और गलत कॉन्फ़िगरेशन से सुरक्षा — अपनी अभिप्रेत नीति लागू करते हैं।
ध्यान दें: कुछ पुराने लिंक पिछले प्रोजेक्ट नाम का उल्लेख कर सकते हैं।
यह क्या है
एक निष्पादन योग्य, हमलावर-संचालित सुरक्षा रिग्रेशन सुइट:
- प्रत्येक दावे के लिए एक सीमित अवस्था-स्थान पर चलाया जा सकने वाला मॉडल-जाँच परीक्षण है।
- कई दावों के साथ एक युग्मित नकारात्मक मॉडल है, जो वास्तविक बग श्रेणी के लिए प्रति-उदाहरण ट्रेस उत्पन्न करता है।
यह इस बात का प्रमाण नहीं है कि OpenClaw हर दृष्टि से सुरक्षित है, और यह संपूर्ण TypeScript कार्यान्वयन को सत्यापित नहीं करता।
मॉडल कहाँ स्थित हैं
मॉडल एक अलग रेपो में अनुरक्षित हैं: vignesh07/openclaw-formal-models।
सीमाएँ
- ये मॉडल हैं, संपूर्ण TypeScript कार्यान्वयन नहीं — मॉडल और कोड के बीच अंतर संभव है।
- परिणाम उस अवस्था-स्थान से सीमित हैं जिसे TLC खोजता है। हरा परिणाम मॉडल की गई मान्यताओं और सीमाओं से परे सुरक्षा को इंगित नहीं करता।
- कुछ दावे स्पष्ट परिवेश मान्यताओं पर निर्भर हैं (उदाहरण के लिए, सही परिनियोजन और सही कॉन्फ़िगरेशन इनपुट)।
परिणामों को पुनरुत्पादित करना
मॉडल रेपो को क्लोन करें और TLC चलाएँ:
git clone https://github.com/vignesh07/openclaw-formal-modelscd 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 |
