Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking

إليك ملخص تقني مفصل للورقة البحثية بعنوان: "Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking" (نظرية التكوين الموثقة آلياً لتقنيات الحجب في الحقول الأولية لـ NTT ما بعد الكم).

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

تتناول الورقة فجوة حرجة في التحقق الرسمي من أمن الأجهزة (Hardware) الخاصة بالتشفير ما بعد الكم (PQC)، وتحديداً لتطبيقات تحويل الأعداد النظرية (NTT) المستخدمة في معايير NIST (مثل ML-KEM و ML-DSA).

• السياق: تعتمد التنفيذات العتادية لـ NTT على الحجب الحسابي (Arithmetic Masking) فوق الحقول الأولية ($\mathbb{Z}_q$) لمقاومة هجمات القنوات الجانبية مثل تحليل القدرة التفاضلي (DPA).
• الفجوة: بينما يمتلك الحجب البولياني (Boolean Masking) (فوق $GF(2^n)$) نظرية تكوين ناضجة (NI, SNI, PINI) مع براهين موثقة آلياً، تفتقر الحجب الحسابية فوق الحقول الأولية إلى نظريات تكوين مماثلة.
• المشلية المحددة: في الحجب الحسابي، تتفاعل العمليات مثل الاختزال المعياري (Modular Reduction) (مثل اختزال باريت - Barrett reduction) مع الأقنعة (Masks) بطرق غير تقليدية. وخلافاً لعملية XOR البوليانية، حيث يحافظ الحجب على التوزيع الموحد تماماً، يمكن للحجب الحسابي أن ينتج توزيعات غير موحدة (Multiplicity > 1).
• الثغرة الأمنية: حددت الدراسات التجريبية والتحليلات الهيكلية السابقة ثغرات في مسرع "Adams Bridge" الخاص بـ Microsoft، حيث كانت الأسلاك الوسيطة بين مراحل خطوط الأنابيب (Pipeline stages) غير موحدة، مما سمح بهجمات DPA. ومع ذلك، كان ينقصنا تفسير نظري رسمي لسبب حدوث ذلك وكيفية إصلاحه عبر نظريات التكوين.

2. المنهجية

يستخدم المؤلفون التحقق الرسمي (Formal Verification) باستخدام مساعد الإثبات Lean 4 لاستخلاص وإثبات نظريات التكوين للحجب الحسابي.

• النموذج الرسمي: قاموا بتعريف مقياس أمني كمي يسمى PF-PINI(k) (الاستقلال عن المسبار في الحقل الأولي - Prime-Field Probe Isolating Non-Interference).
  • بخلاف المفاهيم الأمنية الثنائية (آمن/غير آمن)، يقيس PF-PINI التعددية (Multiplicity) لقيم المخرجات بالنسبة لفضاء القناع.
  • $k=1$ يعني توزيعاً موحداً تماماً.
  • $k=2$ يعني تعددية قصوى قدرها 2، مما يسرب ما يصل إلى 1 بت من المعلومات لكل سلك.
• "حجة التجديد" (The Renewal Argument): الرؤية النظرية الجوهرية هي أن تطبيق قناع عشوائي جديد بين مرحلتين من خط الأنابيب "يمحو" تماماً معامل الأمان ($k_1$) للمرحلة الأولى من السلك الوسيط، بغض النظر عن مدى عدم توحد مخرجات المرحلة الأولى.
• الجسر العتادي: قام المؤلفون بربط الفجوة رسمياً بين النماذج الجبرية المجردة ($\mathbb{Z}_q$) وحسابات الأعداد الطبيعية (Nat) المخلصة للعتاد المستخدمة في تصميمات RTL، وتحديداً لاختزال باريت.
• نطاق التحقق: يتكون العمل بأكمله من 18 نظرية موثقة آلياً مع صفر من ثغرات sorry (أي لا توجد افتراضات غير مثبتة)، مما يضمن ضمانات عالية الموثوقية.

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

تقدم الورقة ست مساهمات رئيسية:

