Signal का एन्क्रिप्शन AI के लिखे 65 लाख लाइन के गणितीय प्रमाण में खरा उतरा

Signal के एन्क्रिप्शन कोड के पास अब ऐसी चीज़ है जिसका दावा बहुत कम व्यापक रूप से इस्तेमाल होने वाले सॉफ़्टवेयर कर सकते हैं: गणितीय प्रमाण कि वह वही करता है जिसका वादा करता है। AI एजेंटों की एक टीम ने Signal प्रोटोकॉल चलाने वाली लाइब्रेरी libsignal की जाँच की और साबित किया कि उसकी आमने-सामने की चैट गुप्त रहती हैं, बातचीत के दूसरे छोर पर मौजूद व्यक्ति की पहचान की पुष्टि करती हैं और कुंजी चोरी हो जाने के बाद हमलावर को फिर से बाहर कर देती हैं। उन्हें कोई नई खामी नहीं मिली।

यह बात Signal के अपने उपयोगकर्ताओं से कहीं आगे तक मायने रखती है। यह प्रोटोकॉल एंड-टू-एंड एन्क्रिप्टेड मैसेजिंग का वैश्विक मानक है और इसके अलग-अलग रूप WhatsApp, Messenger और Google Messages की चैट को सुरक्षित रखते हैं। असल में जारी किए जा चुके कोड की इतनी गहराई से जाँच पहले इतनी धीमी थी कि लगभग किसी ने इसे आज़माया ही नहीं: इस क्षेत्र की सबसे बड़ी उपलब्धियों में से एक, सत्यापित ऑपरेटिंग-सिस्टम कर्नेल, तैयार करने में बीस व्यक्ति-वर्ष लगे थे। इस काम में चार हफ़्ते लगे।

Google DeepMind द्वारा बनाए गए इस टूल का नाम AlphaProof Code है। पहले मानव विशेषज्ञों और AI मॉडलों ने Signal के सुरक्षा लक्ष्यों को Lean में औपचारिक कथनों में बदला—यह गणितीय प्रमाणों के लिए बनाई गई प्रोग्रामिंग भाषा है—और हर कथन की समीक्षा एक व्यक्ति ने की। इसके बाद Gemini Carbon से संचालित 40 से 80 एजेंटों की टीमों ने प्रमाण लिखे। ये टीमें एक मशीन पर लगातार 24 से 72 घंटे तक काम करती रहीं। नतीजे में Lean की करीब 65 लाख पंक्तियाँ बनीं।

इन लाखों पंक्तियों पर किसी को भरोसा करने की ज़रूरत नहीं है। Lean का कर्नेल हर कदम की जाँच करता है और जो प्रमाण सही नहीं होता, उसे ख़ारिज कर देता है। इसलिए इससे कोई फ़र्क नहीं पड़ता कि प्रमाण किस मॉडल ने लिखा या इस दौरान उससे कितनी बार ग़लती हुई। लोगों को जिस चीज़ पर भरोसा करना है, वह इससे कहीं छोटी है: विनिर्देशों की करीब 26,000 पंक्तियाँ और ARM प्रोसेसर द्वारा कोड चलाए जाने का एक मॉडल।

ये प्रमाण Signal के उन हिस्सों को कवर करते हैं जो बातचीत की सुरक्षा करते हैं: PQXDH हैंडशेक, जो चैट शुरू करता है, और Triple Ratchet, जो हर संदेश के लिए कुंजी बदलता है। इसमें उत्तर-क्वांटम परत भी शामिल है, जिसे भविष्य के क्वांटम कंप्यूटरों से बचाव के लिए बनाया गया है। व्यवहार में इसका मतलब है कि फ़ोन की मौजूदा कुंजियाँ चुरा लेने से पुराने संदेश नहीं खुलते, और दोनों पक्षों के नई कुंजियों का आदान-प्रदान करते ही चोर की पहुँच फिर बंद हो जाती है।

