Google DeepMind के AlphaProof Code ने Signal के libsignal को परखा

टेस्टिंग से आगे, गणितीय प्रमाण

आम तौर पर सॉफ्टवेयर की सुरक्षा टेस्टिंग और ऑडिट से परखी जाती है, जिससे यही कहा जा सकता है कि कोई खामी नहीं मिली। औपचारिक सत्यापन में कोड के बारे में प्रमेय की तरह साबित किया जाता है कि वह कुछ गुणों का उल्लंघन नहीं कर सकता। यह तरीका बेहद महँगा माना जाता है; seL4 कर्नेल के सत्यापन में एक व्यक्ति के करीब बीस साल के बराबर मेहनत लगी थी।

शोधकर्ताओं ने पहले तय किया कि क्या साबित करना है। इसके बाद Gemini 4 Carbon मॉडल पर चलने वाले एजेंटों ने Lean भाषा में करीब 65 लाख पंक्तियों के प्रमाण लिखे, जिनका हर चरण Lean का वेरिफायर अपने आप जाँचता है। किसी शोधकर्ता ने खुद प्रमाण की एक भी पंक्ति नहीं लिखी।

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

सीमाएँ

सत्यापन आंशिक है। यह सिर्फ दो लोगों की बातचीत को कवर करता है, Linux पर चलने वाले टेस्ट संस्करण पर है, मोबाइल ऐप्स पर नहीं, और बुनियादी क्रिप्टोग्राफिक घटकों को बिना जाँचे सही मानकर चलता है। Signal के CTO Ehren Kret ने इसे "एक बड़ी प्रगति" बताया। लेखकों का निष्कर्ष है कि अब प्रमाण सस्ते होने लगे हैं, इसलिए असली सवाल यह है कि क्या साबित किया जाए।