1. نظرية التجديد (Theorem 4.1): تثبت أنه إذا تم تطبيق قناع عشوائي جديد بين مرحلتين ($G_1 \to G_2$)، فإن السلك الوسيط يصبح موحداً تماماً. مجموعة أزواج الأقنعة التي تنتج أي قيمة وسيطة محددة لها عدد كاردينالية يساوي $q$ بالضبط، وبشكل مستقل عن معامل أمان $G_1$.
2. نظرية التكوين الإيجابية (Theorem 4.4): توضح أن خط أنابيب مكون من مرحلتين مع حجب جديد يحقق PF-PINI($k_2$). يعتمد أمن المخرجات المركبة فقط على معامل المرحلة الثانية ($k_2$)؛ حيث يتم محو ضعف المرحلة الأولى ($k_1$) تماماً.
3. نظريات التكوين السلبية (Theorems 5.1–5.3): تثبت أنه بدون حجب جديد، يحتفظ السلك الوسيط بتعددية المرحلة الأولى ($k_1$). إذا كان $k_1 > 1$، يكون السلك غير موحد، مما يخلق شرطاً ضرورياً لهجمات DPA.
4. الجسر الجبري-العتادي (Theorem 6.1): يثبت رسمياً أن خريطة اختزال باريت الجبرية مكافئة لخريطة حساب الأعداد الطبيعية (Nat) المخلصة للعتاد تحت شروط النطاق القياسية ($q \le 2^s$). وهذا يؤكد أن الحدود النظرية تنطبق مباشرة على تنفيذات السيليكون.
5. تشخيص Adams Bridge: تقوم الورقة بتطبيق النظريات رسمياً لتشخيص مسرع Adams Bridge الخاص بـ Microsoft. يؤكد الإثبات أن غياب الحجب الجديد بين المراحل يترك أسلاك مخرجات باريت غير موحدة (PF-PINI(2))، مما يفسر نجاح هجمات DPA التجريبية السابقة.
6. حاجز الـ 1-بت العالمي: تقدم أدلة حسابية على أن حد PF-PINI(2) هو عالمي لعمليات الاختزال المعياري (سواء باريت أو مونتغمري)، مما يشير إلى وجود "حاجز 1-بت" أساسي لهذه العمليات.

4. النتائج الرئيسية

• الإثبات الرسمي للتكوين: تثبت الورقة أن الحجب الجديد بين المراحل هو الشرط الضروري والكافي لتكوين أجهزة (gadgets) حسابية بشكل آمن.
• الأمن الكمي:
  • مع الحجب الجديد: السلك الوسيط موحد ($k=1$). المخرج النهائي محكوم بمعامل المرحلة الثانية ($k_2$).
  • بدون الحجب الجديد: السلك الوسيط غير موحد (يصل إلى $k_1$). هذا عدم التوحيد هو السبب الجذري لتسرب القنوات الجانبية الملحوظ في الهجمات التجريبية.
• إصلاح Adams Bridge: يؤكد التشخيص أن إضافة سجل قناع عشوائي واحد وعملية طرح بين مرحلتي Butterfly وBarrett في خط أنابيب Adams Bridge من شأنه أن يلغي ثغرة DPA في الأسلاك الوسيطة دون تغيير معامل أمان المخرج النهائي.
• توافر الأدوات: الكود المصدري الكامل لـ Lean 4، بما في ذلك 1 الـ 18 نظرية وسكريبت إعادة الإنتاج، متاح للجمهور، مما يسمح بالتحقق المستقل من البراهن.

5. الأهمية

• أول تكوين حسابي موثق آلياً: يعد هذا العمل أول عمل يقدم نظريات تكوين موثقة آلياً للحجب الحسابي فوق الحقول الأولية، مما يسد فجوة نظرية كبرى في أمن عتاد PQC.
• الربط بين النظرية والتطبيق: من خلال ربط البراهن الجبرية المجردة بالحساب المخلص للعتاد رسمياً، توفر الورقة أساساً صارماً للتحقق من تصميمات السيليكون الواقعية، متجاوزة الاختبار التجريبي.
• إرشادات التصميم: تضع قاعدة تصميم واضحة وقابلة للإثبات لأجهزة PQC: دائماً قم بإدراج حجب جديد بين مراحل خط الأنابيب. هذا التغيير المعماري البسيط يضمن أن أمن خط الأنابيب المركب يتحدد فقط من خلال الحلقة الأضعف في المرحلة النهائية، وليس في المراحل المتوسطة.
• تلاقي الأدلة: يتوافق الإثبات الرسمي تماماً مع ثلاثة تحليلات سابقة مستقلة (تحليل القدرة التجريبي، مراجعة الكود، وتحليل التبعية الهيكلية)، مما يؤكد أن الخلل المعماري المحدد في مسرع Adams Bridge هو بالفعل السبب الجذري لضعفه.

باختصار، توفر هذه الورقة العمود الفقري الرياضي والرسمي المطلوب لتصميم مسرعات عتادية آمنة، قابلة للتكوين، ومقاومة للقنوات الجانبية لعصر التشفير الجديد لما بعد الكم.