यह दिखाने के लिए कि सिस्टम अच्छे और ख़राब कोड में फ़र्क कर सकता है, शोधकर्ताओं ने libsignal की दो पुरानी, पहले ही ठीक की जा चुकी खामियाँ फिर से शामिल कीं। उनमें से एक के कारण लाइब्रेरी को उस गुप्त कुंजी की एक प्रति अपने पास रखनी पड़ती थी, जिसे उसे मिटा देना चाहिए था। दोनों ही मामलों में AlphaProof Code ने मशीन से जाँचा हुआ प्रमाण तैयार किया कि खामी वाले बिल्ड में सुरक्षा नहीं थी।

इसकी सीमाएँ भी साफ़ हैं। प्रमाण केवल दो लोगों के बीच के सत्रों को कवर करता है और DeepMind ने समूह संदेशों को भविष्य के कामों में रखा है। यह libsignal के संस्करण 0.105.4 पर लागू होता है, जिसे एक छोटे परीक्षण प्रोग्राम के भीतर ARM Linux के लिए मानक Rust कंपाइलर से संकलित किया गया था; iPhone, Android या डेस्कटॉप के पूरे Signal ऐप पर नहीं। क्रिप्टोग्राफी के निचले स्तर के आधारभूत घटकों को सुरक्षित मान लिया गया है, उनका प्रमाण नहीं दिया गया। मनुष्यों द्वारा मंज़ूर किए गए विनिर्देशों में कोई ग़लती सुरक्षा की गारंटी को कमज़ोर कर सकती है। WhatsApp और दूसरे ऐप प्रोटोकॉल के अपने-अपने संस्करण चलाते हैं, इसलिए यह नतीजा उन पर अपने आप लागू नहीं होता। Google ने Wired को यह बताने से भी इनकार किया कि इस विश्लेषण पर कितना ख़र्च आया या कंपनी इसे सेवा के रूप में बेचने की योजना बना रही है या नहीं।

Signal ने इस नतीजे का स्वागत किया। Signal के मुख्य प्रौद्योगिकी अधिकारी एहरेन क्रेट (Ehren Kret) ने एक बयान में कहा, “AI से संचालित सुरक्षा ख़तरों के बढ़ने के बीच, Signal प्रोटोकॉल के कार्यान्वयन का कड़ाई से सत्यापन करने से हमें अपने कोड की गोपनीयता संबंधी गारंटियों पर और भी भरोसा होता है।” DeepMind के शोध वैज्ञानिक स्वरत चौधुरी (Swarat Chaudhuri) ने ज़्यादा सतर्क रुख़ अपनाया। उन्होंने Wired से कहा कि इस तरीके को “दुनिया के सभी सॉफ़्टवेयर” तक पहुँचाने से पहले “अभी लंबा रास्ता तय करना है।”

Signal इस्तेमाल करने वालों को कुछ इंस्टॉल करने या कोई सेटिंग बदलने की ज़रूरत नहीं है। यह प्रमाण ऐप में पहले से मौजूद कोड के बारे में है।

DeepMind ने 10 नवंबर को एक तकनीकी शोधपत्र के साथ यह काम प्रकाशित किया और विनिर्देशों तथा प्रमाणों को GitHub पर ओपन सोर्स के रूप में जारी किया। कंपनी Signal परियोजना को अप्रैल में तय की गई औपचारिक सत्यापन की एक बड़ी चुनौती की दिशा में अहम पड़ाव बताती है। साथ ही, उसने चिकित्सा उपकरणों के फ़र्मवेयर और बिजली ग्रिड के सॉफ़्टवेयर को उन प्रणालियों के उदाहरण के रूप में गिनाया है, जिनकी जाँच वह आगे करना चाहती है।

चौधुरी ने यह भी स्पष्ट किया कि इस काम का कितना हिस्सा मशीनों को सौंपना चाहिए। उन्होंने Wired से कहा, “हम ऐसी दुनिया नहीं चाहते जहाँ AI लक्ष्य तय करे और AI ही प्रमाण तैयार करे।” सुरक्षित किसे माना जाए, यह फ़ैसला अब भी मनुष्य करते हैं; AI सिर्फ़ उसका प्रमाण देता है।

टैग: साइबर सुरक्षा, Google DeepMind, AlphaProof Code, libsignal, Signal, एंड-टू-एंड एन्क्रिप्शन