Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts
تقدم Granite منهجية تأسيسية نمطية تتحقق من كل من الصحة الوظيفية وعدم التسريب لمعالجات RTL من خلال إنشاء تكافؤ تتبع مع عقود تسريب ISA حتمية، مما يتيح تركيب براهين الأجهزة والبرمجيات لإقصاء المواصفات الوسيطة من قاعدة الحوسبة الموثوقة.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك تبني سيارة سباق فائقة السرعة. تريدها أن تكون سريعة للغاية، لذا تضيف شواحن توربينية، ونظام توجيه تنبؤي، ونظامًا يتوقع المنعطف الذي ستسلكه تاليًا. لكن هناك عقبة: إذا أصدر محرك السيارة صوت "طقطقة" محددًا فقط عندما تنعطف يسارًا، فقد يتمكن جاسوس متسلل يستمع من الجوانب من معرفة مسارك بالكامل بمجرد سماع الضجيج. في عالم الرقائق الحاسوبية، يُسمى هذا "قناة جانبية زمنية" (timing side channel). لسنوات، حاول المبرمجون كتابة أكواد تستغرق نفس القدر من الوقت تمامًا بغض النظر عن البيانات السرية التي تتعامل معها، مثل جاسوس يحاول السير في ممر دون إحداث أي صوت. ولكن مع ازدياد سرعة وذكاء الرقائق، بدأت هذه الرقائق في إصدار ضوضاء صغيرة غير متوقعة — مثل توقف مفاجئ لتفقد مرآة أو دفعة من السرعة — والتي كشفت الأسرار عن غير قصد. تتناول هذه الورقة الفكرة المرعبة المتمثلة في أنه حتى لو كان الكود الخاص بك مثاليًا، فإن الأجهزة نفسها قد تسرب أسرارك من خلال إيقاع نبضات قلبها.
قام الباحثون وراء هذا العمل، المعروفون باسم "جرانيت" (Granite)، ببناء طريقة جديدة لإثبات رياضي بأن شريحة الكمبيوتر تحافظ على أسرارها بأمان. لم يكتفوا بالتخمين أو إجراء الاختبارات؛ بل ابتكروا حجة رياضية صارمة ومنظمة خطوة بخطوة تربط القواعد عالية المستوى لكيفية تصرف الكمبيوتر (مجموعة التعليمات - ISA) وصولاً إلى الأسلاك والترانزستورات الدقيقة (RTL). إن اكتشافهم الرئيسي هو طريقة لإثبات أن توقيت الشريحة يتحدد فقط بناءً على الأشياء المسموح بأن تكون علنية، مثل الزر الذي تم ضغطه، وليس بناءً على البيانات السرية التي تعالجها، مثل كلمة مرور أو مفتاح تشفير. إنهم ينفون صراحة فكرة أنه يمكنك الوثوق في شريحة لمجرد أنها تبدو جيدة أو لأنها اجتازت اختبارات قياسية؛ ويظهرون أنه بدون هذا النوع المحدد من الإثبات، فإن التسريبات الخفية ستكون موجودة بشكل شبه مؤكد. هم لا يقترحون فقط أن هذا يعمل؛ بل أثبتوا ذلك رسميًا لتصميم معالج تم تصنيعه بنجاح لـ FPGA، رغم أنه لم يتم دمجه بعد في نظام كامل (System-on-Chip) لاختبار ما بعد التصنيع.
قصة كاشف الشريحة العظيم
تخيل المعالج الحاسوبي كمطبخ صاخب وفوضوي في مطعم فاخر. الطهاة (الأجهزة/Hardware) يقومون بإعداد الوجبات (تشغيل البرامج) للزبائن. "بنية مجموعة التعليمات" (ISA) هي قائمة الطعام وكتاب الوصفات. هي تخبر المطبخ: "إذا تلقيت طلبًا لبرغر، يجب عليك في النهاية تقديم برغر". لكن القائمة لا تخبرك كم من الوقت سيستغرق صنع البرغر، أو متى يمسك الطاهي بالسكين.
في الأيام الخوالي، كانت التعليمات للطهاة أن يكونوا "ثابتي الوقت" (constant-time). كان هذا يعني أنه يتعين عليهم تقطيع الخضروات بنفس السرعة تمامًا سواء كان الزبون يطلب سلطة أو شريحة لحم، حتى لا يتمكن جاسوس يراقب من النافذة من معرفة ما يتم طبخه من خلال إيقاع التقطيع. ولكن بعد ذلك، أصبح المطبخ سريعًا جدًا. بدأ الطهاة في استخدام "التخمين" (speculation) — كانوا يتوقعون ما يريده الزبون ويبدأون في تقطيع البصل قبل تأكيد الطلب حتى. هذه اللعبة من التخمين خلقت ضوضاء جديدة وعرضية: الوقت الذي استغرقه إدراك الخطأ، أو الوقت الذي استغرقه الإمساك بتوابل معينة، بدأ يسرب المعلومات. يمكن للجاسوس أن يستمع للمطبخ ويستنتج: "آه، لقد تردد الطاهي لمدة 0.0001 ثانية؛ لا بد أنه كان يطبخ شيئًا يحتوي على بصل سري!"
هنا يأتي دور جرانيت (Granite)، مفتش المطبخ النهائي. جرانيت لا يكتفي بمراقبة الطهاة فحسب؛ بل يعيد كتابة قواعد المطبخ لضمان عدم هروب أي أسرار من خلال توقيت التقطيع.
سحر "الطاهي الظل"
تكمن عبقرية جرانيت في خدعة ذكية تتضمن "طاهي الظل". تخيل أن لديك الطاهي الحقيقي، الذي يعرف جميع الوصفات السرية (البيانات السرية). ولديك أيضًا طاهي ظل، وهو معصوب العينين ويعرف فقط الأجزاء العلنية من الطلب (البيانات العلنية).
تقول طريقة جرانيت: "سنثبت أن الطاهي الحقيقي وطاهي الظل يتحركان في خطى متزامنة ومثالية". إذا استغرق الطاهي الحقيقي 5 ثوانٍ لتقطيع بصلة لأن البصلة كانت كبيرة، يجب أن يستغرق طاهي الظل أيضًا 5 ثوانٍ بالضبط، رغم أن طاهي الظل لا يعرف أن البصلة كانت كبيرة. توقيت طاهي الظل مدفوع فقط بالطلب العلني. إذا اعتمد توقيت الطاهي الحقيقي على سر (مثل نوع البصلة)، فسوف يختل التزامن بين الطاهيين، وسيفشل الإثبات.
لجعل هذا يعمل، يقدم جرانيت "المُحرك" (Driver) و"الشاهد" (Witness).
- المُحرك هو مثل بندول ضبط الإيقاع (metronome) الذي يستمع فقط للطلب العلني. هو يقرر متى يجب أن يتحرك المطبخ للأمام، مما يضمن أن توقيت أفعال المطبخ محكوم فقط بما يريد الزبون أن يُعرف، وليس بالمكونات السرية.
- الشاهد هو مكان مخصص للأجزاء الفوضوية وغير المتوقعة في المطبخ (مثل تأخير عشوائي لأن المقلاة كانت ساخنة). يقول الشاهد: "حسنًا، نحن لا نهتم بالضبط بما يحدث هنا، طالما أنه لا يعتمد على السر".
من خلال إثبات أن المطبخ الحقيقي يتصرف تمامًا مثل مطبخ يديره المُحرك والشاهد، يثبت جرانيت أن إيقاع المطبخ (التوقيت) لا يمكنه مستحيلاً كشف المكونات السرية.
اللغز التركيبي (Modular)
أحد أصعب أجزاء فحص مطبخ كامل هو أنه كبير جدًا بحيث لا يمكن النظر إليه دفعة واحدة. يحل جرانيت هذه المشكلة عن طريق تقسيم المطبخ إلى محطات صغيرة ومستقلة: محطة التقطيع، محطة الشواء، محطة التقديم.
يثبت جرانيت أن كل محطة آمنة بمفردها. على سبيل المثال، يتم فحص محطة "الضرب" (التي تقوم بالعمليات الحسابية) للتأكد من أنه إذا استغرقت وقتًا أطول لضرب رقمين، فذلك لأن الأرقام كانت أصفارًا (وهو أمر مسموح بمعرفته)، وليس بسبب قيمة سرية ما. وبمجرد إثبات سلامة كل محطة على حدة، يقوم جرانيت بتجميعها معًا مثل قطع الليغو. ولأن الإثبات "تركيبي" (modular)، فإذا استبدلت محطة الشواء بأخرى أسرع، فلن تحتاج إلى إعادة فحص المطبخ بأكمله؛ بل تتحقق فقط من المحطة الجديدة، ويظل النظام بأكمله آمنًا.
الحكم النهائي
لم يكتف الباحثون بالحديث عن هذا؛ بل بنوا تصميم معالج وأجروا إثباتهم عليه. لقد أخذوا قطعة من البرمجيات التي كانت معروفة بالفعل بأنها "ثابتة الوقت" (برنامج تشفير يسمى Salsa20) وأثبتوا أنه عندما يعمل على تصميم المعالج الخاص بهم، فإنه لا يسرب أي أسرار عبر التوقيت.
هذا أمر بالغ الأهمية لأنه يغير ما يجب عليك الوثوق به. عادةً، عليك الوثوق بعقد معقد بين البرمجيات والأجهزة. يوضح جرانيت أنه إذا ربطت إثبات الأجهزة الخاص بهم مع إثبات برمجي موثق، فيمكن حذف عقد "الأجهزة-البرمجيات" نفسه من قائمة الأشياء الموثوقة. ومع ذلك، لا يزال الإثبات يعتمد على بعض المكونات الأساسية، مثل التعريف الرسمي لعقد مجموعة التعليمات والأداة التي تترجم الكود إلى وصف الأجهزة، والتي تظل ضمن "قاعدة الحوسبة الموثوقة" (Trusted Computing Base). حتى أنهم وجدوا خطأً في تصميمهم الخاص: أدركوا أن الكتابة إلى بعض مفاتيح التحكم (CSRs) يمكن أن تسرب معلومات، وقاموا بإصلاحها قبل اكتمال الإثبات.
باختصار، جرانيت هو طريقة جديدة لبناء رقائق حاسوبية مضمونة رياضيًا للحفاظ على أسرارها، حتى عندما تعمل بسرعة وتخمّن وتصدر ضجيجًا. إنه يحول مطبخ الحوسبة الحديثة الفوضوي والصاخب إلى حصن صامت يحفظ الأسرار، ويثبت أنه يمكنك الحصول على السرعة والأمان في آن واحد.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.