السلام عليكم
فرع جديد من أنوية نظم التشغيل تسمّى Micro-Kernel ، وفكرتها تقوم على تقليص حجم النواة و التخلّص من بعض الوظائف ، فمثلاً الجزء الخاص بمسوّقات التشغيل Drivers ، تم إزالتها من kernel mode ونقلها إلى user mode ، بعكس الأمر مع Linux kernel .
ظهرت قبل فترة ( لا أعرف متى بصراحة ) ، عائلة من أنوية نظم التشغيل الصغيرة ، تحمل اسم L4 ، وظهر مشروع بحثي مبني على L4 يحمل الاسم seL4 ، وبهذا نكون وصلنا لموضوعنا . هذه النواة الصغيرة ، لا تحمل أي Bug ، ومثبت هذا بطريقة رياضية Formal Method ، وهي تأكيد على أن implementation لنواة نظام التشغيل مطابقة تماماً ( تماماً ) للمواصفات . طبعاً هم فرضوا أمور مثل : أن أخطاء العتاد Hardware خارج الحسابات ، و غيرها من الأمور الأخرى التي تعتبر خارج الحالات الطبيعية ، ولهم اقتباس جميل من انشتاين :
As far as the laws of mathematics refer to reality, they are not certain; and as far as they are certain, they do not refer to reality
المهم ، أنهم أثبتوا أن هذه النواة خالية من مشاكل :
Buffer overflows ، Null pointer dereferences ، Pointer errors in general ، Memory leaks و Arithmetic overflows and exceptions .
و الفكرة هي بأنك إذا كتبت مواصفات بشكل صحيح ( وهذا أسهل من كتابة implementation ) ، ففي الغالب أنك ستحدد ما تريد من مشروعك ، لأن الأفكار ستعبر عنها بسهولة أكبر من كتابة code ، وبالتالي عند عمل implementation ، يجب أن تثبت علمياً أنك طبّقت حرفياً ما جاء في هذه المواصفات ، وبالتالي مشروعك خالي من أي Bug :
Does seL4 have zero bugs?
Our proof states that, if the proof assumptions are true, the seL4 kernel has no deviations from its specification. There may still be unexpected features in the specification and one or more of the assumptions may not apply. In particular, the remaining implementation details below the level of the C programming language may still contain as many or few defects as other well-engineered software. The proof and assumption page has the longer version.
يمكن استخدام seL4 ، في embedded systems ، التي تحتاج لأمان عالي ، و يبدو أنه يمكن استخدمها لأي هدف آخر .
المهم ، الكلام كبير و شخصياً ما فهمت شيء بشكل حقيقي ، لكن ما فيه مانع أن تحاول تقرأ و تستفيد ،( أشكر الاخ عبدالعزيز - زميل في العمل - على التوضيح ) ،
عموماً ، للاستزادة:
