ध्यान दें: कुछ पुराने लिंक पिछले प्रोजेक्ट नाम का उल्लेख कर सकते हैं।
यह क्या है
एक निष्पादन योग्य, हमलावर-संचालित सुरक्षा रिग्रेशन सुइट:- प्रत्येक दावे के लिए एक सीमित अवस्था-स्थान पर चलाया जा सकने वाला मॉडल-जाँच परीक्षण है।
- कई दावों के साथ एक युग्मित नकारात्मक मॉडल है, जो वास्तविक बग श्रेणी के लिए प्रति-उदाहरण ट्रेस उत्पन्न करता है।
मॉडल कहाँ स्थित हैं
मॉडल एक अलग रेपो में अनुरक्षित हैं: vignesh07/openclaw-formal-models।यह रेपो वर्तमान में पहुँच योग्य नहीं है (इसे लिखे जाने के समय GitHub “Repository not found” लौटाता है)। यदि यह आपके लिए अब भी अनुपलब्ध है, तो यह मानने से पहले कि मॉडल हटा दिए गए हैं, वर्तमान स्थान के लिए OpenClaw अनुरक्षक चैनलों में पूछें।
सीमाएँ
- ये मॉडल हैं, संपूर्ण TypeScript कार्यान्वयन नहीं — मॉडल और कोड के बीच अंतर संभव है।
- परिणाम उस अवस्था-स्थान से सीमित हैं जिसे TLC खोजता है। हरा परिणाम मॉडल की गई मान्यताओं और सीमाओं से परे सुरक्षा को इंगित नहीं करता।
- कुछ दावे स्पष्ट परिवेश मान्यताओं पर निर्भर हैं (उदाहरण के लिए, सही परिनियोजन और सही कॉन्फ़िगरेशन इनपुट)।
परिणामों को पुनरुत्पादित करना
मॉडल रेपो को क्लोन करें और TLC चलाएँ:दावे और लक्ष्य
Gateway का एक्सपोज़र और खुले Gateway का गलत कॉन्फ़िगरेशन
दावा: प्रमाणीकरण के बिना लूपबैक से परे बाइंड करने से दूरस्थ समझौता संभव हो सकता है और एक्सपोज़र बढ़ता है; मॉडल की मान्यताओं के अनुसार, टोकन/पासवर्ड अप्रमाणित हमलावरों को रोकता है।
मॉडल रेपो में
docs/gateway-exposure-matrix.md भी देखें।
Node निष्पादन पाइपलाइन (सर्वाधिक-जोखिम वाली क्षमता)
दावा: मॉडल मेंexec host=node के लिए (a) घोषित कमांड के साथ Node कमांड अनुमति-सूची और (b) कॉन्फ़िगर होने पर लाइव अनुमोदन आवश्यक हैं; दोबारा उपयोग रोकने के लिए अनुमोदनों को टोकनयुक्त किया जाता है।
पेयरिंग स्टोर (DM गेटिंग)
दावा: पेयरिंग अनुरोध TTL और लंबित अनुरोधों की सीमाओं का पालन करते हैं।इनग्रेस गेटिंग (उल्लेख और नियंत्रण-कमांड बायपास)
दावा: उल्लेख आवश्यक करने वाले समूह संदर्भों में, कोई अनधिकृत नियंत्रण कमांड उल्लेख गेटिंग को बायपास नहीं कर सकता।रूटिंग और सत्र-कुंजी पृथक्करण
दावा: अलग-अलग पीयर से प्राप्त DM एक ही सत्र में तब तक नहीं मिलते, जब तक उन्हें स्पष्ट रूप से लिंक या कॉन्फ़िगर न किया गया हो।v1++ मॉडल: समवर्तीता, पुनः प्रयास और ट्रेस शुद्धता
वास्तविक दुनिया के विफलता मोडों के संबंध में सटीकता बढ़ाने वाले अनुवर्ती मॉडल: गैर-परमाण्विक अपडेट, पुनः प्रयास और संदेश फैन-आउट।पेयरिंग स्टोर की समवर्तीता और आइडेम्पोटेंसी
दावा: पेयरिंग स्टोर इंटरलीविंग के दौरान भीMaxPending और आइडेम्पोटेंसी लागू करता है — जाँच-फिर-लेखन परमाण्विक/लॉक किया हुआ होना चाहिए और रीफ़्रेश से डुप्लिकेट नहीं बनने चाहिए। ठोस रूप में: समवर्ती अनुरोध किसी चैनल के लिए MaxPending से अधिक नहीं हो सकते और एक ही (channel, sender) के बार-बार अनुरोध/रीफ़्रेश से डुप्लिकेट सक्रिय लंबित पंक्तियाँ नहीं बनतीं।
इनग्रेस ट्रेस सहसंबंध और आइडेम्पोटेंसी
दावा: इनजेशन पूरे फैन-आउट में ट्रेस सहसंबंध बनाए रखता है और प्रदाता के पुनः प्रयासों के दौरान आइडेम्पोटेंट रहता है। जब एक बाहरी घटना कई आंतरिक संदेश बन जाती है, तो हर भाग समान ट्रेस/घटना पहचान बनाए रखता है; पुनः प्रयास से दोहरा प्रसंस्करण नहीं होता; यदि प्रदाता घटना ID अनुपलब्ध हों, तो अलग-अलग घटनाओं को हटने से बचाने के लिए डीडुप्लिकेशन किसी सुरक्षित कुंजी (उदाहरण के लिए ट्रेस ID) का उपयोग करता है।रूटिंग dmScope प्राथमिकता और identityLinks
दावा:dmScope प्राथमिकता और पहचान लिंक नियतात्मक रूप से व्यवहार करते हैं: डिफ़ॉल्ट main स्कोप एकल स्वामी के DM के बीच एक क्रमिक सत्र साझा करता है (व्यक्तिगत-एजेंट डिफ़ॉल्ट), जबकि कॉन्फ़िगर किया गया कोई भी पृथक्कारी स्कोप (per-peer, per-channel-peer, per-account-channel-peer) DM सत्रों को सख्ती से अलग रखता है। चैनल-विशिष्ट dmScope ओवरराइड वैश्विक डिफ़ॉल्ट पर प्राथमिकता पाते हैं; identityLinks सत्रों को केवल स्पष्ट रूप से लिंक किए गए समूहों के भीतर मिलाते हैं, असंबंधित पीयर के बीच नहीं। बहु-उपयोगकर्ता इनबॉक्स से किसी पृथक्कारी स्कोप को चुनने की अपेक्षा की जाती है (बहु-उपयोगकर्ता DM ट्रैफ़िक का पता चलने पर रनटाइम सुरक्षा ऑडिट इसकी अनुशंसा करता है)।