Signal प्रोटोकॉल का सत्यापन
Google DeepMind के शोधकर्ताओं ने चार सप्ताह के प्रूफ-ऑफ-कांसेप्ट प्रोजेक्ट में Signal प्रोटोकॉल के कई प्रमुख क्रिप्टोग्राफिक गारंटियों को गणितीय रूप से सिद्ध करने, या औपचारिक रूप से सत्यापित करने के लिए एजेंटिक AI का उपयोग किया। इस कार्य में AlphaProof Code नामक एक नए AI फ्रेमवर्क का उपयोग किया गया।
सत्यापन में PQXDH हैंडशेक और Triple Ratchet प्रोटोकॉल के लिए मशीन-कोड स्तर के गुणों को कवर किया गया। टीम ने libsignal-protocol संस्करण 0.105.4 और SPQR संस्करण 1.6.0 से बने एक कंपाइल्ड बाइनरी में लगभग 140,000 मशीन निर्देशों को सत्यापित किया। AI ने Lean में लगभग 6.5 मिलियन लाइनों का प्रूफ कोड जेनरेट किया, जबकि एजेंटों द्वारा प्रमाण (proofs) तैयार करने से पहले मानव विशेषज्ञों ने विनिर्देशों (specifications) की समीक्षा की।
DeepMind के विश्लेषण में Signal प्रोटोकॉल के जिन हिस्सों का अध्ययन किया गया, उनमें कोई नई भेद्यता नहीं मिली। जब शोधकर्ताओं ने Signal के उन पुराने संस्करणों पर AlphaProof Code का उपयोग किया जिनमें ज्ञात और लंबे समय से ठीक की जा चुकी भेद्यताएं शामिल थीं, तो इसने उनकी सही पहचान की और दिखाया कि प्रोटोकॉल को औपचारिक रूप से सत्यापित नहीं किया जा सकता था।
