💻 computer science

From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification

تقدم هذه الورقة أول برهان عالمي تم التحقق منه آلياً في لغة Lean 4، والذي يثبت أن استقلال القيمة يستلزم توزيعات هامشية متطابقة لعمليات القناع الحسابي عبر جميع المقاسات $q > 0$ ، مما يستبدل التحقق القائم على SMT للمجالات المحدودة بأساس نظري حلقي للأجهزة المخصصة للتشفير لما بعد الكوانتوم.

المؤلفون الأصليون: Ray Iskander, Khaled Kirah

نُشر 2026-04-22

📖 4 دقيقة قراءة☕ قراءة في استراحة قهوة

CC BY 4.0

المؤلفون الأصليون: Ray Iskander, Khaled Kirah

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

تخيل أنك تقوم ببناء خزنة عالية الأمان لحماية أثمن أسرار العالم. في المستقبل، ستتمكن الحواسيب "الكمية" القوية من كسر أقفال اليوم، لذا فأنت بحاجة لبناء نوع جديد من الخزنات باستخدام التشفير ما بعد الكمي (PQC).

ولكن هناك عقبة: حتى لو كان القفل مثاليًا من الناحية الرياضية، فقد يقوم لص باختراق القفل ليس بكسر القفل نفسه، بل عبر الاستماع إلى صوت نقرات التروس أو الشعيد بحرارة المعدن أثناء تدوير المفتاح. هذا ما يسمى بـ "هجوم القناة الجانبية" (Side-channel attack).

لإيقاف ذلك، يستخدم المهندسون حيلة تسمى "التقنيع" (Masking). فبدلاً من تدوير المفتاح بيد واحدة، يتم تقسيم الحركة بين يدين (حصص/shares) تتحركان بشكل عشوائي. إذا راقب اللص إحدى اليدين فقط، فلن يرى سوى ضجيج عشوائي.

المشكلة: فخ "العينة الصغيرة"

كان مؤلفو هذه الورقة البحثية، "راي" و"خالد"، قد بنوا سابقًا روبوتًا ذكيًا للغاية (يُسمى QANARY) للتحقق مما إذا كانت تصميمات الخزنات الخاصة بهم آمنة ضد هجمات القنوات الجانبية هذه.

ومع ذلك، كان هناك خلل كبير في كيفية اختبارهم:

الطريقة القديمة: لإثبات أن الخزنة آمنة، قام الروبوت بفحص التصميم باستخدام نظام عدّ بسيط جدًا (مثل قفل يحتوي على 5 وضعيات ممكنة فقط). لقد فحص كل تركيبة من تلك الوضعيات الخمس.
الواقع: الخزنات الحقيقية التي نبنيها للمستقبل تستخدم أرقامًا ضخمة جدًا لدرجة أنها تكاد تكون لانهائية (مثل 3,329 أو 8 ملايين وضعية).
الفجوة: إثبات أن القفل يعمل مع 5 وضعيات لا يضمن أنه سيعمل مع 8 ملايين وضعية. الأمر يشبه إثبات أن جسرًا يمكنه تحمل دراجة هوائية عن طريق اختباره بسيارة لعبة؛ أنت تعلم أن السيارة اللعبة تناسبه، لكن لا يمكنك التأكد بنسبة 100% من أن شاحنة حقيقية لن تكسره.

اعتمدت الطريقة القديمة على القوة الغاشمة (Brute force) -أي تجربة كل الاحتمالات- وهو أمر مستحيل عندما تصبح الأرقام بهذا الحجم الكبير.

الحل: "المفتاح الشامل"

في هذه الورقة، توقف المؤلفون عن محاولة عدّ كل الاحتمالية الممكنة. بدلاً من ذلك، انتقلوا إلى الرياضيات البحتة (تحديدًا ما يسمى نظرية الحلقات - Ring Theory) لإثبات أن الخزنة آمنة لكل أحجام الأرقام الممكنة، دفعة واحدة.

إليك التشبيه:

