التشويش للتحقق من صحة أمان SoC. الابتكار في التحقق

التشويش هو التحقق من البرامج ما هو العشوائي هو التحقق من الأجهزة. هل يمكن لنهج التشويش تحسين اختبار أمان الأجهزة؟ بول كننغهام (مدير عام، التحقق في Cadence)، راؤول كامبوسانو (Silicon Catalyst، رجل أعمال، المدير الفني السابق لشركة Synopsys) وأنا نواصل سلسلتنا حول أفكار البحث. كما هو الحال دائما، ردود الفعل موضع ترحيب.

الابتكار

اختيار هذا الشهر هو HyperFuzzing للتحقق من صحة أمان SoC. قدم المؤلفون هذه الورقة في ICCAD 2020. وهم من IIT Kanpur.

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

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

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

رأي بول

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

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

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

فكرة التأكيدات على عمليات المحاكاة المتعددة قوية جدًا. أتساءل عما إذا كان من الممكن توسيع SystemVerilog بشكل نظيف لدعم هذه الأنواع من التأكيدات. وهذا يمكن أن يفتح الباب أمام بعض الإضافات المحلية المقنعة للمحاكاة التجارية والأدوات الرسمية. قد يكون الاحتمال الآخر هو توسيع معيار التحفيز المحمول (PSS) الجديد ليشمل التأكيدات التي تمتد عبر اختبارات متعددة تم إنشاؤها.

هذه الورقة سهلة القراءة وممتعة، على الرغم من أنني أرغب في الحصول على مزيد من التفاصيل حول النتائج. يدعي المؤلفون أن الحل الذي توصلوا إليه وجد ثغرات أمنية في اختبار SoC مفتوح المصدر، ولكن لا توجد تفاصيل حول ماهية هذه الثغرات أو كيفية مقارنة نهجهم مع الأساليب الأخرى في الأدبيات التي يمكن تطبيقها للعثور على نفس الثغرات.

رأي راؤول

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

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

وجهة نظري

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

شارك هذا المنشور عبر: المصدر: https://semiwiki.com/eda/299391-fuzzing-to-validate-soc-security-innovation-in-verification/