KEM-IND-CCA-Preserving Compilation of Jasmin's ML-KEM
यह शोध पत्र Rocq प्रूवर में एक पूर्णतः यांत्रिक प्रमाण प्रस्तुत करता है कि जैस्मीन (Jasmin) कंपाइलर सिग्नल (Signal) में उपयोग किए जाने वाले अत्यधिक अनुकूलित ML-KEM कार्यान्वयन के लिए कार्यात्मक शुद्धता (functional correctness) और KEM-IND-CCA सुरक्षा दोनों को सुरक्षित रखता है, जिसे एक नए गेम-आधारित सुरक्षा ढांचे, संभाव्य गणनाओं (probabilistic computations) का समर्थन करने वाले इंटरेक्शन-ट्री सिमेंटिक्स और एक रिलेशनल होअर लॉजिक (relational Hoare logic) के माध्यम से प्राप्त किया गया है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
डिजिटल सुरक्षा की उच्च-दांव वाली दुनिया में, क्रिप्टोग्राफी एक अदृश्य ताले के रूप में कार्य करती है जो निजी संदेशों से लेकर वित्तीय लेनदेन तक सब कुछ सुरक्षित रखती है। दशकों से, विशेषज्ञों ने इन तालों को अटूट सुनिश्चित करने के लिए गणितीय प्रमाणों पर भरोसा किया है, लेकिन सुंदर गणित और उन्हें चलाने वाले कंप्यूटर कोड की जटिल वास्तविकता के बीच एक महत्वपूर्ण अंतर बना हुआ है। भले ही कोई क्रिप्टोग्राफिक योजना सैद्धांतिक रूप से सुरक्षित सिद्ध हो, लेकिन उस सिद्धांत को विशिष्ट निर्देशों में अनुवादित करने की प्रक्रिया जिसे एक कंप्यूटर प्रोसेसर समझता है, सूक्ष्म त्रुटियां उत्पन्न कर सकती है। ये त्रुटियां, जो अक्सर उन कंपाइलर द्वारा पेश की जाती हैं जो अनुवाद करते हैं, ऐसी कमजोरियां पैदा कर सकती हैं जिनका हमलावर फायदा उठाते हैं। जैसे-जैसे दुनिया भविष्य के खतरों से निपटने के लिए नए, क्वांटम-प्रतिरोधी एन्क्रिप्शन मानकों की ओर बढ़ने की तैयारी कर रही है, इन नए सिस्टमों को मशीन कोड तक पूरी तरह से सुरक्षित रखना अब केवल एक सैद्धांतिक चिंता नहीं है; यह वैश्विक संचार नेटवर्क की सुरक्षा के लिए एक आवश्यकता है।
शोधकर्ताओं की एक टीम ने अब एक अत्यंत महत्वपूर्ण नए एन्क्रिप्शन मानक के लिए इस अंतर को पाट दिया है, जिसे ML-KEM के रूप में जाना जाता है, जिसका उपयोग पहले से ही सिग्नल (Signal) जैसे लोकप्रिय सुरक्षित मैसेजिंग अनुप्रयोगों में किया जा रहा है। उनका कार्य यह प्रदर्शित करता है कि उच्च-स्तरीय सुरक्षा कोड को मशीन निर्देशों में अनुवादित करने के लिए उपयोग किया जाने वाला विशिष्ट सॉफ्टवेयर टूल अनजाने में सुरक्षा गारंटी को तोड़ता नहीं है। मूल रूप से, उन्होंने सिद्ध किया है कि मूल, मानव-पठनीय कोड के लिए स्थापित सुरक्षा गुण उस अंतिम, अनुकूलित असेंबली कोड में पूरी तरह से संरक्षित हैं जिसे कंप्यूटर वास्तव में निष्पादित करता है। यह उपलब्धि महत्वपूर्ण है क्योंकि यह कंपाइलर को एक "ब्लैक बॉक्स" के रूप में विश्वास करने की आवश्यकता को समाप्त करती है जिसमें छिपे हुए बग हो सकते हैं; इसके बजाय, कंपाइलर को स्वयं एक सुरक्षित सेतु के रूप में गणितीय रूप से सत्यापित किया गया है जो अमूर्त सुरक्षा प्रमाणों और भौतिक हार्डवेयर के बीच कार्य करता है।
शोधकर्ताओं के सामने जो चुनौती थी वह आधुनिक एन्क्रिप्शन की प्रकृति के कारण अद्वितीय थी। जिस विशिष्ट एल्गोरिदम का उन्होंने अध्ययन किया, ML-KEM, वह 'रिजेक्शन सैंपलिंग' नामक एक तकनीक पर निर्भर करता है, जहाँ कंप्यूटर बार-बार यादृच्छिक संख्याओं (random numbers) को तब तक आजमाता है जब तक कि उसे एक विशिष्ट पैटर्न वाला नंबर न मिल जाए। इस प्रक्रिया का अर्थ है कि प्रोग्राम हमेशा एक निश्चित समय के लिए नहीं चलता है; यह जल्दी भी समाप्त हो सकता है, या इसमें उम्मीद से कई अधिक प्रयास लग सकते हैं। कंपाइलर सत्यापन के पिछले तरीके उन प्रोग्रामों के लिए डिज़ाइन किए गए थे जो एक अनुमानित, निश्चित क्रम के चरणों में चलते हैं। वे इस प्रकार के संभाव्य व्यवहार (probabilistic behavior) को संभालने में संघर्ष करते थे, जहाँ कोड का पथ संयोग पर निर्भर करता है। यदि एक कंपाइलर सत्यापन उपकरण इन यादृच्छिक लूपों को ध्यान में नहीं रख सकता है, तो वह यह गारंटी नहीं दे सकता कि अंतिम मशीन कोड मूल डिजाइन के समान व्यवहार करेगा, जिससे सुरक्षा श्रृंखला में एक संभावित छेद रह जाता है।
इसे हल करने के लिए, शोधकर्ताओं ने इन प्रोग्रामों के व्यवहार को समझने के लिए एक नया ढांचा बनाया। उन्होंने कोड के निष्पादन को केवल निर्देशों की एक सरल सूची के रूप में नहीं, बल्कि संभावित अंतःक्रियाओं के एक वृक्ष (tree) के रूप में माना, जहाँ प्रत्येक यादृच्छिक विकल्प और बाहरी दुनिया के साथ प्रत्येक अंतःक्रिया एक शाखा है। इस दृष्टिकोण ने उन्हें प्रोग्राम के "लगभग निश्चित" (almost sure) समापन को मॉडल करने की अनुमति दी—जिसका अर्थ है कि यह एक की प्रायिकता (probability of one) के साथ अंततः समाप्त हो जाएगा, भले ही सटीक समय अनिश्चित हो। इस नए मॉडल का उपयोग करके, वे यह परिभाषित करने में सक्षम हुए कि एक संभाव्य सेटिंग में कंपाइलर का सही होना क्या होता है। उन्होंने सिद्ध किया कि मूल कोड द्वारा लिए जाने वाले प्रत्येक संभावित पथ के लिए, संकलित कोड एक मिलान पथ लेता है, और परिणामों के सटीक वितरण को बनाए रखता है।
टीम ने इस ढांचे को जैस्मीन (Jasmin) कंपाइलर पर लागू किया, जो उच्च-आश्वासन वाले क्रिप्टोग्राफिक कोड लिखने के लिए विशेष रूप से डिज़ाइन किया गया एक टूल है। उन्होंने सिग्नल में उपयोग किए जाने वाले ML-KEM के कार्यान्वयन पर ध्यान केंद्रित किया, जो लाखों उपयोगकर्ताओं वाला एक मैसेंजर ऐप है। एक शक्तिशाली 'प्रूफ असिस्टेंट' का उपयोग करते हुए, जो पूर्ण कठोरता के साथ गणितीय तर्कों की जांच करने वाला एक सॉफ्टवेयर टूल है, उन्होंने सत्यापित किया कि कंपाइलर स्रोत कोड को असेंबली भाषा में बिना सुरक्षा गुणों को बदले सही ढंग से अनुवादित करता है। उनका प्रमाण संपूर्ण संकलन प्रक्रिया को कवर करता है, प्रारंभिक उच्च-स्तरीय विवरण से लेकर अंतिम मशीन निर्देशों तक। परिणाम यह गारंटी है कि एन्क्रिप्शन की सुरक्षा, जो पहले केवल स्रोत कोड के लिए सिद्ध की गई थी, अब उपयोगकर्ता के डिवाइस पर चल रहे वास्तविक कोड के लिए भी सत्य है।
यह कार्य पोस्ट-क्वांटम संक्रमण में उच्चतम स्तर का आश्वासन लाने के एक बड़े प्रयास का हिस्सा है, जो भविष्य के क्वांटम कंप्यूटरों के हमलों का सामना करने में सक्षम एन्क्रिप्शन विधियों की ओर एक वैश्विक बदलाव है। हालाँकि शोधकर्ताओं ने अभी तक अपने प्रमाण को 'साइड-चैनल हमलों' (side-channel attacks) को कवर करने के लिए विस्तारित नहीं किया है—जहाँ एक हमलावर यह जानकर रहस्य जान सकता है कि गणना में कितना समय लगता है या कितनी बिजली का उपयोग होता है—लेकिन उन्होंने भविष्य के ऐसे कार्यों के लिए आवश्यक आधार तैयार कर दिया है। यह स्थापित करके कि कंपाइलर मूल 'सुरक्षा खेल' (security game) को संरक्षित करता है, उन्होंने एक ठोस आधार बनाया है जिस पर अधिक जटिल सुरक्षा गारंटी बनाई जा सकती है। सत्यापन पूरी तरह से यांत्रिक (mechanized) है, जिसका अर्थ है कि प्रमाण के प्रत्येक चरण की जाँच एक कंप्यूटर द्वारा की गई है, जिससे तर्क में मानवीय त्रुटि की कोई गुंजाइश नहीं रहती।
इस कार्य के निहितार्थ केवल एक एल्गोरिदम तक ही सीमित नहीं हैं। शोधकर्ताओं द्वारा विकसित ढांचा इतना सामान्य है कि इसे अन्य क्रिप्टोग्राफिक योजनाओं और सुरक्षा गुणों पर लागू किया जा सकता है। उन्होंने दिखाया है कि कंपाइलर की शुद्धता के लेंस के माध्यम से 'गेम-आधारित सुरक्षा' (game-based security), जो क्रिप्टोग्राफिक मजबूती को परिभाषित करने का एक मानक तरीका है, के बारे में तर्क करना संभव है। इसका अर्थ है कि जैसे-जैसे नए एन्क्रिप्शन मानक विकसित और कार्यान्वित किए जाते हैं, उन्हें इसी तरह की कठोर सत्यापन प्रक्रिया से गुजरने के लिए प्रस्तुत किया जा सकता है। शोधकर्ताओं ने अपने उपकरणों और प्रमाणों को ओपन सोर्स बना दिया है, जिससे अन्य विशेषज्ञ उनके कार्य का निरीक्षण, सत्यापन और उस पर निर्माण कर सकें। आधुनिक समाज की नींव रखने वाले डिजिटल बुनियादी ढांचे में विश्वास बनाए रखने के लिए यह पारदर्शिता अत्यंत महत्वपूर्ण है।
अंत में, यह शोध पत्र एक ऐसे भविष्य की ओर एक महत्वपूर्ण कदम है जहाँ हम इस बात पर आश्वस्त हो सकते हैं कि हमारे डेटा की रक्षा करने वाले डिजिटल ताले उतने ही मजबूत हैं जितने कि गणितज्ञों ने उन्हें डिजाइन करते समय वादा किया था। अमूर्त सुरक्षा प्रमाणों और मशीन कोड की ठोस वास्तविकता के बीच के अंतर को पाटकर, शोधकर्ताओं ने क्रिप्टोग्राफिक आपूर्ति श्रृंखला से एक प्रमुख अनिश्चितता को हटा दिया है। उनका कार्य यह सुनिश्चित करता है कि जब कोई उपयोगकर्ता एक सुरक्षित संदेश भेजता है, तो सुरक्षा गारंटी जिस पर वे भरोसा करते हैं, वह केवल एक सैद्धांतिक आदर्श नहीं है, बल्कि एक ऐसा गुण है जो उनके डिवाइस के सिलिकॉन चिप्स तक गणितीय रूप से संरक्षित है। यह स्तर का आश्वासन ही हमें उस तकनीक पर भरोसा करने की अनुमति देता है जो हमें जोड़ती है, भले ही हम डिजिटल युग में नए और विकसित होते खतरों का सामना कर रहे हों।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।