💻 computer science

Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware

تقدم هذه الورقة أول البراهين التي تم التحقق منها آلياً باستخدام لغة Lean 4، والتي تثبت أن قناع الحساب المتجدد لكل مرحلة يضمن الأمان على مستوى خط الأنابيب لمسرعات تحويل NTT في التشفير ما بعد الكم، مع تحديد إخفاقات معمارية محددة مثل مسرع Adams Bridge التي تنتهك هذه الشروط الأمنية.

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

نُشر 2026-04-23

📖 5 دقيقة قراءة🧠 قراءة متعمّقة

CC BY 4.0

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

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

الصورة الكبيرة: بناء خزنة رقمية آمنة

تخد تخيل أنك تبني خزنة عالية الأمان لحماية سر (مثل كلمة مرور أو مفتاح خاص). في عالم "التشفير ما بعد الكم" (نوع جديد من الرياضيات يُستخدم لمنع أجهزة الكمبيوتر الكمية المستقبلية من سرقة الأسرار)، يتم بناء هذه الخزنة باستخدام آلة معقدة تسمى خط أنابيب NTT.

فكر في خط الأنابيب هذا كأنه خط تجميع في مصنع. تدخل المواد الخام (بياناتك السرية) من طرف واحد، وتمر عبر سلسلة من محطات العمل (المراحل)، وتخرج من الطرف الآخر كمنتج نهيد.

ما هي المشكلة؟ اللصوص (الهكرز) يحاولون التلصص على المواد أثناء معالجتها. ولمنعهم، يستخدم المصنع تقنية تسمى "التمويه" (Masking).

التشبيه: استراتيجية "القصاصات الملونة" (الكونفيتي)

تخيل أنك تحمل حزمة من الأوراق المهمة (سرّك) عبر غرفة مزدحمة.

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

المشكلة: "فخ الحدس"

لدى المهندسين الذين يبنون هذه المصانع حدس قوي: "إذا كانت كل محطة عمل بمفردها آمنة، فلا بد أن يكون خط التجميع بأكمله آمناً".

لفترة طويلة، لم يستطع أحد إثبات ذلك رياضياً لهذه الآلات تحديداً.

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

الاكتشافات الثلاثة الكبرى

استخدم المؤلفون مساعداً حاسوبياً فائق الذكاء (يسمى Lean 4) لكتابة "برهان" لا يمكن للإنسان أن يجادل فيه. وقد وجدوا ثلاثة أشياء:

1. إصلاح "الحلقة المفقودة"

في الأعمال السابقة، أثبتوا أنه إذا كانت القصاصات الملونة عشوائية، فإن السر يكون آمناً. لكن كان لديهم فجوة صغيرة في البرهان: لم يشرحوا تماماً ما يحدث عند إضافة قصاصات ملونة جديدة في كل خطوة.

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

2. خدعة "واحد لواحد" السحرية

نظروا إلى محطة عمل واحدة (مرحلة "الفراشة" - Butterfly stage). وأثبتوا خاصية سحرية:

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

3. قاعدة "التمويه الطازج" لخط الإنتاج بأكمله

هذا هو الجزء الأهم. لقد أثبتوا أنه إذا اتبعت قاعدة بسيية واحدة، فإن خط التجميع بأكره سيكون آمناً:

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

الشرير: آلة "جسر آدمز" (Adams Bridge)

يستخدم البحث هذه البرهنة الجديدة لتحليل آلة حقيقية تسمى جسر آدمز (تُستخدم في مشروع يسمى Caliptra).

ما الذي فعلته بشكل خاطئ: كانت آلة جسر آدمز "كسولة". فقد رمت قصاصات ملونة طازجة عند محطة العمل الأولى، ولكنها توقفت بعد ذلك. بالنسبة لبقية خط التجميع، أعادت استخدام نفس القصاصات القديمة أو لم تستخدم أي قصاصات على الإطلاق.
النتيجة: لأنها خرقت "قاعدة التمويه الطازج"، تلاشى ضمان الأمان. بدأت "القصاصات الملونة" تتراكم بطريقة يمكن التنبؤ بها، مما سمح للصوص بإعادة بناء السر.
التشخيص: يشرح هذا البحث لماذا فشلت. لم يكن مجرد خطأ برمجياً؛ بل كان خللاً هيكلياً جوهرياً. حاولت الآلة تخطي خطوة "القصاصات الملونة الطازجة"، وأثبتت الرياضيات أنه لا يمكنك تخطيها.

لماذا يجب أن تهتم؟

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

الملخص في جملة واحدة

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

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

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

تعتمد معايير التشفير ما بعد الكم (PQC)، وتحديداً ML-KEM (FIPS 203) و ML-DSA (FIPS 204)، بشكل كبير على تحويل الأعداد النظرية (NTT) المنفذ فوق الحلقات المحدودة $\mathbb{Z}_q$ . وغالباً ما تستخدم المسرعات العتادية لهذه الخوارزميات مراحل فراشة كولي-توكي (Cooley-Tukey butterfly) ذات خطوط الأنابيب (pipelined).

بينما تم التحقق رسمياً من أمان أدوات التمويه الفردية (مثل بوابات XOR أو AND)، توجد فجوة حرجة في تركيب (composition) هذه الأدوات في خطوط الأنابيب الحسابية:

الفجوة: الأطر الحالية (مثل ISW، t-SNI، PINI، DOM) تمت صياغتها رسمياً بشكل أساسي لـ التمويه البولياني (Boolean masking) فوق $GF(2)$ . ولا يوجد دليل رسمي لتركيب التمويه الحسابي (arithmetic masking) فوق $\mathbb{Z}_q$ خصيصاً لهيكل فراشة NTT.
الفخ: يفترض المصممون حدسياً أنه إذا كان كل مرحلة من مراحل خط الأنابيب آمناً، فإن خط الأنابيب بأكمله يكون آمناً. ومع ذلك، فإن خاصية الأمان القياسية التي يتحقق منها المصممون — وهي استقلال القيمة عند كل نقطة (pointwise value-independence) (حيث لا تتغير قيمة السلك إذا تغير السر مع بقاء الأقنعة ثابتة) — هي خاصية خاطئة بالنسبة لفراشات NTT. والاعتماد على هذه الخاصية الخاطئة يؤدي إلى استنتاجات أمنية غير صحيحة.
الأثر في العالم الحقيقي: وُجد أن مسرع Adams Bridge (المستخدم في CHIPS Alliance Caliptra) غير آمن تجريبياً في عمل سابق. وكان السبب الجذري يُعزى إلى نقص التمويه "الطازج" (fresh masking) بين المراحل، ولكن كان ينقصنا تفسير رياضي رسمي لذلك.

2. المنهجية

يستخدم المؤلفون الإثبات التفاعلي (Interactive Theorem Proving - ITP) لتقديم ضمانات صارمة ومدققة آلياً.

سلسلة الأدوات: تمت صياغة البراهين باستخدام Lean 4 مستفيدين من مكتبة Mathlib.
النطاق: يغطي العمل نموذج الاستقصاء (probing model) من الدرجة الأولى ISW، حيث يمكن للمهاجم مراقبة سلك واحد بالضبط في كل دورة ساعة.
النهج:
1. النمذجة الجبرية: يتم نمذجة فراشة NTT كدالة تآلفية (affine function) للقناع الطازج.
2. توليد المثال المضاد: إثبات أن خاصية "استقلال القيمة عند كل نقطة" الحدسية تفشل.
3. تعريف الخاصية الصحيحة: تعريف وإثبات التوحيد الهامشي للفراشة (Butterfly Marginal Uniformity) (أي أن توزيع السلك المخرج يكون موحداً عبر مساحة القناع، وبشكل مستقل عن السر).
4. التركيب الاستقرائي: إثبات أنه إذا كانت كل مرحلة تحقق التوحيد الهامشي وتستخدم أقنعة طازجة ومستقلة في كل مرحلة، فإن خط أنابيب NTT المكون من $k$ مرحلة يحافظ على هذه الخاصية.

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

تقدم الورقة ثلاث نتائج رئيسية مدققة آلياً (جميعها بدون استخدام sorry؛ مما يعني عدم وجود بديهيات غير متحقق منها):

أ. جسر $r$ -Bearing (سد ثغرة سابقة)

السياق: أثبت عمل سابق (الورقة 3) أن استقلال القيمة يستلزم ثبات التوزيع الهامشي ولكن فقط في الحالات التي لا تحتوي على عشوائية طازجة ( $r$ -free).
النتيجة: وسع المؤلفون هذا ليشمل حالة $r$ -bearing (مع وجود عشوائية طازجة). لقد أثبتوا أن استقلال القيمة (Value-Independence) يستلزم صفر معلومات متبادلة (MutualInfoZero) (أي صفر معلومات متبادلة بين السر والسلك) في ظل وجود عشوائية طازجة. وهذا يربط بين الاستقلال الجبري والأمان المعلوماتي.