الروبوت القديم (أدوات حل SMT): تخيل أنك تحاول إثبات أن الباب آمن عبر تجربة كل مفتاح في العالم، واحدًا تلو الآخر. إذا كان لديك 5 مفاتيح، سيستغرق الأمر دقيقة. إذا كان لديك 8 ملايين مفتاح، سيستغرق الأمر للأبد.
الروبوت الجديد (إثبات Lean 4): تخيل صانع أقفال ماهر ينظر إلى شكل ثقب المفتاح وشكل المفتاح. يدرك قائلاً: "آه، نظرًا للطريقة التي ينحني بها المعدن، مهما كان حجم المفتاح كبيرًا، فسيناسب القفل دائمًا". هو لا يحتاج لتجربة المفاتيح؛ بل يحتاج فقط لفهم هندسة القفل.

"معجزة الأسطر الخمسة"

الجزء الأكثر إثارة للدهشة في الورقة هو مدى بساطة الحل الذي توصلوا إليه.

الطريقة القديمة تطلبت فحص 33 مليون سيناريو مختلف للشعور بالثقة.
الطريقة الجديدة تطلبت إثباتًا رياضيًا من خمسة أسطر فقط.

لماذا؟ لأن المؤلفين أدركوا أن أمن الخزنة لا يتعلق بالأرقام المحددة، بل يتعلق بـ قواعد اللعبة (الجبر). بمجرد إثبات أن القواعد تعمل لأي رقم، فلن تحتاج إلى فحص الأرقام بشكل فردي.

ماذا يعني هذا بالنسبة لك؟

أمن مستقبلي: الخزنات المبنية للمعايير الجديدة لـ NIST (مثل ML-KEM و ML-DSA) أصبحت الآن مضمونة رياضيًا بأن تكون آمنة، ليس فقط للأرقام التي نستخدمها اليوم، بل لأي أرقام قد نستخدمها غدًا.
ثقة أقل، إثبات أكثر: في السابق، كان علينا الوثوق بأن برامج الكمبيوتر التي تفحص الأقفال ليس بها أخطاء. الآن، الإثبات بسيط وجوهري لدرجة أنه يتم التحقق منه بواسطة جوهر اللغة الرياضية نفسها. إنه يشبه الانتقال من الثقة في كلمة الميكانيكي إلى قراءة المخطط بنفسك.
الكفاءة: وجدوا أن المشكلة "المعقدة" كانت معقدة فقط لأنهم كانوا ينظرون إليها من الزاوية الخطأ. بمجرد النظر إليها من خلال عدسة الجبر، كان الحل بسيطًا مثل قول: "أ زائد ب ناقص ب يساوي أ دائمًا".

الخلاصة

لقد أخذ المؤلفون فجوة أمنية ضخمة ومخيفة (حيث لم نكن متأكدين مما إذا كانت الأرقام الكبيرة آمنة) وملأوها بجسر رياضي صغير وأنيق. لقد أثبتوا أنه إذا نجحت حيلة "التقنيع" لرقم صغير، فإن قوانين الرياضيات تضمن نجاحها لأكبر الأرقام التي يمكن تخيلها.

لم يبنوا مجرد قفل أفضل؛ بل أثبتوا أن مخطط القفل غير قابل للكسر، مهما كان حجمه.

إليك ملخص تقني مفصل للورقة البحثية بعنوان "من التعداد المحدود إلى البرهان الشامل: الأسس النظرية الحلقية للتحقق من قناع الأجهزة في التشفير ما بعد الكمي (PQC)" من تأليف راي إسكندر وخالد كيرة.

1. بيان المشكلة

تعالج الورقة فجوة حرجة في التحقق الرسمي من أجهزة التشفير ما بعد الكمي (PQC)، وتحديداً فيما يتعلق بـ القناع الحسابي (arithmetic masking) المستخدم للدفاع ضد هجمات القنوات الجانبية (مثل تحليل القدرة) في مسرعات تحويل "نيبير" (NTT).

