⚙️ seL4 Microkernel
مجلد النواة
أول نواة في العالم يُثبَت رياضياً خلوّها من الأخطاء البرمجية
نواة مُثبَتة رسمياً — seL4 هي النواة الوحيدة في العالم التي تم إثبات صحتها رياضياً (Formally Verified). بمعنى أن كل سطر فيها مضمون لا يحتوي على أخطاء أمنية.
دور النواة في النظام
عزل الحاويات
تضمن النواة أن لا توجد أي حاوية يمكنها الوصول إلى ذاكرة حاوية أخرى إلا بتصريح صريح عبر نظام Capabilities. هذا العزل مُطبَّق على مستوى العتاد نفسه.
التواصل الآمن — IPC
توفر قنوات اتصال سريعة وآمنة (Endpoints) لتبادل الرسائل بين الحاويات دون أي مشاركة مباشرة في الذاكرة.
إدارة العتاد
تتولى النواة التحكم الحصري بالمقاطعات (Interrupts) وتقسيم الموارد، وتمنع أي وصول مباشر للعتاد — كما تعلّمنا من خطأ General Protection Fault (0xd).
كيف نتعامل مع النواة؟
01
لا نعدّل النواة أبداً
نحن لا نلمس كود seL4 الداخلي. النواة هي صندوق أسود موثوق.
↓
02
نبني ونكوّن فقط
نستخدم CMake عبر سكربتات مجلد scripts/ لبناء النواة وضبط إعداداتها.
↓
03
النواة تعمل في الخلفية
بعد الإقلاع، تترك النواة إدارة كل شيء لحاوية init التي نكتبها نحن بلغة Rust.