Towards System-Oriented Formal Verification of Local-First Access Control
यह शोध पत्र एक क्षमता-आधारित (capability-based) प्रतिकृति डेटा प्रकार (replicated data type) के लिए सत्यापित अर्थ और अपरिवर्तनीयता (invariants) विकसित करने हेतु Rust-आधारित Verus फ्रेमवर्क का उपयोग करके, बायज़ेंटाइन फॉल्ट-टॉलरेंट, लोकल-फर्स्ट सिस्टम में एक्सेस कंट्रोल के औपचारिक सत्यापन के लिए एक बॉटम-अप दृष्टिकोण प्रस्तुत करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप और आपके दोस्तों का एक समूह एक साझा डिजिटल नोटबुक पर सहयोग करने की कोशिश कर रहे हैं। हालाँकि, इसके बजाय कि हर कोई एक विशाल केंद्रीय सर्वर (जैसे गूगल डॉक्स) में लॉग इन करे, प्रत्येक व्यक्ति के पास अपने स्वयं के डिवाइस पर नोटबुक की अपनी निजी प्रति है। आप केवल तभी एक-दूसरे के साथ सिंक करते हैं जब आपके पास इंटरनेट कनेक्शन होता है।
इसे "लोकल-फर्स्ट" (Local-First) सॉफ्टवेयर कहा जाता है। यह शानदार है क्योंकि यह तेज़ है और ऑफलाइन काम करता है, लेकिन यह एक बहुत बड़ी सिरदर्दी पैदा करता है: यदि कोई "बॉस" (केंद्रीय सर्वर) निगरानी नहीं कर रहा है, तो आप यह कैसे नियंत्रित करेंगे कि कौन क्या संपादित (edit) कर सकता है?
यह शोध पत्र इस बात की खोज करता है कि कैसे इन विकेंद्रीकृत प्रणालियों के लिए एक "डिजिटल सुरक्षा गार्ड" बनाने के लिए उन्नत गणित और कंप्यूटर विज्ञान का उपयोग किया जाए, जो अनहैकेबल (unhackable) भी हो और अविश्वसनीय रूप से स्मार्ट भी।
समस्या: "ग्रुप चैट में अराजकता"
एक सामान्य प्रणाली में (जैसे फेसबुक), यदि आप किसी को समूह से बाहर निकालते हैं, तो केंद्रीय सर्वर कहता है, "तुम बाहर हो!" और सभी को तुरंत पता चल जाता है।
एक लोकल-फर्स्ट प्रणाली में, कोई केंद्रीय सर्वर नहीं होता है। कल्पना कीजिए कि एक ग्रुप चैट है जहाँ:
- चालाक दोस्त (बाइज़ेंटाइन फॉल्ट्स - Byzantine Faults): समूह में एक व्यक्ति दुर्भावनापूर्ण व्यवहार कर रहा है। वे संदेश को "बैकडेट" करने की कोशिश कर सकते हैं, यह दिखावा करते हुए कि उन्होंने आज आपके द्वारा बनाए गए नियम को उलटने के लिए कल एक कमांड भेजा था।
- समय यात्री (कन्करेंसी - Concurrency): दो लोग ठीक एक ही समय पर कुछ करते हैं। व्यक्ति A, चार्ली को "एडिटर" के अधिकार देता है, लेकिन ठीक उसी क्षण, व्यक्ति B चार्ली के अधिकार वापस ले लेता है। क्योंकि वहां कोई केंद्रीय घड़ी नहीं है, समूह के अलग-अलग लोगों को वास्तविकता के अलग-अलग संस्करण दिखाई दे सकते हैं।
एक सख्त गणितीय योजना के बिना, समूह के "नियम" अंततः टूट जाएंगे, और नोटबुक विरोधाभासी अनुमतियों (permissions) का ढेर बन जाएगी।
समाधान: "गणितीय नियम पुस्तिका"
शोधकर्ताओं ने केवल कोड नहीं लिखा; उन्होंने एक औपचारिक विनिर्देश (formal specification) लिखा। इसे ऐसे समझें जैसे कि किसी सूक्ष्म ब्रह्मांड के भौतिकी के नियमों को लिखना। यह कहने के बजाय कि, "यह सुनिश्चित करने की कोशिश करें कि केवल एडमिन ही नाम बदल सके," उन्होंने एक गणितीय सूत्र लिखा जो हर संभावित परिदृश्य में यह परिभाषित करता है कि "एडमिन" और "बदलना" का सटीक अर्थ क्या है।
उन्होंने तीन मुख्य "ब्रह्मांड के नियमों" पर ध्यान केंद्रित किया:
- प्राधिकरण सुरक्षा (Authorization Safety): एक बार जब कोई नियम पत्थर की लकीर बन जाता है (जैसे समूह का निर्माण), तो उसे बेतरतीब ढंग से नहीं बदला जाना चाहिए।
- क्वेरी सुरक्षा (Query Safety): यदि आप सिस्टम से पूछते हैं, "एडमिन कौन है?", तो उत्तर केवल तभी बदलना चाहिए जब वास्तव में किसी अधिकृत क्रिया को निष्पादित किया गया हो।
- निरसन सुरक्षा (Revocation Safety): यदि कोई अनुमति वापस ली जाती है, तो वह वापस ली हुई ही रहनी चाहिए, भले ही कोई "चालाक दोस्त" यह दिखाने की कोशिश करे कि निरसन (revocation) कभी हुआ ही नहीं था।
उपकरण: "सुपर-पावर्ड माइक्रोस्कोप" (Verus)
यह सुनिश्चित करने के लिए कि उनका कोड वास्तव में इन नियमों का पालन करता है, उन्होंने Verus नामक एक उपकरण का उपयोग किया।
मान लीजिए कि नियमित प्रोग्रामिंग एक घर बनाने जैसा है और यह उम्मीद करना है कि वह गिर न जाए। Verus का उपयोग करना एक उच्च-तकनीकी सिम्युलेटर के भीतर घर बनाने जैसा है जो घर में कदम रखने से पहले ही गुरुत्वाकर्षण और हवा की गति के नियमों के विरुद्ध संरचना के हर परमाणु का परीक्षण करता है। यदि "चालाक दोस्त" द्वारा नियम तोड़ने की 0.00001% भी संभावना है, तो सिम्युलेटर (थ्योरम प्रूवर) इंजीनियरों पर तब तक चिल्लाता रहेगा जब तक वे इसे ठीक नहीं कर देते।
यह क्यों मायने रखता है
शोधकर्ता एक "बॉटम-अप" दृष्टिकोण अपना रहे हैं। वे एक बार में पूरे इंटरनेट को ठीक करने की कोशिश नहीं कर रहे हैं। इसके बजाय, वे एक छोटा, पूरी तरह से सत्यापित "बिल्डिंग ब्लॉक" बना रहे हैं।
यदि वे यह सिद्ध कर सकते हैं कि यह छोटा सा ब्लॉक अविनाशी है और नियमों का पूरी तरह से पालन करता है, तो वे अंततः इन ब्लॉक्स को एक साथ जोड़कर विशाल, सुरक्षित, विकेंद्रीकृत प्रणालियाँ बना सकते हैं—जैसे कि एक विकेंद्रीकृत विकिपीडिया या एक सुपर-सुरक्षित मैसेजिंग ऐप (जैसे मैट्रिक्स) जिसका उपयोग सरकारें या अस्पताल भी बिना इस चिंता के कर सकें कि कोई एक बुरा तत्व समूह के नियमों को तोड़ सकता है।
संक्षेप में: वे एक ऐसी दुनिया के लिए गणितीय ब्लूप्रिंट बना रहे हैं जहाँ हम हमें नियंत्रण में रखने के लिए किसी "बिग ब्रदर" सर्वर की आवश्यकता के बिना स्वतंत्र रूप से सहयोग कर सकते हैं।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।