Google DeepMind ने Signal के मुख्य मशीन कोड की जाँच के लिए AI एजेंटों का इस्तेमाल किया

Google DeepMind ने 10 नवंबर, 2026 को AlphaProof Code पेश किया। इसके तहत AI एजेंटों की टीमों ने Signal के संकलित libsignal कोड में सुरक्षा के निर्दिष्ट गुणों के लिए Lean के ऐसे प्रमाण तैयार किए जिन्हें मशीन से जाँचा जा सकता है। पाँच सदस्यों वाली शोध टीम ने चार हफ्तों में प्रमाणों का काम पूरा किया और बाहरी समीक्षा के लिए अपने विनिर्देश और सत्यापन संबंधी सामग्री जारी की।

यह काम Signal के प्रोटोकॉल डिज़ाइन के अमूर्त मॉडल से आगे बढ़कर उसके संकलित कार्यान्वयन तक पहुँचा। शोधकर्ताओं ने बिना किसी बदलाव वाले libsignal v0.105.4 और SPQR v1.6.0 क्रेट को एक छोटे कमांड-लाइन हार्नेस में शामिल किया। फिर मानक rustc का इस्तेमाल करके एक स्थिर रूप से लिंक किया गया AArch64 Linux एक्ज़ीक्यूटेबल बनाया। इस तकनीकी शोधपत्र के अनुसार, यह व्यापक रूप से इस्तेमाल किए जाने वाले क्रिप्टोग्राफ़िक प्रोटोकॉल के कार्यान्वयन के बिना बदलाव वाले कोड के लिए प्रोटोकॉल-स्तर पर सुरक्षा के पहले प्रमाण हैं।

AlphaProof Code ने काम को कैसे बाँटा

पाँच शोधकर्ताओं ने प्रमाणों के काम में चार हफ्ते लगाए। इस दौरान उन्होंने अपने वर्कस्टेशन पर एजेंटों को लगातार चलाया और प्रतीकात्मक तथा संगणकीय प्रमाणों पर समानांतर रूप से काम किया। शोधपत्र के अनुसार, एजेंटों ने मशीन से जाँचे गए Lean प्रमाण कोड की लगभग 6.5 मिलियन पंक्तियाँ तैयार कीं। ये प्रमाण लगभग 26,000 पंक्तियों के विश्वसनीय विनिर्देशों और AArch64 की अर्थ-संरचना पर आधारित थे।

मनुष्यों ने गुणों का चयन किया, अस्पष्टताओं और सुरक्षा संबंधी समझौतों का समाधान किया, विनिर्देशों की समीक्षा की और अंतिम मंज़ूरी का अधिकार अपने पास रखा। Gemini 4 Carbon और Claude Opus 5.5 पर चलने वाले एजेंटों ने उन विनिर्देशों का मसौदा तैयार किया और उनकी समीक्षा की; समीक्षा में एक अलग मॉडल परिवार के एजेंट भी शामिल थे। इसके बाद Gemini 4 Carbon एजेंट टीमों ने प्रमाण का पूरा कोड तैयार किया; लेखकों में से किसी ने भी प्रमाण कोड नहीं लिखा। आम तौर पर, एक मशीन पर 40 से 80 एजेंट 24 से 72 घंटे तक काम करते थे। एक ऑर्केस्ट्रेटर और टीम लीड प्रमाण तैयार करने वाले एजेंटों के काम में तालमेल बिठाते थे, जबकि आर्किटेक्ट और इंटीग्रेटर की भूमिकाएँ साझा प्रमाण-आधार को बनाए रखती थीं।

एक गेटकीपर ने किसी प्रमाण को तभी स्वीकार किया, जब Lean के कर्नेल ने उसकी जाँच कर ली और एक तुलनित्र ने पुष्टि कर दी कि वह अलग रखे गए, मनुष्यों से स्वीकृत विनिर्देश से मेल खाता है। इस जाँच में हर पारगामी परिभाषा शामिल थी और केवल Lean के मानक स्वयंसिद्धों का इस्तेमाल किया गया। जब प्रमाणों से विनिर्देशों की समस्याएँ सामने आईं, तो एजेंट छोटे संशोधन सुझा सकते थे; लेकिन विश्वसनीय मान्यताओं में बदलाव के लिए मनुष्यों की मंज़ूरी या उपयोगकर्ता की ओर से तय की गई नीति आवश्यक थी, और ऐसे बदलावों को उनके औचित्य सहित दर्ज किया जाता था। यह नियंत्रण एजेंटों द्वारा तैयार किए गए प्रमाणों से जुड़े एक दर्ज जोखिम का समाधान करता है: किसी विनिर्देश की परिभाषाओं में से किसी एक के ज़रिए उसे अप्रत्यक्ष रूप से कमज़ोर किया जा सकता है।

