From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
यह शोध पत्र SpecMon रनटाइम मॉनिटर का उपयोग करके औपचारिक प्रोटोकॉल विनिर्देशों और वास्तविक दुनिया के कार्यान्वयन के बीच के अंतर को पाटता है ताकि यह सत्यापित किया जा सके कि व्हाट्सएप वेब और सिग्नल डेस्कटॉप के देखे गए निष्पादन नए विकसित टैमेरिन-अनुकूल (Tamarin-compatible) मॉडलों के अनुरूप हैं, जिससे सुरक्षा गुणों की पुष्टि होती है और अनुप्रयोगों के बीच अनदस्तावेजी अंतरों का अनावरण होता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने नहीं लिखा है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
डिजिटल युग में, अरबों लोग अपने सबसे निजी विचार साझा करने, अपने वित्तीय डेटा को सुरक्षित करने और अपने दैनिक जीवन को व्यवस्थित करने के लिए मैसेजिंग ऐप्स पर निर्भर हैं। इन अनुप्रयोगों (एप्लिकेशन्स) के पीछे एक जटिल नियमों का समूह होता है जिसे 'प्रोटोकॉल' कहा जाता है, जो इस बात का ब्लूप्रिंट (खाका) कार्य करता है कि संदेशों को कैसे लॉक, भेजा और अनलॉक किया जाता है। इनमें से सबसे प्रसिद्ध ब्लूप्रिंट 'सिग्नल प्रोटोकॉल' है, जो एक ऐसी प्रणाली है जिसे यह सुनिश्चित करने के लिए डिज़ाइन किया गया है कि यदि कोई हैकर संदेश को बीच में ही रोक भी ले, तो भी वह उसे पढ़ न सके। वर्षों से, सुरक्षा विशेषज्ञों ने यह सिद्ध करने के लिए शक्तिशाली कंप्यूटर टूल्स का उपयोग किया है कि यह ब्लूप्रिंट गणितीय रूप से सुदृढ़ है। उन्होंने दिखाया है कि यदि नियमों का पूरी तरह से पालन किया जाए, तो यह प्रणाली अटूट है। हालाँकि, एक ब्लूप्रिंट और एक इमारत में अंतर होता है। केवल इसलिए कि एक डिज़ाइन कागज़ पर आदर्श दिखता है, इसका मतलब यह नहीं है कि निर्माण दल ने हर निर्देश का पालन किया, सही सामग्री का उपयोग किया, या निर्माण के दौरान अनजाने गलतियों से बचा। सॉफ्टवेयर की दुनिया में, सैद्धांतिक डिज़ाइन और उपयोगकर्ता के फोन पर चलने वाले वास्तविक कोड के बीच का अंतर ही वह जगह है जहाँ अक्सर कमजोरियाँ छिपी होती हैं।
CISPA हेल्म्सहोल्ट्ज़ सेंटर फॉर इंफॉर्मेशन सिक्योरिटी के शोधकर्ताओं की एक टीम ने इस अंतर को पाटने का लक्ष्य रखा। वे यह जानना चाहते थे कि सिग्नल प्रोटोकॉल के वास्तविक संस्करण, जैसा कि वे व्हाट्सएप और सिग्नल ऐप्स के भीतर चलते हैं, वास्तव में उन सख्त नियमों का पालन करते हैं जिनका उन्हें पालन करने के लिए डिज़ाइन किया गया है। इन विशाल अनुप्रयोगों के पूरे कोडबेस को पढ़ने की कोशिश करने के बजाय—एक ऐसा कार्य जो कठिन है क्योंकि उनके कुछ हिस्से छिपे हुए या बंद (क्लोज्ड) हैं—शोधकर्ताओं ने एक विशेष 'वॉचडॉग' (निगरानी तंत्र) बनाया। यह वॉचडॉग, जिसे 'स्पेकमोन' (SpecMon) कहा जाता है, एप्लिकेशन को चलते समय देखता है, उसके नेटवर्क के साथ होने वाली हर बातचीत और उसकी सुरक्षा कुंजियों (सिक्योरिटी कीज़) के साथ किए जाने वाले हर कैलकुलेशन को सुनता है। यह लाइव क्रियाओं की तुलना वास्तविक समय में आदर्श सैद्धांतिक मॉडल से करता है। यदि एप्लिकेशन कोई शॉर्टकट लेने की, कोई कदम छोड़ने की, या ब्लूप्रिंट द्वारा अनुमत विधि से भिन्न विधि का उपयोग करने की कोशिश करता है, तो वॉचडॉग अलार्म बजा देता है।
शोधकर्ताओं ने इस पद्धति को दो प्रमुख अनुप्रयोगों पर लागू किया: सिग्नल डेस्कटॉप, जो निरीक्षण के लिए खुला है, और व्हाट्सएप वेब, जो एक विशाल निगम के स्वामित्व वाली एक बंद, प्रोप्राइटरी प्रणाली है। सिग्नल डेस्कटॉप एप्लिकेशन के लिए, उन्होंने प्रोटोकॉल के एक मौजूदा, अत्यधिक विस्तृत गणितीय मॉडल से शुरुआत की और उसमें वास्तविक सॉफ्टवेयर में पाए जाने वाले विशिष्ट, जटिल विवरण जोड़े, जैसे कि यह भविष्य के क्वांटम कंप्यूटरों का प्रतिरोध करने के लिए डिज़ाइन किए गए नए प्रकार के एन्क्रिप्शन को कैसे संभालता है। व्हाट्सएप के लिए, उन्हें उल्टा काम करना पड़ा। बिना किसी पूर्व मॉडल के शुरुआत करते हुए, उन्होंने एप्लिकेशन के व्यवहार को देखा, उसकी क्रियाओं को रिकॉर्ड किया, और शून्य से एक नया, कस्टम ब्लूप्रिंट बनाया जो बिल्कुल वैसा ही था जैसा सॉफ्टवेयर कर रहा था। यह एक महत्वपूर्ण उपलब्धि थी, क्योंकि यह पहली बार था जब व्हाट्सएप के प्रोटोकॉल के कार्यान्वयन (इम्प्लीमेंटेशन) से सीधे एक औपचारिक मॉडल तैयार किया गया था।
एक बार जब ये मॉडल तैयार हो गए, तो शोधकर्ताओं ने उनका परीक्षण किया। उन्होंने हजारों सिम्युलेटेड बातचीत चलाईं, जिसमें ऐसे परिदृश्य शामिल थे जहाँ संदेशों में देरी हुई, क्रम से बाहर भेजे गए, या जहाँ नेटवर्क कनेक्शन बाधित हुआ। हर मामले में, एप्लिकेशन ने ठीक वैसे ही व्यवहार किया जैसा कि उनके मॉडल ने भविष्यवाणी की थी, जिससे पुष्टि हुई कि मुख्य सुरक्षा तंत्र सही ढंग से कार्य कर रहे हैं। शोधकर्ताओं ने जानबूझकर सॉफ्टवेयर में त्रुटियां भी डालीं ताकि यह देख सकें कि क्या उनका वॉचडॉग उन्हें पकड़ पाता है। उन्होंने ऐप्स को पुरानी एन्क्रिप्शन कुंजियों का पुन: उपयोग करने, सिग्नेचर चेक्स को छोड़ने, या अप्रत्याशित तरीकों से गुप्त डेटा लीक करने के लिए प्रेरित किया। सिस्टम ने इन सभी सुरक्षा दोषों का पता लगा लिया, जिससे यह सिद्ध हुआ कि निगरानी उपकरण नियमों से खतरनाक विचलन को पहचानने के लिए पर्याप्त संवेदनशील है।
हालाँकि, निगरानी ने दो अनुप्रयोगों के बीच सूक्ष्म अंतर भी प्रकट किए जो तुरंत स्पष्ट नहीं थे। शोधकर्ताओं ने पाया कि व्हाट्सएप "रीड रिसीट्स" (वह सूचना जो प्रेषक को बताती है कि संदेश देखा गया है) को सिग्नल की तुलना में अलग तरह से संभालता है। सिग्नल में, ये रिसीट्स उन्हीं मजबूत एन्क्रिप्शन के भीतर लिपटे होते हैं जो संदेशों के होते हैं और सुरक्षा कुंजियों के निरंतर अपडेट में भाग लेते हैं। व्हाट्सएप में, ये रिसीट्स उस एन्क्रिप्टेड परत के बाहर भेजे जाते हैं, जिसका अर्थ है कि वे समान सुरक्षा अपडेट को ट्रिगर नहीं करते हैं। हालाँकि शोधकर्ताओं को इस अंतर के आधार पर व्हाट्सएप की सुरक्षा को तोड़ने का कोई तरीका नहीं मिला, लेकिन उन्होंने उल्लेख किया कि इसका मतलब यह है कि यदि कोई गुप्त कुंजी चोरी हो जाती है, तो एप्लिकेशन को अपनी सुरक्षा बहाल करने में अधिक समय लग सकता है। उन्होंने यह भी पुष्टि की कि व्हाट्सएप में अभी तक कुछ उन्नत गोपनीयता सुविधाएँ शामिल नहीं हैं, जैसे कि सर्वर से प्रेषक की पहचान छिपाना, जो सिग्नल ऐप में मौजूद हैं।
यह अध्ययन प्रदर्शित करता है कि वास्तविक दुनिया के जटिल सॉफ्टवेयर को चलते हुए देखना और यह सत्यापित करना संभव है कि वे अपने सुरक्षा वादों का पालन करते हैं, बिना उनके सोर्स कोड की हर एक पंक्ति को देखे। यह प्रक्रिया कुशल थी, जिसे सेटअप करने और चलाने में केवल कुछ सप्ताह लगे, और इसने अनुप्रयोगों की गति में बहुत कम देरी की। एक ऐसा सिस्टम बनाकर, जहाँ सैद्धांतिक मॉडल और लाइव मॉनिटरिंग एक ही भाषा साझा करते हैं, शोधकर्ताओं ने एक ऐसा तरीका प्रदान किया है जिससे डेवलपर्स और सुरक्षा विशेषज्ञ निरंतर यह जांच सकते हैं कि उनके अनुप्रयोग विकसित होते समय सुरक्षित रहते हैं। यह दृष्टिकोण उन डिजिटल उपकरणों में विश्वास बनाने का एक नया मार्ग प्रदान करता है जिनका हम प्रतिदिन उपयोग करते हैं, यह सुनिश्चित करते हुए कि हमारे रहने वाले भवन उतने ही सुरक्षित हैं जितने कि वे ब्लूप्रिंट जिनसे उन्हें बनाया गया है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।