The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware

ملخص تقني: حاجز البت الواحد هو عالمي

بيان المشكلة
يعتبر تحويل نظرية الأعداد (NTT) العمود الفقري الحسابي لمعايير التشفير ما بعد الكم (PQC) التابعة للمعهد الوطني للمعايير والتقنية (NIST)، وهما ML-DSA (FIPS 204) و ML-KEM (FIPS 203). تعتمد التنفيذات العتادية لهذه المعايير على التغطية الحسابية (arithmetic masking) لمقاومة هجمات القنوات الجانبية، وتحديداً تحليل القدرة التفاضلي (DPA). وبينما أثبتت نماذج التكوين (compositional frameworks) الخاصة بالتغطية البولينية فوق $GF(2^n)$ (مثل PINI) كفاءتها، فإن التغطية الحسابية فوق $\mathbb{Z}_q$ لعدد أولي $q$ تفرض تحديات فريدة.

أثبتت الأعمال السابقة في برنامج QANARY (الأوراق 1-6) تحليلات الاعتماد الهيكلي وكمّت هوامش الأمان لمكونات محددة، ولا سيما إثبات أن اختزال باريت (Barrett reduction) يحقق "حاجز البت الواحد" (PF-PINI(2)). ومع ذلك، ظل هناك فجوتان حرجتان:

1. عمق خط الأنابيب التعسفي: كانت نظريات التكوين السابقة محدودة بمرحلتين فقط. لم يكن هناك ضمان رسمي لخطوط أنابيب مكونة من $k$ مرحلة مع وجود تغطية جديدة بين المراحل.
2. اختزال مونتغمري: بينما تم توصيف اختزال باريت، فإن اختزال مونتغمري — وهو ثاني اختزال معياري مستخدم في عتاد NTT (والمهيمن في تنفيذات ML-DSA وبعض تنفيذات ML-KEM) — افتقر إلى توصيف PF-PINI رسمي.
3. الحدود الموحدة من البداية إلى النهاية: لم يكن هناك حد واحد لعدد العناصر (cardinality bound) تم التحقق منه آلياً يجمع نتائج خطوط الأنابيب المكونة من الفراشات (butterflies)، واختزال باريت، واختزال مونتغمري.

المنهجية
تستخدم الورقة التحقق الرسمي باستخدام مساعد الإثبات Lean 4. المنهجية بناءة تماماً، مع صفر من الـ sorry (الافتراضات غير المثبتة) وصفر من البديهيات غير القياسية. تعتمد المنهجية على:

• تعريف PF-PINI: استخدام معامل (Prime-Field Probe Isolating Non-Interference) المعروف بـ PF-PINI، والذي يحدد تسرب سلك واحد تحت غطاء حسابي واحد. يكون الجهاز (gadget) من نوع PF-PINI($M$) إذا كان عدد عناصر المجموعة العكسية (preimage) لأي قيمة مخرجات لا يتجاوز $M$.
• نمذجة خط الأنابيب: تعريف خط أنابيب مكون من $k$ مرحلة حيث تكون كل مرحلة $G_i$ هي جهاز PF-PINI، تفصل بينها أقنعة عشوائية جديدة. يتم حساب مخرج خط الأنابيب بشكل تكراري.
• التحليل التوليفي: إثبات أن التغطية الجديدة بين المراحل "تمحو" معاملات التسرب للمراحل المتوسطة، مما يترك الحد النهائي معتمداً فقط على معامل المرحلة الأخيرة.
• النمذجة المتوافقة مع العتاد: نمذجة اختزال مونتغمري لمراعاة عرض سجلات العتاد وسلوك الالتفاف (wraparound)، وتحديداً تحليل إزاحة التصادم $2^{w-s}$.

المساهمات الرئيسية
تقدم الورقة أربع مساهمات رئيسية، جميعها تمت صياغتها رسمياً في Lean 4:

1. نظرية تكوين $k$-مرحلة (النظرية 3.1):
   تُعمم هذه النظرية نتيجة التكوين ذات المرحلتين السابقة لتشمل أي عمق $k \ge 1$. وتثبت أنه لخط أنابيب من الأجهزة $G_0, \dots, G_{k-1}$ مع تغطية جديدة بين المراحل، فإن عدد عناصر المجموعة العكسية للمخرج محكوم بـ:
   $$| \{ (m, f) : \text{pipeline output} = v \} | \le G_{k-1}.\text{maxMult} \cdot q^{2k-2}$$
   ومن الأهمية بمكان أن هذا الحد محدد بالمرحلة الأخيرة؛ حيث يتم محو معاملات جميع المراحل المتوسطة بواسطة الأقنعة الجديدة.

