KEM-IND-CCA-Preserving Compilation of Jasmin's ML-KEM
تقدم هذه الورقة برهاناً ميكانيكياً كاملاً في مُثبّت Rocq يثبت أن مُجمّع Jasmin يحافظ على كل من الصحة الوظيفية وأمن KEM-IND-CCA لتنفيذ ML-KEM عالي التحسين المستخدم في Signal، وهو ما تحقق من خلال إطار أمني جديد قائم على الألعاب، ودلالات شجرة التفاعل التي تدعم الحسابات الاحتمالية، ومنطق هوار علاقي.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
في عالم الأمن الرقمي عالي المخاطر، يعمل التشفير كقفل غير مرئي يحمي كل شيء، من الرسائل الخاصة إلى المعاملات المالية. ولعقود من الزمن، اعتمد الخبراء على البراهين الرياضية لضمان أن تكون هذه الأقفال غير قابلة للكسر، ولكن ظلت هناك فجوة حرجة بين الرياضيات الأنيقة على الورق والواقع الفوضوي لشيفرة الحاسوب التي تشغلها. فحتى عندما يكون المخطط التشفيري مثبتاً أمنياً من الناحية النظرية، فإن عملية ترجمة تلك النظرية إلى التعليمات المحددة التي يفهمها معالج الحاسوب يمكن أن تؤدي إلى أخطاء دقيقة. وهذه الأخطاء، التي غالباً ما تسببها المترجمات (compilers) التي تقوم بعملية الترجمة، يمكن أن تخلق ثغرات يستغلها المهاجمون. وبينما يستعد العالم للانتقال إلى معايير تشفير جديدة مقاومة للحوسبة الكمومية لحماية الأنظمة من التهديدات المستقبلية، فإن ضمان بقاء هذه الأنظمة الجديدة آمنة وصولاً إلى لغة الآلة لم يعد مجرد شاغل نظري؛ بل أصبح ضرورة لسلامة شبكات الاتصالات العالمية.
لقد نجح فريق من الباحثين الآن في سد هذه الفجوة لأحد أهم معايير التشفير الجديدة، والمعروف باسم ML-KEM، والذي يُستخدم بالفعل في تطبيقات المراسلة الآمنة الشهيرة مثل Signal. ويوضح عملهم أن أداة البرمجيات المحددة المستخدمة لترجمة كود الأمن عالي المستوى إلى تعليمات الآلة لا تكسر ضمانات الأمان عن طريق الخطأ. وجوهر الأمر هو أنهم أثبتوا أن الخصائص الأمنية المحددة للكود الأصلي القابل للقراءة البشرية يتم الحفاظ عليها تماماً في كود التجميع (assembly code) المحسن النهائي الذي ينفذه الحاسوب فعلياً. ويعد هذا الإنجاز مهماً لأنه يلغي الحاجة إلى الوثوق بالمترجم باعتباره "صندوقاً أسود" قد يحتوي على أخطاء خفية؛ وبدلاً من ذلك، تم التحقق رياضياً من أن المترجم نفسه يمثل جسراً آمناً بين البراهين الأمنية المجردة والعتاد المادي.
كان التحدي الذي واجهه الباحثون فريداً من نوعه لطبيعة التشفير الحديث. فالخوارزمية المحددة التي درسوها، ML-KEM، تعتمد على تقنية تسمى "أخذ العينات بالرفض" (rejection sampling)، حيث يقوم الحاسوب بتكرار محاولات اختيار أرقام عشوائية حتى يجد رقماً يتوافق مع نمط معين. وتؤدي هذه العملية إلى أن البرنامج لا يعمل دائماً لفترة زمنية ثابتة؛ فقد ينتهي بسرعة، أو قد يستغرق محاولات أكثر مما هو متوقع. كانت الطرق السابقة للتحقق من المترجمات مصممة للبرامج التي تعمل في تسلسل خطوات ثابت ومتوقع، وقد واجهت صعوبة في التعامل مع هذا النوع من السلوك الاحتمالي، حيث يعتمد المسار الذي يتخذه الكود على الصدفة. وإذا لم يتمكن أداة التحقق من المترجم من مراعاة هذه الحلقات العشوائية، فلن يتمكن من ضمان أن كود الآلة النهائي يسلك نفس الطريقة التي صُمم بها الأصل، مما يترك ثغرة محتملة في سلسلة الأمن.
ولحل هذه المشكلة، بنى الباحثون إطار عمل جديداً لفهم كيفية سلوك هذه البرامج. فقد عاملوا تنفيذ الكود ليس كمجرد قائمة بسيطة من التعليمات، بل كشجرة من التفاعلات الممكنة، حيث يمثل كل اختيار عشوائي وكل تفاعل مع العالم الخارجي فرعاً في الشجرة. سمح هذا النهج بنمذجة "الإنهاء شبه المؤكد" للبرنامج — أي أنه سينتهي في النهاية باحتمالية واحد، حتى لو كان الوقت الدقيق غير قابل للتنبؤ به. وباستخدام هذا النموذج الجديد، تمكنوا من تحديد ما يعنيه أن يكون المترجم صحيحاً في بيئة احتمالية. لقد أثبتوا أنه لكل مسار محتمل يمكن أن يتخذه الكود الأصلي، يتخذ الكود المترجم مساراً مطابقاً، مما يحافظ على نفس توزيع النتائج بدقة.
طبق الفريق هذا الإطار على مترجم Jasmin، وهو أداة مصممة خصيصاً لكتابة كود تشفير عالي الضمان. وقد ركزوا على تنفيذ ML-KEM المستخدم في تطبيق Signal، وهو تطبيق مراسلة يستخدمه الملايين. وباستخدام "مساعد برهان" (proof assistant) قوي، وهو أداة برمجية تتحقق من الحجج الرياضية بدقة مطلقة، تحققوا من أن المترجم يترجم الكود المصدر بشكل صحيح إلى لغة التجميع دون تغيير الخصائص الأمنية. ويغطي برهانهم عملية الترجمة بأكملها، من الوصف الأولي عالي المستوى وصولاً إلى تعليمات الآلة النهائية. والنتيجة هي ضمان بأن أمن التشفير، الذي كان مثبتًا سابقاً للكود المصدر فقط، يسري الآن أيضاً على الكود الفعلي الذي يعمل على جهاز المستخدم.
يعد هذا العمل جزءاً من جهد أكبر لجلب أعلى مستويات الضمان إلى مرحلة الانتقال لما بعد الحوسبة الكمومية، وهي عملية تحول عالمية نحو طرق تشفير يمكنها الصمود أمام هجمات الحواسيب الكمومية المستقبلية. وبينما لم يمدد الباحثون بعد برهانهم ليشمل هجمات القنوات الجانبية (side-channel attacks) — حيث يمكن للمهاجم معرفة الأسرار من خلال مراقبة المدة التي يستغرقها الحساب أو مقدار الطاقة المستخدمة — فقد وضعوا الأساس اللازم لمثل هذا العمل المستقبلي. ومن خلال إثبات أن المترجم يحافظ على "اللعبة الأمنية" الأساسية، فقد أنشأوا قاعدة صلبة يمكن بناء ضمانات أمنية أكثر تعقيداً فوقها. كما أن عملية التحقق تمت آلياً بالكامل، مما يعني أن كل خطوة في البرهان قد تم فحصها بواسطة حاسوب، مما لا يترك مجالاً للخطأ البشري في المنطق نفسه.
تمتد آثار هذا العمل إلى ما هو أبعد من مجرد خوارومة واحدة. إن إطار العمل الذي طوره الباحثون عام بما يكفي ليتم تطبيقه على مخططات أمنية وخصائص أمنية أخرى. لقد أظهروا أنه من الممكن التفكير في "الأمن القائم على الألعاب" (game-based security)، وهو طريقة قياسية لتحديد القوة التشفيرية، من خلال منظور صحة المترجم. وهذا يعني أنه مع تطوير وتنفيذ معايير تشفير جديدة، يمكن إخضاعها لنفس عملية التحقق الصارمة. لقد جعل الباحثون أدواتهم وبراهينهم مفتوحة المصدر، مما يسمح للخبراء الآخرين بفحص عملهم والتحقق منه والبناء عليه. وتعد هذه الشفافية أمراً حاسماً للحفاظ على الثقة في البنية التحتية الرقمية التي تدعم المجتمع الحديث.
في النهاية، تمثل هذه الورقة البحثية خطوة مهمة نحو مستقبل يمكننا فيه أن نكون واثقين من أن الأقفال الرقمية التي تحمي بياناتنا قوية تماماً كما وعد بها علماء الرياضيات. ومن خلال سد الفجوة بين البراهين الأمنية المجردة والواقع الملموس لكود الآلة، أزال الباحثون مصدراً رئيسياً لعدم اليقين من سلسلة التوريد التشفيرية. إن عملهم يضمن أن الرسائل الآمنة التي يرسلها المستخدم، ليست مجرد مثالات نظرية، بل هي خصائص محفوظة رياضياً وصولاً إلى شرائح السيليكون في أجهزتهم. وهذا المستوى من الضمان هو ما يسمح لنا بالوثوق بالتكنولوجيا التي تربطنا، حتى ونحن نواجه تهديدات جديدة ومتطورة في العصر الرقمي.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.