Microsoft कृत्रिम बुद्धिमत्ता एजेंटों का उपयोग करके गणितीय रूप से साबित कर रहा है कि इसका एन्क्रिप्शन कोड में कोई खामी नहीं है
Windows और Azure के क्रिप्टोग्राफी लाइब्रेरी के पीछे की टीम कुछ असामान्य कर रही है: केवल कोड का परीक्षण नहीं, बल्कि इसे सही साबित कर रही है, हर संभावित इनपुट के लिए, औपचारिक गणितीय प्रमाण का उपयोग करके जिसे आंशिक रूप से कृत्रिम बुद्धिमत्ता द्वारा लिखा गया है।
मुख्य बिंदु
- Microsoft का SymCrypt लाइब्रेरी, जो Windows और Azure में उपयोग की जाने वाली क्रिप्टोग्राफी इंजन है, 2024 के मध्य तक Rust, Lean और Aeneas को जोड़ने वाली एक टूलचेन का उपयोग करके औपचारिक रूप से सत्यापित किया जा रहा है।
- पहले सत्यापित एल्गोरिदम SHA-3 हैं, जो डेटा के डिजिटल फिंगरप्रिंट बनाने के लिए एक मानक, और ML-KEM, एक पोस्ट-क्वांटम एन्क्रिप्शन स्कीम जो भविष्य के क्वांटम कंप्यूटरों से हमलों के विरुद्ध प्रतिरोधी है।
- कृत्रिम बुद्धिमत्ता एजेंट, सॉफ्टवेयर जो बहु-चरणीय कार्यों को स्वतंत्र रूप से पूरा कर सकते हैं, गणितीय प्रमाण चरण लिख रहे हैं जिन्हें मानव इंजीनियर तब समीक्षा करते हैं और स्वतंत्र रूप से जांचते हैं।
- Microsoft ने सत्यापित कोड, विशिष्टताओं और प्रमाणों को SymCrypt की एक सार्वजनिक शाखा में ओपन सोर्स किया है, जिससे बाहरी समीक्षा के लिए काम उपलब्ध है।
- भविष्य के एल्गोरिदम जिन्हें समान उपचार के लिए योजनाबद्ध किया गया है उनमें AES-GCM, FrodoKEM और ML-DSA शामिल हैं, जो सभी Windows और Linux में आज डेटा की सुरक्षा करते हैं।
क्रिप्टोग्राफिक कोड, सॉफ्टवेयर जो हर ऐप, ब्राउज़र और ऑपरेटिंग सिस्टम में डेटा को एन्क्रिप्ट और सुरक्षित करता है, कुख्यात रूप से अप्रमाणित है। एक छूटी हुई सीमा जांच, जिसका अर्थ है कि यह पुष्टि करने में विफलता कि कोई संख्या सुरक्षित सीमा के भीतर रहती है, सतह पर सुरक्षित दिखने वाली सुरक्षा को खोल सकती है। परीक्षण कई बग पकड़ता है। यह सभी को नहीं पकड़ता है।
Microsoft Research एक अलग दृष्टिकोण पर काम कर रहा है: कोड को गणितीय रूप से सही साबित करना, इससे पहले कि यह जारी हो।
परियोजना SymCrypt के चारों ओर केंद्रित है, Microsoft की ओपन सोर्स क्रिप्टोग्राफिक लाइब्रेरी जो Windows और Azure Linux के अंदर चलती है। इंजीनियर अब Rust में नए क्रिप्टोग्राफिक एल्गोरिदम लिख रहे हैं, एक प्रोग्रामिंग भाषा जो डिजाइन द्वारा मेमोरी-सेफ्टी त्रुटियों के पूरे परिवारों को नियम देती है। फिर वे उन Rust प्रोग्राम को Aeneas नामक एक टूल के माध्यम से चलाते हैं, जो कोड को एक ऐसे रूप में अनुवाद करता है जिसे Lean नामक एक प्रमाण सहायक समझ सकता है।
Lean एक चैटबॉट नहीं है। यह एक औपचारिक प्रमाण फ्रेमवर्क है, सॉफ्टवेयर जो गणितीय तर्कों की जांच करता है जैसे एक कैलकुलेटर अंकगणित की जांच करता है, सिवाय इसके कि यह प्रमाणों की जांच करता है, और यह कभी अंकगणितीय गलती नहीं करता है।
लक्ष्य एक प्रमेय तैयार करना है: हर वैध इनपुट के लिए, यह कार्यान्वयन ठीक वही परिणाम देता है जो प्रकाशित मानक कहता है। आमतौर पर नहीं। हमेशा।
पहली सार्वजनिक रिलीज SHA-3 को कवर करती है, किसी भी डेटा के अद्वितीय डिजिटल फिंगरप्रिंट बनाने के लिए एक मानक एल्गोरिदम, और ML-KEM, एक पोस्ट-क्वांटम की एक्सचेंज स्कीम। पोस्ट-क्वांटम क्रिप्टोग्राफी का मतलब है एल्गोरिदम जो क्वांटम कंप्यूटरों के विरुद्ध भी सुरक्षित रहने के लिए बनाए गए हैं, मशीनें जो आज की कई एन्क्रिप्शन विधियों को तोड़ सकती हैं।
गणितीय प्रमाण में कृत्रिम बुद्धिमत्ता कैसे फिट होती है?
औपचारिक प्रमाण लिखना धीमा है। यह वह है जहाँ कृत्रिम बुद्धिमत्ता एजेंट आते हैं।
एजेंट दोहराए जाने वाले मध्य चरणों को संभालते हैं, प्रमाण अंशों का मसौदा तैयार करते हैं जो मध्यवर्ती परिणामों को जोड़ते हैं। मानव इंजीनियर उन भागों पर ध्यान केंद्रित करते हैं जिन्हें वास्तविक निर्णय की आवश्यकता है: यह जांचना कि औपचारिक विनिर्देश वास्तव में प्रकाशित मानक से मेल खाता है, और कोड को संतुष्ट करना चाहिए उच्च-स्तरीय गुणों की समीक्षा करना। प्रमाण-जांच स्वयं पूरी तरह से स्वचालित और नियतात्मक है, जिसका अर्थ है कि मशीन प्रमाण को स्वीकार करती है या अस्वीकार करती है। एजेंट के लिए धोखा देने की कोई गुंजाइश नहीं है।
Microsoft इसे एक स्वच्छ विभाजन के रूप में वर्णित करता है: एजेंट लिखते हैं, मनुष्य समीक्षा करते हैं, प्रमाण जांचक फैसला करता है।
जो लोग Windows, Azure या किसी ऐसी सेवा का उपयोग करते हैं जो Microsoft की सुरक्षा स्टैक पर निर्भर करती है, उनके लिए व्यावहारिक अर्थ सीधा है। आपकी फाइलों, आपके क्लाउड डेटा और आपके लॉगिन की सुरक्षा करने वाली एन्क्रिप्शन को अकेले परीक्षण प्रदान कर सकता है से अधिक उच्च मानक तक रखा जा रहा है। यदि प्रमाण पास करते हैं, तो कोड ठीक वही करता है जो मानक की आवश्यकता है।
ओपन सोर्स की गई शाखा बाहरी शोधकर्ताओं को Rust कोड और प्रमाणों को साथ-साथ निरीक्षण करने देती है, इसलिए दावे केवल Microsoft के शब्द नहीं हैं।
निगरानी रखें: औपचारिक रूप से सत्यापित निर्माण स्थिर Windows रिलीज में पहुंचने की घोषणाएं, और क्या अन्य क्रिप्टोग्राफी लाइब्रेरी समान कृत्रिम बुद्धिमत्ता-सहायक प्रमाण वर्कफ़्लो को अपनाते हैं। यह सॉफ्टवेयर सही होने के बारे में उद्योग कैसे सोचता है इसमें एक वास्तविक बदलाव को चिह्नित करेगा।
