الأخبار أخرجت ذلك مؤخرًا تم تقديم اقتراح ليتم تضمينه في نواة لينكس شنومكس (أو ربما سيتم ترقيم الفرع 6.0 ، كل هذا يتوقف على قرار Linus Torvalds بسبب تعليقه على إصدار Kernel 5.19).
الاقتراح المقدم هو حول مجموعة من التصحيحات مع تنفيذ آلية RV (التحقق من وقت التشغيل) ، وهي وسيلة للتحقق من التشغيل الصحيح في أنظمة موثوقة للغاية تضمن عدم وجود أعطال.
تصديق يتم إجراؤه في وقت التشغيل عن طريق إرفاق معالجات بنقاط التتبع التي تتحقق من التقدم الفعلي للتنفيذ مقابل نموذج مرجعي حتمي محدد مسبقًا للأتمتة الذي يحدد السلوك المتوقع للنظام.
مطور لينكس ، يذكر دانيال بريستو دي أوليفيرا:
خلال السنوات القليلة الماضية ، كنت أستكشف إمكانية التحقق من سلوك نواة Linux باستخدام Runtime Verification.
Runtime Verification (RV) هي طريقة خفيفة الوزن (لكنها صارمة) تكمل تقنيات التحقق الشاملة الكلاسيكية (مثل فحص النموذج وإثبات النظرية) مع نهج عملي أكثر للأنظمة المعقدة. بدلاً من الاعتماد على نموذج مفصل للنظام (على سبيل المثال ، إعادة تنفيذ مستوى تعليمي) ، يعمل الواقع الافتراضي من خلال تحليل تتبع التنفيذ الفعلي للنظام ، ومقارنته بمواصفات رسمية لسلوك النظام.
يعد استخدام الأتمتة الحتمية للواقع الافتراضي نهجًا راسخًا. في الحالة المحددة لـ Linux kernel ، يمكنك معرفة كيفية نمذجة السلوك المعقد لنواة Linux من خلال هذه المقالة:
دي أوليفيرا ، دانيال بريستو ؛ كوسينوتا ، توماسو ؛ دي أوليفيرا ، رومولو سيلفا. * التحقق الرسمي الفعال لنواة Linux. * في: المؤتمر الدولي لهندسة البرمجيات والأساليب الرسمية. سبرينغر ، شام ، 2019. ص. 315-332.
وما مدى فعالية هذا النهج هنا:
دي أوليفيرا ، دانيال ب. دي أوليفيرا ، رومولو إس. كوسينوتا ، توماسو. * نموذج مزامنة مؤشر الترابط لنواة PREEMPT_RT Linux. * Journal of Systems Architecture، 2020، 107: 101729.
TLDR: يمكن نمذجة السلوك المعقد بطريقة معيارية ، مع حمل مقبول (حتى لأنظمة الإنتاج).
يذكر أن تنقل معلومات نقطة المسار النموذج من حالة إلى أخرى، وإذا كانت الحالة الجديدة لا تتطابق مع معلمات النموذج ، يتم إنشاء تحذير أو تدخل النواة في حالة "ذعر" (على افتراض أن الأنظمة عالية الموثوقية ستكتشف مثل هذه المواقف وتستجيب لها).
نموذج الإنسان الآلي يعرّف الانتقالات من حالة إلى أخرى ويتم تصديرها إلى تنسيق "نقطة" (Graphviz) ، وبعد ذلك يتم ترجمتها باستخدام الأداة المساعدة dot2c إلى تمثيل C ، والذي يتم تحميله في شكل وحدة kernel تتعقب الانحرافات. التنفيذ من نموذج محدد مسبقًا.
يتم وضع فحص النماذج في وقت التشغيل كطريقة أخف وأسهل للتنفيذ للتحقق من صحة التنفيذ في الأنظمة ذات المهام الحرجة ، والتي تكمل الطرق الكلاسيكية للتحقق من الموثوقية ، مثل التحقق من النموذج والبراهين الرياضية على امتثال الكود للمواصفات الواردة بلغة رسمية.
لخص مشرف النظام الفرعي للتتبع ستيفن روستيد الأمر على النحو التالي:
»هذا هو أكبر تغيير لطلب السحب هذا. يقدم التحقق من وقت التشغيل المطلوب لتشغيل Linux على أنظمة الأمان الحساسة. يسمح بإدراج نماذج تلقائية حتمية في النواة ليتم إرفاقها بنقاط التتبع ، حيث ستنقل المعلومات حول نقاط التتبع هذه النموذج من حالة إلى أخرى.
من بين المزايا المذكورة لـ RV هي القدرة على توفير تحقق صارم دون تنفيذ منفصل للنظام بأكمله بلغة نمذجة ، بالإضافة إلى استجابة مرنة للأحداث غير المتوقعة ، على سبيل المثال ، لمنع انتشار فشل الأنظمة الحرجة.
أخيرًا ، إذا كنت مهتمًا بأن تكون قادرًا على معرفة المزيد عنها ، فيمكنك الرجوع إلى التفاصيل في الرابط التالي.
مصدر: https://www.phoronix.com/