💻 computer science

Controller Datapath Aware Verification of Masked Hardware Generated via High Level Synthesis

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

المؤلفون الأصليون: Nilotpola Sarma, Vaishali Ghanshyam Chaudhuri, Chandan Karfa

نُشر 2026-03-20

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

CC BY 4.0

المؤلفون الأصليون: Nilotpola Sarma, Vaishali Ghanshyam Chaudhuri, Chandan Karfa

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

الصورة الكبيرة: بناء خزنة سرية

تخيل أنك تقوم ببناء خزنة عالية التأمين لتخزين وصفة سرية (الخوارزمية التشفيرية). تريد التأكد من عدم قدرة أي شخص على سرقة الوصفة من خلال مراقبة كمية الكهرباء التي تستهلكها الخزنة أثناء عملها. يُعرف هذا باسم هجوم القناة الجانبية للطاقة (Power Side-Channel Attack).

لإيقاف ذلك، تستخدم تقنية تسمى التمويه (Masking).

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

المشكلة: البنّاء "المسرع"

تقليديًا، يتم بناء هذه الخزنات المموّهة يدويًا بواسطة مهندسين خبراء. إنها عملية بطيئة، مملة، ومن السهل ارتكاب الأخطاء فيها.

لتسريع العملية، بدأ المهندسون في استخدام التوليف عالي المستوى (High-Level Synthesis - HLS).

التشبيه: فكر في الـ HLS كروبوت بناء آلي فائق السرعة. تعطيه مخططًا (كود برمجي)، فيقوم فورًا ببناء الخزنة المادية (الأجهزة/Hardware) من أجلك. إنه رائع لأنه يوفر الوقت ويسمح لك بتجربة تصميمات مختلفة بسرعة.

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

الإنذار الكاذب: المفتش شديد الارتياب

بعد أن يبني الروبوت الخزنة، تحتاج إلى مفتش للتحقق مما إذا كان التمويه لا يزال يعمل.

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

الحل: المحقق "الواعي بالحالة"

قام مؤلفو هذه الورقة البحثية بإنشاء أداة جديدة تسمى MaskedHLSVerif.

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

لماذا يهم هذا الأمر؟

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

ملخص في كبسولة

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

إليك ملخص تقني مفصل للورقة البحثية بعنوان "التحقق من المتحكم-المسار البياني الواعي للمقنعات الموَلَّدة عبر التركيب عالي المستوى (HLS)."

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

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

المشكلة الجوهرية:
صُممت أدوات التحقق الرسمي الحالية للأجهزة المقنعة (مثل REBECCA) للعمل مع مسارات بيانات ثابتة. ومع ذلك، تقوم أدوات HLS بتحسين التصاميم عبر مشاركة الموارد (مثل استخدام ضارب واحد لعمليات متعددة عبر دورات زمنية مختلفة). وهذا يخلق بنية "متحكم-مسار بياني" (Controller-Datapath) مدفوعة بآلة حالة محدودة (FSM) ومبدلات (MUXes).

القصور في الأدوات الحالية:

الإيجابيات الكاذبة (False Positives): تقوم أدوات مثل REBECCA بإجراء تحليل تركيبي "ساذج". فهي تفترض أن جميع مجموعات المدخلات الممكنة تركيبياً لمبدل (MUX) هي مدخلات يمكن الوصول إليها.
الواقع: في التصميم الموَلَّد عبر HLS، يتحكم نظام الحالة المحدودة (FSM) في خطوط اختيار المبدلات (MUX select lines)، مما يضمن حدوث مجموعات محددة وصحيحة فقط من المدخلات في حالات معينة. لذا، فإن العديد من المجموعات الممكنة نظرياً (مثل خلط الحصص من فترات زمنية مختلفة) لا يتم تنفيذها أبداً.
النتيجة: تقوم الأدوات الحالية بفحص هذه المجموعات غير القابلة للوص reach، وتكتشف "تسريبات" لا وجود لها في الأجهزة الفعلية، وتُبلغ خطأً بأن التصميم غير آمن (إيجابيات كاذبة). وهذا يمنع اعتماد تقنية HLS في تصميم الأجهزة الآمنة.

2. المنهجية: MaskedHLSVerif

يقترح المؤلفون MaskedHLSVerif، وهو تدفق عمل للتحقق يقوم بـ التحقق الرسمي لكل حالة على حدة (state-wise formal verification) للقضاء على الإيجابيات الكاذبة الناتجة عن مشاركة الموارد.

الخطوات الرئيسية في التدفق:

توليد HLS: توليد تصميم RTL المقنع من مواصفات C/C++ مقنعة باستخدام أداة HLS (مثل Vitis Hls).
استخراج FSM: استخراج حالات الآلة (FSM) من تصميم RTL الموَلَّد.
التقسيم حسب الحالة (Unrolling):
- بدلاً من التحقق من التصميم بأكمله دفعة واحدة، تقوم الأداة بتقسيم التصميم إلى تصميمات فرعية أصغر ( $D_0, D_1, \dots, D_n$ )، واحد لكل حالة من حالات الـ FSM.
- التبعية المتكررة: من الضروري أن يتضمن كل تصميم فرعي لكل حالة ( $D_x$ ) ليس فقط العمليات النشطة في الحالة $x$ ، بل أيضاً جميع العمليات التابعة لها بشكل متكرر من الحالات السابقة. هذا يضمن أن الإشارات الوسيطة يتم تسميتها بشكل صحيح بناءً على المدخلات الأصلية.
انتشار التسميات (Label Propagation):
- يتم تسمية إشارات المدخلات كـ حصص (Shares)، أو أقنعة (Masks)، أو قيم عامة (Public).
- يتم نشر هذه التسميات عبر التصميمات الفرعية لكل حالة. ولأن التصميمات الفرعية تتضمن سلسلة التبعية الكاملة، فإن تسميات الإشارات الوسيطة تُشتق مباشرة من المدخلات الأصلية، مما يتجنب تعقيد إعادة حساب التسميات للعقد الوسيطة.
التحقق الرسمي:
- يتم تغذية كل تصميم فرعي لكل حالة ( $D_x$ ) في محرك REBECCA (محرك التحقق الأساسي) جنباً إلى جنب مع ملف التسمية الخاص به.
- يقوم REBECCA بالتحقق من أمن المسار البياني النشط لتلك الحالة المحددة، متجاهلاً تركيبات المبدلات (MUX) غير القابلة للوصول.
التجميع:
- إذا اجتازت جميع التصميمات الفرعية التحقق، يُعتبر التصميم الأصلي الموَلَّد عبر HLS آمناً.
- إذا فشلت حالة معينة، تحدد الأداة الحالة والموقع الدقيقين لخلل التقنيع.

السلامة النظرية:
يثبت المؤلفون أن هذا النهج سليم. بما أن كل مسار تنفيذ صالح للتصميم الأصلي يتوافق مع تسلسل من العمليات التي يتم التقاطها في تصميم فرعي واحد على الأقل لكل حالة، فإن التحقق من جميع التصميمات الفرعية يضمن أمن الكل.

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

تحديد القصور: تحدد الورقة رسمياً أن أدوات الحالة الراهنة (SOTA) تفشل في التصاميم الموَلَّدة عبر HLS بسبب عدم قدرتها على التمييز بين حالات المسار البياني القابلة للوصول وغير القابلة للوصول في البنى ذات الموارد المشتركة.
تحليل الأثر: تناقش الورقة كيف يمكن لتحسينات HLS المحددة (مثل إعادة الارتباط - Reassociation، وتوازن التعبيرات - Expression Balancing) أن تكسر أمن التقنيع عن غير قصد عن طريق تغيير ترتيب العمليات أو إزالة خطوات إعادة التقنيع الضرورية.
تدفق أداة مبتكر (MaskedHLSVerif): أول إطار عمل للتحقق من الأجهزة المقنعة الموَلَّدة عبر HLS من خلال تجريد المسار البياني النشط لكل حالة FSM، مما يقضي على الإيجابيات الكاذبة.
كشف العيوب: قادرة الطريقة على اكتشاف ليس فقط المشكلات الهيكلية، بل أيضاً الثغرات الأمنية الناجمة عن تحسينات HLS (مثل أخطاء إعادة الارتباط).

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

قام المؤلفون بتقييم الأداة على ستة اختبارات معيارية تشفيرية تم توليدها بواسطة Vitis HLS، تشمل:

ضاريات متسلسلة مقنعة باستخدام مخططات التقنيع DOM و HPC1 و HPC2 و COMAR.
تنفيذات S-box لخوارزمية PRESENT المقنعة باستخدام DOM و HPC1.

التجربة 1: التحقق من الاختبارات المعيارية القياسية

الإعداد: التحقق من الاختبارات الستة باستخدام كل من REBECCA (مباشرة) و MaskedHlsVerif.
النتيجة:
- REBECCA: سجلت إيجابيات كاذبة لجميع التصاميم الستة (أبلغت خطأً أنها غير آمنة بسبب تركيبات المبدلات غير القابلة للوصول).
- MaskedHLSVerif: تحققت بشكل صحيح من جميع التصاميم باعتبارها آمنة.
- التحقق: أكد المؤلفون أمن الـ RTL باستخدام TVLA (تقييم تسرب ناقل الاختبار) على عمليات محاكاة مستوى البوابة، مما أثبت أن التصاميم كانت بالفعل آمنة وأن نتائج REBECCA كانت إيجابيات كاذبة.

التجربة 2: اكتشاف العيوب الناجمة عن التحسين

الإعداد: قام المؤلفون بتفعيل تحسين HLS متعمد (#pragma HLS EXPRESSION_BALANCE) على ضارب DOM متسلسل. تسبب هذا التحسين في إعادة ارتباط عمليات التقنيع، مما خلق خللاً حقيقياً في التقنيع من الدرجة الأولى.
النتيجة:
- حدد MaskedHLSVerif التصميم على أنه غير آمن في الحالة الثانية.
- حدد بدقة مكان التسريب (القيم السرية غير المقنعة في مجموعة التسميات) الناتج عن إعادة الارتباط، مما أظهر قدرته على كشف الانتهاكات الأمنية الناتجة عن تحسينات HLS.

5. الأهمية

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