أعلنت مؤسسة RISC-V أنها تحققت كيف يعمل microkernel seL4 في الأنظمة ذات بنية مجموعة التعليمات RISC-V. حيث يتم تقليل عملية التحقق إلى إثبات رياضي لموثوقية seL4 ، مما يشير إلى الامتثال الكامل للمواصفات المحددة بلغة رسمية.
يتيح اختبار الموثوقية استخدام seL4 في أنظمة المهام الحرجة القائمة على معالجات RISC-V RV64، الأمر الذي يتطلب مستوى أعلى من الموثوقية ولا يضمن الفشل.
يمكن لمطوري البرمجيات الذين يعملون على قمة نواة seL4 التأكد تمامًا من أنه في حالة حدوث عطل في جزء واحد من النظام ، فلن ينتشر هذا الفشل إلى بقية النظام ، وعلى وجه الخصوص ، إلى أجزائه المهمة. .
حول seL4
هندسة seL4 يتميز بإزالة الأجزاء لإدارة موارد kernel في مساحة المستخدم واستخدام نفس طرق التحكم في الوصول لهذه الموارد مثل موارد المستخدم.
النواة الصغيرة لا تقدم تجريدات عالية المستوى مستعد بالفعل لإدارة الملفات والعمليات واتصالات الشبكة وما إلى ذلك ، ولكن بدلاً من ذلك يوفر فقط الحد الأدنى من الآليات للتحكم في الوصول إلى مساحة العنوان الفعليةوالمقاطعات وموارد المعالج.
يتم تنفيذ عمليات تجريدية وأدوات تحكم عالية المستوى للتفاعل مع الكمبيوتر بشكل منفصل أعلى النواة الدقيقة في شكل مهام يتم تنفيذها على مستوى المستخدم.
يتم تنظيم وصول مثل هذه المهام إلى الموارد المتاحة في microkernel من خلال تعريف القواعد.
يوفر RISC-V نظامًا مفتوحًا ومرنًا من تعليمات الآلة التي يسمح بإنشاء معالجات دقيقة للتطبيقات التعسفية ، دون الحاجة إلى استقطاعات وبدون فرض شروط للاستخدام.
يتيح لك RISC-V إنشاء معالجات SoCs مفتوحة تمامًا. حاليًا ، استنادًا إلى مواصفات RISC-V ، تقوم العديد من الشركات والمجتمعات بموجب تراخيص مجانية مختلفة (BSD و MIT و Apache 2.0) بتطوير عشرات المتغيرات من نوى المعالجات الدقيقة المنتجة بالفعل و SoCs والرقائق.
ظل دعم RISC-V موجودًا منذ إصدار Glibc 2.27 و binutils 2.30 و gcc 7 و Linux 4.15 kernel.
حول اختبار seL4 microkernel
في البداية ، microkernel تم التحقق من seL4 لمعالجات ARM 32 بت، لاحقًا لمعالجات x86 64 بت.
ويلاحظ أن الجمع بين بنية الأجهزة RISC-V المفتوحة مع النواة الصغيرة المفتوحة سيحقق seL4 مستوى جديدًا من الأمان، حيث يمكن أيضًا التحقق من مكونات الأجهزة المستقبلية بشكل كامل ، وهو أمر مستحيل تحقيقه لبنى الأجهزة الاحتكارية.
عندما نتحقق من seL4 ، يجب أن نفترض أن الجهاز يعمل بشكل صحيح (أي كما هو محدد). يفترض ذلك وجود مواصفات لا لبس فيها في المقام الأول ، وهذا ليس هو الحال بالنسبة لجميع الأجهزة.
ولكن حتى في حالة وجود مثل هذا التحديد ، ويكون رسميًا (أي مكتوب في شكلية رياضية تدعم التفكير الرياضي حول خصائصه) ، كيف نعرف أنه يجسد بالفعل سلوك الأجهزة؟
الحقيقة هي أننا يمكن أن نكون متأكدين تمامًا من أنها ليست كذلك. لا تختلف الأجهزة عن البرامج في أن كلاهما به أخطاء.
لكن امتلاك ISA مفتوح له مزايا تتجاوز كونه خاليًا من حقوق الملكية. واحد هو أنه يسمح بتطبيقات الأجهزة مفتوحة المصدر.
عند التحقق من seL4 ، يُفترض أن المعدات تعمل على النحو المشار إليه وأن المواصفات تصف سلوك النظام بشكل كامل ، ولكن في الحقيقة المعدات ليست خالية من الأخطاء ، وهو ما يتضح جيدًا من خلال المشكلات التي تظهر بانتظام في آلية تنفيذ المضاربة تعليمات.
تعمل الأنظمة الأساسية للأجهزة على تبسيط تكامل التغييرات المتعلقة بالأمان ، على سبيل المثال ، لحظر جميع قنوات التسرب المحتملة من خلال قنوات الجهات الخارجية ، حيث يكون التخلص من مشكلة بواسطة الأجهزة أكثر فاعلية من محاولة إيجاد حلول بواسطة البرامج.
أخيرًا ، إذا كنت تريد معرفة المزيد عنها ، فيمكنك الرجوع إلى الملاحظة الموجودة في الرابط التالي.
بالنسبة لي ، هذا المعالج هو الشيء الذي يناديني كثيرًا. يبقى فقط لبعض أجهزة الكمبيوتر السمينة أن تصنع جهاز كمبيوتر يمكننا شراؤه.
مشكلة ARM هي أمر يثير غضبي ، لقد رأينا بالفعل ما حدث مع Huawei مع العقوبات. أنا واضح أنه بالنسبة لـ RISC-V هو حل أفضل على جميع المستويات. في الوقت الحالي ، وضعت Huawei عينها عليها بالفعل ، وربما في المستقبل سيكون لديهم معدات بهذا الميكرو. إذا كان الأمر كذلك ، فمن المؤكد أنه سيكون هناك المزيد من الشركات التي تتبناها وبالنسبة لي سيكون هذا هو النموذج المثالي وقبل كل شيء أن التوزيعات تدعمه وليس فقط ARM كما يحدث مع معظم.
10