सुरक्षा का दायरा और पुराने बगों की जाँच

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

यह जाँचने के लिए कि क्या वे विनिर्देश वास्तविक त्रुटियों को पकड़ सकते हैं, टीम ने पहले सुधारे जा चुके libsignal के दो बग—जिन्हें weak state और small subgroup के नाम से जाना जाता है—के सुधारों को उलटकर लागू किया और बदले हुए बाइनरी को फिर से संकलित किया। दोनों मामलों में, टीम ने Lean प्रमाण तैयार किए कि प्रतीकात्मक सुरक्षा प्रमेय विफल हो गया। सार्वजनिक सत्यापन रिपॉज़िटरी में संगणकीय, प्रतीकात्मक, साझा बाइनरी और AArch64 अर्थ-संरचना से जुड़ी सामग्री अलग-अलग रखी गई है। इसमें यह भी बताया गया है कि प्रमाणों को दोबारा कैसे बनाया जाए और उनकी स्वतंत्र रूप से जाँच कैसे की जाए।

Signal के मुख्य प्रौद्योगिकी अधिकारी Ehren Kret ने कहा कि इस काम से “हमारे कोड की निजता संबंधी गारंटियों पर हमारा भरोसा और भी बढ़ता है।”

सीमाएँ और अगले कदम

ये गारंटियाँ Signal के पूरे ऐप्लिकेशन को प्रमाणित करने से बहुत दूर हैं। ये शोधकर्ताओं के libsignal-cli बिल्ड से संबंधित हैं, जो एक नई प्रक्रिया के रूप में चलता है। कुंजी निर्माण का सत्यापन नहीं किया गया, समूह संदेश-विनिमय को भविष्य के काम के लिए छोड़ दिया गया और साइड चैनल तथा कई डिवाइसों की स्थिति इस परिदृश्य के दायरे से बाहर हैं। निचले स्तर के क्रिप्टोग्राफ़िक प्रिमिटिव और चुने हुए आउटपुट तथा लाइब्रेरी रूटीन को विश्वसनीय अनुबंधों के रूप में दर्शाया गया है। इसलिए नतीजा इन अनुबंधों, स्वीकृत विनिर्देशों, Lean के कर्नेल, AArch64 की अर्थ-संरचना और प्रिमिटिव से जुड़ी मान्यताओं पर भी निर्भर करता है।

शोधपत्र के अनुसार, दोनों में से कोई भी तर्क उस पोस्ट-क्वांटम पुनर्प्राप्ति को प्रमाणित नहीं करता जिसे जोड़ने के लिए SPQR डिज़ाइन किया गया है: संगणकीय प्रमेय में शास्त्रीय हमलावर शामिल हैं, जबकि प्रतीकात्मक रैचेट प्रमेय हमलावर को SPQR कुंजियाँ चुनने देते हैं। संगणकीय मॉडल हमलावर की कई कार्रवाइयों पर भी पाबंदी लगाता है और संदेशों तथा सत्रों की संख्या पर्याप्त रूप से बढ़ जाने पर निरर्थक हो जाता है। ये सीमाएँ बताती हैं कि किसी बाहरी समीक्षक को मशीन से जाँचे गए प्रमाणों को किसी खास परिनियोजन की सुरक्षा-गारंटी मानने से पहले किन बातों पर भरोसा करना होगा।

शोधकर्ताओं ने अगले कदमों के रूप में प्रमेयों को अधिक मज़बूत करने, अधिक जुड़े हुए रूटीन का सत्यापन करके और क्रिप्टोग्राफ़िक अनुबंधों को सत्यापित कार्यान्वयनों से जोड़कर विश्वसनीय आधार को घटाने, तथा समूह संदेश-विनिमय, sealed sender और सर्वर-साइड प्रोटोकॉल तक दायरा बढ़ाने की बात कही है। libsignal के नए संस्करणों को जारी करने से पहले सत्यापित करना उनका उद्देश्य है, लेकिन यह शोध का लक्ष्य है, घोषित परिनियोजन नहीं।

इस नतीजे का तात्कालिक महत्व यह है कि यह काम के बँटवारे को दर्शाता है: एजेंटों ने प्रमाणों का निर्माण किया, जबकि विश्वसनीयता अब भी मनुष्यों द्वारा समीक्षा किए गए विनिर्देशों और स्पष्ट मान्यताओं पर टिकी है। प्रमाणों और जाँच प्रक्रियाओं को जारी करने से बाहरी समीक्षकों को इस बुनियाद की जाँच करने का अवसर मिलता है, जबकि शोधकर्ता इस कार्यप्रवाह को libsignal के सतत विकास में शामिल करने की दिशा में काम कर रहे हैं।