السياق: تعتمد المعايير الحديثة لـ NIST (مثل FIPS 203 لـ ML-KEM و FIPS 204 لـ ML-DSA) على الحساب النمطي فوق حقول أولية كبيرة ( $q = 3,329$ و $q = 8,380,417$ على التوالي).
قصور الأعمال السابقة: اعتمد إطار العمل السابق للمؤلفين، QANARY، على تحليل التبعية الهيكلية (SADC) للتحقق من أمن الأجهزة. ومع ذلك، فإن ضمان الصلاحية الخاص به (النظرية 3.9.1) اعتمد على أدوات حل SMT (مثل Z3 و CVC5) لإجراء تعداد شامل عبر نطاق محدود ( $q=5$ $q = 5$ ).
- الفجوة: إن البرهان الذي تم التحقق منه عند $q=5$ لا يضمن هيكلياً الصحة للمعاملات الإنتاجية ( $q=3,329$ أو $q=8,380,417$ ). فأدوات SMT تقوم بتعداد الحالات ولكنها لا تستطيع إجراء الاستقراء الهيكلي. علاوة على ذلك، تضمنت القاعدة الموثوقة أدوات معقدة غير متحقق منها (Z3، CVC5، ومشفرات Python).
التحدي: كانت هناك حاجة إلى برهان شامل ومتحقق منه آلياً يظل صالحاً لجميع قيم $q > 0$ ، مما يلغي الحاجة إلى إعادة التحقق لكل مجموعة معاملات جديدة ويقلل من قاعدة الحوسبة الموثوقة.

2. المنهجية

انتقل المؤلفون من حل SAT لمتجهات البت (bit-vector SAT solving) إلى الاستدلال التفاعلي (ITP) باستخدام Lean 4 ومكتبته الرياضية Mathlib.