ب. توحيد الفراشة لكل سياق (الرؤية الجوهرية)

الفخ: يثبت المؤلفون رسمياً أن استقلال القيمة عند كل نقطة هو أمر خاطئ لمخرجات الفراشة. تغيير السر يغير بالفعل قيمة السلك حتى مع وجود أقنعة ثابتة.
الحل: يثبتون التوحيد الهامشي للفراشة (Butterfly Marginal Uniformity). لأي فراشة كولي-توكي مع قناع مخرج طازج $m \in \mathbb{Z}_q$ $m \in Z_{q}$ :
- لأي سلك مخرج وأي قيمة مستهدفة $v$ ، يوجد قيمة قناع واحدة فقط $m$ تنتج $v$ .
- هذا يخلق توزيعاً هامشياً موحداً عبر مساحة القناع، وهو مستقل عن السر.
- الشمولية: هذا ينطبق على جميع قيم $q > 0$ (سواء كانت أولية أو مركبة)، وجميع عوامل التدوير (twiddle factors)، وجميع المدخلات.

ج. تركيب خط الأنابيب (النظرية الرئيسية)

النتيجة: خط أنابيب NTT مكون من $k$ مرحلة مع تمويه طازج لكل مرحلة يحقق التوحيد لكل سياق في كل مرحلة.
الآلية: يعتمد الإثبات على حقيقة أن الفراشة هي دالة تآلفية (affine) بالنسبة للقناع (مشابهة لعملية XOR في التمويه البولياني). ولأن العملية خطية/تآلفية، فإن توحيد القناع الطازج ينتقل عبر خط الأنابيب دون تراكم التسريب، بشرط حقن قناع طازج جديد عند كل مرحلة.
الأهمية: هذا يرسخ مبدأ تصميم التمويه الطازج (Fresh Masking Design Principle): لتأمين خط أنابيب NTT، يجب تطبيق أقنعة طازجة مستقلة عند كل حد فاصل بين المراحل.

4. النتائج وتفاصيل الأثر (Artifact)

التحقق الرسمي: يتكون الأثر من 9 نظريات موزعة على 3 ملفات من Lean 4 (حوالي 580 سطراً من الكود).
إحصائيات البناء: تمت صياغة الأداة بحيث تعمل مع 1,738 مهمة بناء، مما نتج عنه 0 خطأ و 0 تحذير.
دراسة الحالة (Adams Bridge): تشرح الورقة الفشل المعماري لمسرع Adams Bridge.
- يقوم Adams Bridge بالتمويه فقط في الجولة 0 (Round 0) من عملية الـ INTT.
- تستمر الجولات اللاحقة بدون تمويه.
- الاستنتاج: بما أن "مبدأ تصميم التمويه الطازج" (النظرية 6.2) قد تم انتهاكه (لا توجد أقنعة طازجة في الجولات 1–3)، فإن نظرية التركيب لا تنطبق، مما يفسر عدم الأمان الهيكلي الذي لوحظ في الدراسات التجريبية السابقة.

5. الأهمية والأثر

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

ملخص القيود والعمل المستقبلي

خطي فقط: يغطي الإثبات الحالي الفراشة التآلفية فقط. أما الأدوات غير الخطية (اختزال باريت) فيتم تناولها في عمل منفصل.
الدرجة الأولى فقط: الإثبات مخصص للدرجة الأولى ( $t=1$ ). يتطلب أمان الدرجة الثانية أقنعة مستقلة لكل زوج مخرج، وهو ما لا يغطيه هذا العمل.
نموذج مثالي: يفترض الإثبات نموذجاً جبرياً نظيفاً، ولا يأخذ في الاعتبار نماذج "الومضات" (glitches)، أو تسريب الانتقال (transition leakage)، أو القنوات الجانبية الزمنية (رغم أن أداة QANARY تعالج التبعيات الهيكلية في RTL).

في الختام، توفر هذه الورقة الأساس الرياضي والتحقق الرسمي المطلوب لتنفيذ مسرعات أجهزة PQC بشكل آمن، مثبتة أن التمويه الطازج لكل مرحلة هو الشرط الضروري والكافي لأمان خطوط أنابيب NTT الخطية.