2. اختزال مونتغمري هو PF-PINI(2) (النظرية 4.3):
   تثبت الورقة رسمياً أن اختزال مونتغمري يحقق خاصية PF-PINI(2)، محاكياً هيكل اختزال باريت. وتوضح أن خريطة مونتغمري المتوافقة مع العتاد لها هيكل "ثنائي الفروع" (يعتمد على ما إذا كان هناك التفاف أم لا)، مما يؤدي إلى عدد عناصر عكسية لا يتجاوز 2. وتثبت النظرية 4.7 أيضاً إحكام (tightness) هذا الحد، مبينة أنه بالنسبة للمعلمات القياسية (ML-KEM و ML-DSA)، فإن التعددية هي 2 بالضبط.

3. حد التعددية من البداية إلى النهاية (النظرية 5.1):
   من خلال الجمع بين نظرية تكوين $k$-مرحلة ونتائج PF-PINI(2) الخاصة باختزال باريت (الورقة 5) ومونتغمري (هذه الورقة) والفراشات (الورقة 4)، تضع الورقة حداً موحداً. لأي خط أنابيب $k$-مرحلة حيث تحقق كل مرحلة $\text{maxMult} \le 2$، يكون عدد عناصر المجموعة العكسية للمخرج محدوداً بـ:
   $$2 \cdot q^{2k-2}$$
   تحت نموذج البحث من الدرجة الأولى (first-order probing model) مع أقنعة منتظمة، يقابل هذا احتمال شرطي لكل ملاحظة قدره $2/q$، وهو مستقل عن عمق خط الأنابيب $k$.

4. الترسيخ الرسمي للنتائج التجريبية (النظرية 5.4):
   تقدم الورقة شرطاً تم التحقق منه عبر Lean ينص على أنه إذا كان أي جهاز في خط الأنابيب لديه $\text{maxMult} \ge 3$ (على سبيل المثال، مرحلة غير مغطاة)، فإن فرضية الحد النهائي للفشل. وهذا يرسخ رسمياً التحليلات التجريبية والهيكلية السابقة لمسرع "Adams Bridge" PQC (الأوراق 1، 2، وأعمال خارجية)، مؤكداً أن تكوينات محددة غير مغطاة في ذلك التصميم تقع خارج الشروط الكافية للحد المستقل عن العمق.

النتائج

• عالمية حاجز البت الواحد: تؤكد الورقة أن "حاجز البت الواحد" (عدد عناصر عكسي يساوي 2) ينطبق على كلا الاختزالين المعياريين (باريت ومونتغمري) المستخدمين في عتاد NIST PQC.
• الاستقلال عن العمق: تثبت البراهين الرسمية أن إضافة مراحل إلى خط الأنابيب لا يؤدي إلى تدهور حد تسرب الملاحظة الواحدة، بشرما تم استخدام تغطية جديدة بين المراحل وكان كل مرحلة يحقق PF-PINI($\le 2$).
• حالة التحقق: تتكون القطعة البرمجية بالكامل من 20 إعلان عبر ثلاثة وحدات نظرية، حيث تم بناء 1,753 وظيفة (jobs) مع صفر أخطاء، وصفر من الـ sorry، ولا توجد إجراءات قرار أصلية (native decision procedures).

الأهمية والادعاءات
تضع هذه الورقة نفسها كمتمم لبرنامج التحقق الرسمي لعتاد NTT المغطى (masked NTT). تكمن أهميتها في توفير أساس تركيبي كمي ومتحقق منه آلياً لمصممي العتاد.

• من أجل الاعتماد (Certification): يوفر حد عدد العناصر المستمد ($2 \cdot q^{2k-2}$) الدليل المحدد المطلوب لحجج مقاومة DPA على مستوى البنية، مكملاً أدوات المستوى البوابي (gate-level) مثل SILVER و maskVerif.
• للمصممين: تقدم مسار علاج توجيهي: لتحقيق حد مستقل عن العمق، يجب على المصممين التأكد من أن كل مرحلة هي PF-PINI($\le 2$) وإدراج أقنعة جديدة بين المراحل.
• تواضع الادعاءات: يصرح المؤلفون صراحةً بأن تفسيرات الاحتمالية والاعتلاج الأدنى (min-entropy) (مثل $2/q$) هي تبعات دلالية غير رسمية لحدود عدد العناصر وليست مُصاغة آلياً في Lean. علاوة على ذلك، فيما يتعلق بتحليل Adams Bridge، تدعي الورقة فقط أن تكوينات محددة تفشل في استيفاء الشروط الكافية للنظرية 5.1؛ وهي لا تدعي أن العتاد "مكسور" أو "غير آمن"، مقرة بأن أطر عمل بديلة أو نماذج أقوى قد تؤدي إلى استنتاجات مختلفة. يتم تأطير العمل كأداة للتحليل التركيبي وليس كحكم أمني نهائي على تنفيذات محددة.