التحول في التجريد: بدلاً من نمذجة الحساب كمتجهات بت مع عمليات تحقق صريحة من تجاوز السعة وعمليات اختزال نمطي (والتي تحجب البنية الجبرية)، قام المؤلفون بنمذجة المجال كـ حلقة قسمة $\mathbb{Z}/q\mathbb{Z}$ .
المفهوم الجوهري: قاموا بصياغة استقلال القيمة (Value-Independence). تكون دالة السلك $w$ مستقلة عن القيمة بالنسبة لسر $x$ إذا كان $w(x - s_1, s_1) = w(x' - s_1, s_1)$ لجميع الأقنعة $s_1$ .
استراتيجية البرهان:
- استخدموا بديهيات الحلقة التبادلية (commutative ring axioms) لـ $\mathbb{Z}/q\mathbb{Z}$ (تحديداً sub_add_cancel) لإثبات أن استقلال القيمة يستليد توزيعاً هامشياً ثابتاً.
- يعتمد البرهان على حقيقة أن إعادة المعلمة ( $s_0 = x - s_1$ ) هي هوية حلقية، وليست إجراءً حسابياً عرضة لأخطاء تجاوز السعة في النموذج المجرد.
- مجموعة البرهان بأكملها خالية من الـ "sorry" (أي لا توجد نصوص غير متحقق منها) وهي متحقق منها عبر النواة (kernel-verified)، مما يعني أن نواة Lean تتحقق من كل خطوة منطقية.

3. المساهمات الرئيسية

تقدم الورقة مجموعة برهنة شاملة تتكون من تسعة نظريات (T1–T6, T1', T3') التي تحل محل التحقق من النطاق المحدود السابق:

النظرية الرئيسية الشاملة (T1): برهان متحقق منه آلياً يفيد بأنه لأي $q > 0$ $q > 0$ ، وأي دالة سلك، وأي أسرار، فإن استقلال القيمة يستلزم توزيعات هامشية متطابقة.
- الأثر: يثبت هذا أنه إذا كان السلك مستقلاً هيكلياً عن السر، فإنه لا يسرب أي معلومات، بغض النظر عن حجم المعامل.
النظريات الداعمة:
- T2 و T3: براهين لـ رحلات إعادة المعلمة (reparametrization round-trips) للقناع البولياني (XOR) والحسابي (الطرح)، وهي صالحة لجميع قيم $k$ و $q$ .
- T3': برهان لـ التقابل (bijectivity) لخريطة إعادة المعلمة، مما يضمن عدم حدوث تصادمات في فضاء القناع.
- T4: حدود عدم تجاوز السعة (No-overflow bounds) التي تربط النموذج الحلقي المجرد بتطبيقات عتادية متجهة بت ملموسة.
- T5: توصيف انحياز مولد الأرقام العشوائية (RNG bias) (على سبيل المثال، لـ $q=3,329$ في ML-KEM) وحدود عالمية للانحياز في أي تكوين $N, q$ .
- T6: مثال مضاد عالمي لعدم الضيق (non-tightness counterexample) يثبت أن عكس النظرية الرئيسية يفشل لجميع قيم $q \ge 2$ (أي أن التوزيع الثابت لا يضمن استقلال القيمة). وهذا يؤكد الطبيعة المتحفظة لأداة QANARY.
الرؤية المنهجية: يوضح المؤلفون أن نظرية الحلقات (ring theory) هي طبقة التجريد الطبيعية للقناع الحسابي، بينما يعد حل SAT لمتجهات البت بديلاً غير فعال وغير شفاف هيكلياً.

4. النتائج

إيجاز البرهان مقابل التعقيد: نتيجة الصلاحية الأساسية (النظرية 4.1)، والتي كانت تتطلب سابقاً 225 تقييماً بوليانياً (و33.5 مليون فحص في السياق الأوسع للورقة الثانية) باستخدام أدوات SMT، يتم الآن إثباتها في خمسة أسطر فقط من كود Lean 4.
حالة التحقق:
- تم إكمال 1,739 مهمة بناء (build tasks).
- 0 خطأ، 0 "sorry" (نصوص غير متحقق منها).
- تم التحقق باستخدام Lean 4.30.0-rc1 مع تثبيت Mathlib على إصدار محدد.
توسع النطاق: يغطي التحقق الآن جميع المعاملات الموجبة ( $q > 0$ )، بما في ذلك معايير NIST الحالية (ML-KEM, ML-DSA)، وأي معايير مستقبلية لتشفير ما بعد الكم، دون الحاجة لإعادة التحقق.
تقليص القاعدة الموثوقة: تم تقليل قاعدة الحوسبة الموثوقة من أدوات SMT المعقدة غير المتحقق منها (Z3, CVC5) ومشفرات Python إلى نواة Lean 4 (والمترجم الأصلي لحالات محددة).

5. الأهمية

الاعتماد (FIPS 140-3): يلغي البرهان الشامل الحاجة إلى قيام مختبرات برنامج التحقق من الوحدات التشفيرية (CMVP) بإعادة التحقق من الأمن لكل تغيير في المعاملات. برهان واحد يغطي جميع قيم $q$ .
قابلية تصميم المحمول (Design Portability): ضمانات الأمان أصبحت الآن "مستقبلية". إذا قامت NIST بتحديث المعاملات أو اعتماد مخططات جديدة تعتمد على الشبكات (lattice-based)، فإن البرهان الرسمي الحالي يظل صالحاً تلقائياً.
موثوقية الأداة: من خلال الانتقة إلى برهان متحقق منه عبر النواة، رفع المؤلفون بشكل كبير من موثوقية تحليل الأمان. لم تعد النتيجة تعتمد على صحة تنفيذ الأدوات الخارجية.
التقدم النظري: تؤسس هذه الورقة أن البنية الجبرية لـ $\mathbb{Z}/q\mathbb{Z}$ كافية لإثبات خصائص الأمان التي كان يُعتقد سابقاً أنها تتطلب تعداداً شاملاً. وهي تشير إلى أن الخصائص المعقدة الأخرى (مثل القناع من الدرجة الأعلى، أو تركيب مراحل NTT) قد تقبل براهين موجزة مماثلة عند صياغتها جبرياً.

في الختام، تغلق هذه الورقة "فجوة النطاق المحدود" في التحقق من أجهزة PQC، منتقلة بالمجال من التعداد الخاص بالحالات إلى البراهين الجبرية الرسمية والشاملة، مما يضمن ضمانات أمنية قوية للجيل القادم من أجهزة التشفير.