التحقق الرسمي من بنية التشفير المعزولة

التحقق الرسمي من بنية التشفير المعزولة

الطابع الزمني: 13 سبتمبر 2023 ، الساعة 4:01 مساءً
عقدة المصدر: 2878420

نشر باحثون في جامعة برينستون وجامعة ميشيغان وكلية لافاييت ورقة فنية بعنوان "التحقق الأمني ​​من البنى منخفضة الثقة".

المستخلص:

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

أعثر على ورقة فنية هنا. نُشرت في سبتمبر 2023 (نسخة ما قبل الطباعة).

تان، تشينهان، يوناثان فيسيها، شيبو تشين، لورين بيرناكي، جان بابتيست جينين، شاراد مالك، وتود أوستن. "التحقق الأمني ​​من البنى منخفضة الثقة." arXiv ما قبل الطباعة arXiv:2309.00181 (2023).

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

الطابع الزمني:

اكثر من شبه هندسة