sEL4

📅 آخر تحديث: ١ أغسطس ٢٠٢٦
✍️ نُشر في: ١ أغسطس ٢٠٢٦
📷 يحتوي على 1 صور
الموسوعة الحرة

seL4 ( الطبقة الرابعة المحسّنة أمنيًا ) هي نواة مصغّرة مفتوحة المصدر، عالية الموثوقية ، وقائمة على القدرات . ترث خصائص الأداء والتصميم لسلسلة نواة الطبقة الرابعة المصغّرة، ولكنها تُنفّذ باستخدام أساليب عالية الموثوقية. [ 1 ] [ 2 ] تستخدم seL4 التحقق الرياضي الرسمي لإثبات سرية النظام وسلامته وتوافره [ 3 ] ، بالإضافة إلى خصائص أخرى . وقد أُدرجت الورقة البحثية الأولية التي تُبيّن آلية التحقق من seL4 في قاعة مشاهير ACM SIGOPS لعام 2019. [ 4 ]

تاريخ

طُوِّرت نواة seL4 المصغرة من الصفر، متأثرةً بعائلة نواة L4 المصغرة، بهدف واضح هو تمكين التحقق الرسمي الشامل [ 5 ] مع الحفاظ على الأداء العالي. [ 6 ] في عام 2009، أعلن مشروع seL4 عن برهان مُدقَّق آليًا على صحة الوظائف، يمتد من المواصفات الرسمية إلى التنفيذ بلغة C. [ 7 ]

في يوليو 2014، أصدرت NICTA بالتعاون مع شركاء صناعيين مصادر نواة seL4 وعناصر التحقق منها كمصدر مفتوح. [ 8 ] [ 9 ]

في 7 أبريل 2020، تم إطلاق مؤسسة seL4 لدعم الحوكمة وتطوير النظام البيئي والإشراف طويل الأجل؛ وقد استضافتها في البداية مؤسسة لينكس. [ 10 ] [ 11 ]

بنيان

يُعدّ seL4 نظامًا بسيطًا للغاية ، حتى بالمقارنة مع أنوية L4 السابقة: فهو يقتصر على إدارة الذاكرة/عزل العمليات وجدولة العمليات - أما باقي العمليات فتُدار خارج وضع النواة. عند بدء التشغيل، تُخصّص نواة seL4 ذاكرة كافية لنفسها بشكل ثابت، ثم تُسلّم جميع الذاكرة والقدرات المتبقية إلى عملية أولية في مساحة المستخدم. يُشبه seL4 برنامج تشغيل وحدة المعالجة المركزية أكثر من أنوية مصغّرة تجارية أخرى مثل Mach و QNX و Minix . [ 12 ] كان الدافع الرئيسي هو تمكين مُصمّمي الأنظمة من حرية اختيار السياسات والبنية، ولكنه يُسهّل أيضًا عملية التحقق ويُقلّل من أخطاء ذاكرة التخزين المؤقت. [ 13 ] [ 14 ] [ 1 ]

التحكم في الوصول القائم على القدرات

يستخدم نظام seL4 نموذجًا قائمًا على الصلاحيات للتحكم في جميع عمليات الوصول إلى موارد الذاكرة ونواة النظام. يُمكّن هذا من تحليل وإدارة تدفق الموارد والمعلومات بطريقة برمجية (بدلاً من سياسات الأمان والبنية الموحدة). في هذا النموذج، تُعدّ الصلاحية رمزًا غير قابل للتزوير يُشير إلى كائن في نواة النظام ويُشفّر العمليات التي يُمكن إجراؤها عليه. تُخزّن الصلاحيات في جداول تُديرها النواة تُسمى عُقد الصلاحيات (CNodes)، والتي تُشكّل مساحة أسماء هرمية تُشابه بنية دليل نظام الملفات. تحتوي عُقدة الصلاحيات على خانات للصلاحيات، وهي نفسها كائن في نواة النظام لا يُمكن الوصول إليه إلا من خلال صلاحية، مما يسمح بتفويض أو تقسيم أو إلغاء صلاحية الوصول إلى الموارد بشكل صريح. [ 15 ]

في لغة seL4، تُمثَّل الذاكرة الفعلية مبدئيًا على أنها إمكانيات ذاكرة غير مُصنَّفة ، تُمنح صلاحية الوصول إلى مناطق خام من ذاكرة الوصول العشوائي (RAM) ولكنها لا تُقابل كائنات قابلة للاستخدام. تُحوَّل الذاكرة غير المُصنَّفة إلى كائنات نواة مُصنَّفة عبر عملية إعادة تصنيف . تُسجِّل النواة العلاقات بين الذاكرة غير المُصنَّفة والكائنات المُشتقة منها في شجرة اشتقاق الإمكانيات (CDT)، مما يسمح للنظام بفرض إعادة استخدام آمنة للذاكرة: يجب إزالة جميع الإمكانيات المُشتقة من منطقة غير مُصنَّفة قبل إعادة تخصيص تلك المنطقة. تستبدل هذه الآلية مُخصِّصات النواة الضمنية بدورة حياة ذاكرة صريحة وقابلة للتدقيق تحت سيطرة التطبيق. [ 15 ]

تُدار الذاكرة الافتراضية أيضًا بواسطة الصلاحيات. تمنح صلاحية الوصول إلى إطار ذاكرة ما القدرة على ربط هذا الإطار بمساحة عنوان، وذلك وفقًا لحقوق الوصول المُضمنة في الصلاحية. تُنشأ مساحات العناوين نفسها من كائنات جداول الصفحات التي تُنشأ بدورها من ذاكرة غير مُصنفة ويتم الرجوع إليها عبر الصلاحيات. بالإضافة إلى الذاكرة العامة، يميز بروتوكول seL4 ذاكرة الجهاز غير المُصنفة ، والتي تخضع لقيود إضافية لمنع إعادة التصنيف أو إعادة الاستخدام غير الآمنة. [ 16 ]

الاتصال بين العمليات (IPC)

لا يُقصد بـ seL4 IPC أن يكون آلية عامة لتمرير الرسائل، بل وسيلة لتنفيذ استدعاء الدوال أو الخدمات عبر نطاقات الحماية المختلفة. يُصنّف مصممو seL4 هذا الأسلوب على أنه استدعاء إجراء محمي (PPC)، والذي ينقل فقط قيمًا صغيرة للوسائط والقيم المُعادة (على غرار استدعاء دالة عبر نطاقات الحماية)، وليس وسيلة نقل مؤقتة لبيانات عشوائية. يوصي مصممو seL4 صراحةً بعدم استخدام IPC لنقل كميات كبيرة من البيانات أو للمزامنة، واستخدامه بشكل أساسي لاستدعاء الخدمات ونقل القدرات عبر آلية الطلب والاستجابة . [ 17 ]

تعتمد آلية الاتصال بين العمليات في لغة seL4 على كائنات نواة مُدارة بالصلاحيات، وهي مصممة لتقليل حالة النواة مع توضيح صلاحيات كل عملية. يُعدّ كائن نقطة النهاية هو كائن الاتصال الرئيسي ، والذي يُمثّل كلاً من حق الاتصال ونقطة الالتقاء للاتصال: لا يُمكن لأي عملية إرسال أو استقبال البيانات من نقطة النهاية إلا إذا كانت تمتلك الصلاحية المناسبة. [ 15 ]

يُعدّ الاتصال بين العمليات عبر نقاط النهاية متزامنًا وحجبيًا (مع وجود اصطلاحات أخرى مُطبقة فوقه). تنتظر عملية الإرسال حتى يصبح المُستقبِل جاهزًا، وتنتظر عملية الاستقبال حتى يصل المُرسِل. على عكس العديد من أنظمة تمرير الرسائل التقليدية، لا تُوفّر نقاط نهاية seL4 قوائم انتظار أو صناديق بريد للرسائل تُديرها النواة. تحتفظ النواة فقط بقوائم انتظار للخيوط المُنتظرة، ويتم نقل بيانات الرسائل مباشرةً بين الخيوط المُتصلة باستخدام حمولة صغيرة ذات حجم ثابت. هذا يُجنّب تخصيص ذاكرة النواة الضمني أثناء الاتصال، ويتوافق مع نموذج إدارة الموارد الصريح في seL4. [ 15 ] [ 7 ] قد تتضمن الرسائل كلاً من البيانات والقدرات المُختارة، مما يسمح للاتصال بين العمليات بأن يكون ليس فقط آلية اتصال، بل أيضًا وسيلة لتفويض السلطة بشكل صريح. يُؤدي نقل قدرة أثناء الاتصال بين العمليات إلى نقل حق الوصول إلى كائن النواة مباشرةً، مما يُدمج الاتصال والتحكم في الوصول بشكل مُحكم. [ 15 ]

فصل مستوى التحكم عن مستوى البيانات

على الرغم من أن الاتصال المتزامن بين العمليات (IPC) هو آلية الاتصال الأساسية التي يوفرها نظام التشغيل، إلا أنه ليس مصممًا لنقل كميات كبيرة من البيانات [ 17 ] ، ويتم تقليل استخدامه في الأنظمة القائمة على seL4 على المسارات الحساسة للأداء. عادةً ما تفصل الأنظمة الاتصال إلى مستوى تحكم ومستوى بيانات. يُستخدم الاتصال بين العمليات (IPC) بشكل أساسي لعمليات التحكم مثل التهيئة، وتفاعلات الطلب والاستجابة، ونقل القدرات، بينما يتم تنفيذ تبادل البيانات بكميات كبيرة أو بتردد عالٍ في مساحة المستخدم باستخدام الذاكرة المشتركة مع الإشعارات غير المتزامنة. [ 15 ] [ 18 ]

تُنشأ مناطق الذاكرة المشتركة صراحةً من ذاكرة غير مُحددة النوع وتُربط بمساحات عناوين متعددة، وتُستخدم الإشعارات للإشارة إلى توفر البيانات أو اكتمال العمل. يُمكّن هذا النمط من تنفيذ هياكل بيانات خالية من الأقفال أو الانتظار، مثل المخازن الحلقية، دون إشراك النواة في مسار البيانات. من خلال إبقاء النواة خارج نقل البيانات المجمعة، تُقلل أنظمة seL4 من عبء النسخ، وتتجنب الحظر غير الضروري، وتحافظ على البساطة المطلوبة للتحقق الرسمي. يُشجع هذا النهج التصميمي من قِبل أُطر عمل عالية المستوى في بيئة seL4، بما في ذلك CAmkES، وإطار عمل برنامج تشغيل أجهزة seL4 (sDDF)، ومجموعة أدوات seL4 المصغرة. [ 19 ] [ 20 ]

مقارنة مع نماذج IPC الأخرى

  • قوائم انتظار رسائل POSIX : تُتيح قوائم انتظار رسائل POSIX قوائم انتظار مُسماة مُدمجة في نواة النظام، تدعم تمرير الرسائل غير المتزامن. وتعتمد هذه القوائم على تخصيص ضمني لذاكرة النواة ومساحة أسماء عامة، وتفصل تمرير الرسائل عن آليات التحكم في الوصول. في المقابل، لا يحتوي بروتوكول seL4 على مساحة أسماء عامة للاتصال بين العمليات (IPC) ولا قوائم انتظار رسائل تُدار بواسطة النواة؛ إذ يتطلب كل اتصال امتلاك إمكانية نقطة نهاية صريحة، ويتم تطبيق سياسات التخزين المؤقت في مساحة المستخدم عند الحاجة. [ 21 ] [ 22 ]
  • منافذ Mach : تجمع منافذ Mach بين التسمية والصلاحية للاتصال بين العمليات، وترتبط عادةً بقوائم انتظار الرسائل التي يديرها النواة والاتصال المخزن مؤقتًا غير المتزامن. في المقابل، تتجنب نقاط نهاية seL4 تخزين رسائل النواة مؤقتًا، وتوفر بدلاً من ذلك دلالات الالتقاء المتزامن، مما يقلل من تعقيد النواة واستخدام الموارد الخفي مقارنةً بآليات الاتصال بين العمليات الأكثر مرونة ولكن الأبطأ في Mach. [ 23 ]
  • نموذج الاتصال بين العمليات في الطبقة الرابعة (L4 IPC) : ينحدر نموذج الاتصال بين العمليات في seL4 مباشرةً من نماذج النواة المصغرة السابقة للطبقة الرابعة، والتي ركزت بدورها على تبادل الرسائل المتزامن عالي الأداء. يحتفظ seL4 بدلالات الاتصال بين العمليات على غرار آلية الالتقاء، ولكنه يفصل تبادل الرسائل عن التزامن. يُمكّن هذا من تحسين تبادل الرسائل لأنظمة PPC (استدعاءات الخادم) ودمجها بشكل أوثق مع نظام صلاحيات رسمي وتصميم نواة مُدقّق، مما يجعل نقل الصلاحيات واضحًا وقابلًا للاستدلال الرسمي. [ 1 ]

الإشعارات والإشارة إلى الأحداث

بالإضافة إلى نقاط النهاية، يوفر seL4 كائنات الإشعارات : كائنات شبيهة بالإشارات الثنائية للإشارة إلى الأحداث غير المتزامنة والمزامنة الخفيفة. تُستخدم الإشعارات عادةً لإيصال أحداث مقاطعة الأجهزة إلى برامج تشغيل الأجهزة في مساحة المستخدم أو للإشارة إلى تغييرات الحالة بين المكونات، مما يدعم بنية النواة المصغرة التي يتم فيها تنفيذ معالجة المقاطعات وبرامج التشغيل خارج النواة. [ 15 ]

التحقق الرسمي

يستخدم نظام seL4 مواصفات مكتوبة كنماذج رياضية بلغة Isabelle/HOL لوصف التشغيل الصحيح لاستدعاءات النظام. ثم تُربط هذه المواصفات بتنفيذ C لإثبات صحتها الوظيفية : حيث تُنفذ جميع استدعاءات النظام العمليات الصحيحة وتُعيد النتائج الصحيحة (بدون أخطاء منطقية، ولن تتعطل، ولن تتوقف عن العمل، إلخ ). [ 7 ] ينتج عن ذلك درجة عالية جدًا من الضمان [ 24 ] بأن نظام قدرات النواة يُطبق خصائص أمن المعلومات الأساسية CIA للعمليات: سرية المعلومات بين العمليات، وسلامة حالة النواة وتدفق التحكم، والتوافر من خلال منع هجمات حجب الخدمة عن استخدام الموارد المصرح به. [ 3 ]

يُعدّ هذا المنتج، الذي يبلغ حجمه حوالي 10 آلاف سطر من التعليمات البرمجية و500 ألف سطر من العمليات، أحد أكبر منتجات التحقق التي طُوّرت على الإطلاق، [ 25 ] وقد أُدرجت الورقة البحثية الأصلية الخاصة به في قاعة مشاهير ACM SIGOPS عام 2019. [ 4 ] إلا أن عبء إثبات 50 سطرًا لكل سطر من التعليمات البرمجية بلغة C يزيد بشكل كبير من تكلفة التطوير ويُبطئ وتيرته، مما يُصعّب إجراء التغييرات. [ 25 ] ومع ذلك، يدّعي مؤلفوه أن التكلفة، البالغة 400 دولار أمريكي لكل سطر من التعليمات البرمجية، كانت أقل من 1000 دولار أمريكي لكل سطر من التعليمات البرمجية للنوى المماثلة عالية الموثوقية (ولكن غير المُتحقق منها)، وضعف سعر النوى المماثلة منخفضة الموثوقية فقط. [ 26 ]

القيود

على غرار الأنظمة الأخرى التي خضعت للتحقق الرسمي، فإن ضمانات seL4 نسبية لمواصفاتها وافتراضاتها الأساسية. ورغم أن هذا يعني أن التحقق لا يعالج جميع الأخطاء المحتملة، إلا أنه يُحسّن بشكل كبير من ضمان النظام ككل من خلال استبعاد فئات عيوب التنفيذ وجعل الافتراضات المتبقية واضحة (وبالتالي قابلة للاختبار). [ 27 ] [ 25 ]

  • يُعدّ seL4 مجرد نواة مصغّرة تُبنى عليها أنظمة تشغيل كاملة . ومع ذلك، تُظهر دراسة حالة لثغرات CVE الحرجة في نواة لينكس أن عزل أنظمتها الفرعية غير المُوثّقة كان سيُقلّل من خطورة كل ثغرة CVE تمّ أخذ عينات منها ولم تكن مرتبطة ببيئة ما قبل الإقلاع. [ 28 ]
  • لا تغطي البراهين جميع جوانب تشغيل حاسوب يعمل بنظام seL4، ولا تشمل جميع المنصات والتكوينات المدعومة. [ 7 ] على سبيل المثال، اقتصرت البراهين الأولية على قاعدة بيانات كود C، ولكن تم توسيع نطاق البراهين لاحقًا ليشمل الملفات الثنائية المُجمَّعة (التحقق من الملفات الثنائية غير مدعوم على جميع المنصات).
  • على الرغم من قدرة seL4 على ربط مواصفاتها بمواصفات الأجهزة ، إلا أنه قد توجد أخطاء في المواصفات أو في الأجهزة نفسها. مع ذلك، لم يتم الإبلاغ علنًا عن أي أخطاء في الأجزاء المُدققة من النواة منذ أكثر من 15 عامًا. [ 29 ] وبينما تؤثر عيوب الأجهزة على جميع أنظمة التشغيل، وتوفر seL4 حلولًا لبعض أخطاء الأجهزة المعروفة، إلا أن المشروع لا يملك حاليًا الموارد الكافية لتنفيذ عدد كبير من هذه الحلول مقارنةً بأنظمة التشغيل التجارية الأكثر تطورًا. [ 30 ] مع ذلك، لا يُعد هذا قيدًا جوهريًا على seL4.

التحقق من الجدول الزمني للميزات / خارطة الطريق (معالم مختارة)

  تم التحقق (إثباتات تم فحصها آلياً لتكوينات محددة)
  اكتملت الميزة (لا يُتوقع أن يؤدي المزيد من التحقق إلى الإخلال بالتوافق)
  في تَقَدم
  البحث جارٍ
مراحل التحقق وخارطة الطريق [ 31 ]
تاريخالمرحلة / النطاقحالةملحوظات
29 يوليو 2009يتوافق إثبات صحة وظائف كود C مع المواصفات المجردة. [ 32 ] [ 7 ]تم التحققمعالج أحادي النواة ولم يمتد إلى النظام الثنائي.
2011–2012تحليل وقت التنفيذ في أسوأ الحالات (WCET) لاستدعاءات نظام نواة seL4 وزمن استجابة المقاطعة لمنصات Arm أحادية النواة محددة. [ 33 ]مستقر (تم تحليله؛ تم استخدام البراهين ذات المستوى الأعلى لاحقًا لتحسين حدود وقت التنفيذ الأسوأ)أُجري أول تحليل من هذا النوع على نظام محمي بالذاكرة . ومنذ ذلك الحين، توقفت شركة Arm عن تحديد أسوأ حالات زمن استجابة التعليمات، ولكن يمكن تطبيق هذا العمل على المنصات المستقبلية. [ 34 ]
2012–حتى الآنإثباتات إنفاذ الأمن (السلامة وسرية تدفق المعلومات) وامتدادات صحة النظام الثنائي [ 32 ] [ 35 ] (تم توسيعها لاحقًا إلى Intel x64 و RISC-V 64) [ 36 ]تم التحقق (يختلف الدعم حسب المنصة)يتحقق من أن الملف الثنائي الناتج عن GCC عند -O2 لا يزال يفرض البراهين عالية المستوى دون التحقق من المُصرّف أو الوثوق به. [ 37 ]
2014–2017تقنيات التحليل عالية الموثوقية (حدود الحلقات، المسارات غير الممكنة، تكامل سلسلة الأدوات) الممتدة من البراهين ذات المستوى الأعلى، مما يُحسّن بشكل أكبر من وقت تنفيذ البرنامج الثنائي في أسوأ حالاته. [ 38 ] [ 34 ] [ 5 ]مستقر (تم تحليله؛ ضمان على مستوى البحث)
19 نوفمبر 2019تم دمج أنظمة الأهمية المختلطة (MCS: سياقات العزل الزمني / الجدولة) في الخط الرئيسي. [ 39 ]مستقر (غير مؤكد)
2019–حتى الآنتم تقييم آليات التوقيت الجانبي / "حماية الوقت"؛ ويجري العمل على صياغتها والتحقق منها. [ 35 ]في تَقَدمسيتطلب ذلك دعمًا للأجهزة.
2024–حتى الآنالمعالجات متعددة النوى: خارطة طريق "النوى المتعددة الثابتة" التي تم التحقق منها وإطار عمل التحقق من التزامن (نهج ضمان تدريجي) [ 40 ]في تَقَدم
الربع الثالث من عام 2027MCS: من المقرر إكمال التحقق من صحة الوظائف على مستوى C. [ 41 ]مخطط له

ملاحظة: تختلف حالة التحقق من seL4 باختلاف البنية والتكوين؛ وتوفر وثائق seL4 مصفوفة توضح الخصائص التي يتم تغطيتها لكل تكوين (مثل صحة الوظائف، والتكامل/التوافر، والسرية، وتغطية صحة الملفات الثنائية). [ 42 ]

النظام البيئي

تُستخدم لغة seL4 بشكل شائع كأساس لنواة أنظمة التشغيل المدمجة المُجزأة، وتدعم مؤسسة seL4 مجموعة من الأدوات والأطر المرتبطة بها. وتُقدم مكونات النظام البيئي (بما في ذلك الشفرة والأدوات والبراهين) عمومًا بموجب تراخيص مفتوحة ( BSD ).

مجموعة أدوات صغيرة

تُعدّ مجموعة أدوات seL4 Microkit إطار عمل لنظام التشغيل مبنيّ على seL4، وهي توفر مجموعة صغيرة من التجريدات التي تهدف إلى تبسيط بناء الأنظمة ذات البنية الثابتة مع الحفاظ على الأداء وكفاءة استخدام الذاكرة. [ 43 ] [ 44 ]

إطار عمل برامج تشغيل الأجهزة (sDDF)

إطار عمل برنامج تشغيل الأجهزة seL4 (sDDF) هو بنية برنامج تشغيل لأنظمة seL4 تمت مناقشتها في العديد من القمم؛ وتصف مواد القمة تصميمًا يركز على فصل الاهتمامات والاتصال غير المتزامن/القائم على الأحداث مع مسارات بيانات الذاكرة المشتركة. [ 45 ]

LionsOS

بنية نظام مرجعي لنظام LionsOS

يخضع نظام التشغيل LionsOS حاليًا للتطوير من قبل قسم الأنظمة الموثوقة في جامعة نيو ساوث ويلز (UNSW) [ 46 ] ، ويهدف إلى توفير خدمات نظام تشغيل موجهة للتطبيقات، مثل الشبكات وأنظمة الملفات وعمليات الإدخال والإخراج الأخرى. وبينما كان النظام يستهدف في المقام الأول البنى الثابتة التي تُخصص مواردها عند بدء التشغيل (مثل الأنظمة المدمجة)، فإنه من المخطط دعم أنظمة تشغيل أكثر ديناميكية. [ 47 ] [ 48 ]

تتمثل الأهداف الرئيسية لنظام التشغيل LionsOS في منافسة نظام Linux باستخدام نواة seL4 المصغرة التي تحافظ على أداء النظام مع توفير تطبيق صحيح لأجهزة seL4 باستخدام أدوات التحقق من قابلية الإرضاء المعيارية (SMT). [ 49 ] تتكون المكونات الأساسية للنظام المقترح من مجموعة أدوات seL4 المصغرة وإطار عمل برنامج تشغيل أجهزة seL4 (sDDF). تم إصدار النسخة 0.3.0 في 25 مارس 2025. [ 50 ] [ 51 ]

الحوكمة والمجتمع

تتولى مؤسسة seL4 تنسيق جوانب إدارة المشروع وتعزيز بيئة محايدة للبائعين. وقد أُطلقت في البداية تحت مظلة مؤسسة لينكس لدعم تبني تقنية seL4 على نطاق أوسع وإدارتها على المدى الطويل بشكل محايد للبائعين. [ 10 ] [ 11 ] ثم تحولت لاحقًا إلى منظمة مستقلة. [ 52 ] وقد تم اختيار رخصة جنو العمومية (GPL) لتشجيع تبادل الاستثمارات التجارية والحد من التفرع. [ 53 ] وتُعد قمة seL4 السنوية منصة رئيسية لعرض تطورات البيئة، وتوجهات البحث، وتقارير الخبرات، وجلسات موجهة للصناعة بهدف تعزيز الاستثمار التجاري في seL4. [ 54 ]

انظر أيضاً

مراجع

  1. 1 2 3 إلفينستون، كيفن؛ هايزر، جيرنوت (3 نوفمبر 2013). "من L3 إلى seL4: ماذا تعلمنا خلال 20 عامًا من النوى المصغرة L4؟" . وقائع ندوة ACM الرابعة والعشرين حول مبادئ أنظمة التشغيل . SOSP '13. نيويورك، نيويورك، الولايات المتحدة الأمريكية: رابطة آلات الحوسبة. الصفحات 133-150 . doi : 10.1145/2517349.2522720 . ISBN  978-1-4503-2388-8.
  2. ↑ دورنر وركس؛ فان فوسن، روبرت (26 نوفمبر 2019). "مقدمة لبناء أنظمة آمنة باستخدام النواة المصغرة seL4" . دورنر وركس . تم الاسترجاع في 3 فبراير 2026 .
  3. 1 2 موراي، توبي (2013). "seL4: من الأغراض العامة إلى إثبات إنفاذ تدفق المعلومات" (ملف PDF) . ندوة IEEE للأمن والخصوصية لعام 2013. IEEE.
  4. 1 2 "جائزة قاعة المشاهير 2019" . ACM SIGOPS . 29 أكتوبر 2019.
  5. 1 2 "seL4 في أستراليا" . اتصالات ACM . أبريل 2020.
  6. ↑ دي ماتوس، إيفرتون؛ لوتون، جورج؛ لينون، كونور (2025). "نحو seL4 لتحسين عزل النظام وأمنه على الأجهزة المدمجة" . مجلة IEEE المفتوحة لجمعية الحاسبات . 6 : 1329-1340 . Bibcode : 2025OJCmS...6.1329D . doi : 10.1109/OJCS.2025.3592377 . ISSN 2644-1268 . 
  7. 1 2 3 4 5 كلاين، جيروين (2009). "seL4: التحقق الرسمي من نواة نظام التشغيل" (ملف PDF) . وقائع ندوة ACM SIGOPS الثانية والعشرين حول مبادئ أنظمة التشغيل (SOSP '09) . ACM.
  8. ↑ ""نظام التشغيل الأكثر موثوقية في العالم" نواة مفتوحة المصدر . فورونيكس . 29 يوليو 2014.
  9. ↑ "إصدار نظام التشغيل الآمن للغاية seL4 كمصدر مفتوح" . SecurityWeek . 29 يوليو 2014.
  10. 1 2 "نواة seL4 المصغرة المُحسّنة للأمان تحصل على دعم مؤسسة لينكس" . مؤسسة لينكس . 7 أبريل 2020.
  11. 1 2 "مطورو seL4 يُنشئون أساسًا مفتوح المصدر لتمكين أنظمة حوسبة أكثر أمانًا وموثوقية" . CSIRO . 8 أبريل 2020.
  12. ↑ أندرونيك، جون (11 يناير 2022). "التحقق الذاتي: فن ومهارة البرهان وواقع الدعم التجاري (محاضرة مدعوة)" . وقائع المؤتمر الدولي الحادي عشر لجمعية ACM SIGPLAN حول البرامج والبراهين المعتمدة . نيويورك، نيويورك، الولايات المتحدة الأمريكية: ACM. ص 1. doi : 10.1145/3497775.3505265 . ISBN  978-1-4503-9182-5.
  13. ↑ هاسلبيك، ماكسيميليان بي إل "كرسي المنطق والتحقق - التدريس" . www21.in.tum.de . تم الاطلاع عليه في 3 فبراير 2026 .
  14. ↑ سيسي، تونا (3 نوفمبر 2024). "نواة النظام المصغرة seL4: البنية" . ميديوم . تم الاسترجاع في 3 فبراير 2026 .
  15. 1 2 3 4 5 6 7 دليل مرجعي لبرنامج seL4 (ملف PDF) (تقرير). مؤسسة seL4.
  16. ↑ "إدارة الذاكرة" . وثائق seL4 .
  17. 1 2 هايزر، جيرنوت (7 مارس 2019). "كيفية استخدام بروتوكول الاتصال بين العمليات seL4 (وكيفية عدم استخدامه)" . microkerneldude.org .
  18. ↑ "IPC والذاكرة المشتركة" . وثائق seL4 .
  19. ↑ "إطار عمل برنامج تشغيل الأجهزة seL4" . docs.sel4.systems .
  20. ↑ "مجموعة أدوات seL4 المصغرة" . docs.sel4.systems .
  21. ↑ "mq_overview(7) - صفحة دليل لينكس" . linux.die.net . مؤرشف من الأصل في 2 أغسطس 2025. تم الاطلاع عليه في 2 فبراير 2026 .
  22. ↑ كيريسك، مايكل (2010). "5: قوائم انتظار رسائل POSIX". واجهة برمجة لينكس: دليل برمجة أنظمة لينكس ويونكس (ملف PDF) . سان فرانسيسكو: دار نشر نو ستارش. ISBN 978-1-59327-220-3.
  23. ↑ رشيد، ريتشارد (1986). ماخ: أساس جديد لنواة نظام يونكس (ملف PDF) . يو إس إي إن آي إكس.
  24. ↑ "الأساليب الرسمية | داربا" . www.darpa.mil . تم الاطلاع عليه بتاريخ 3 فبراير 2026 .
  25. 1 2 3 فيشر، كاثلين؛ لانشبري، جون؛ ريتشاردز، ريموند (13 أكتوبر 2017). "برنامج HACMS: استخدام الأساليب الرسمية للقضاء على الأخطاء القابلة للاستغلال" . المعاملات الفلسفية. السلسلة أ، العلوم الرياضية والفيزيائية والهندسية . 375 (2104) 20150401. رمز Bibcode : 2017RSPTA.37550401F . doi : 10.1098/rsta.2015.0401 . ISSN 1364-503X . PMC 5597724. PMID 28871050 .   
  26. ↑ هايزر، جيرنوت (2015). "seL4 مجاني! ماذا يعني ذلك بالنسبة لك؟" (ملف PDF) .
  27. ↑ هول، أنتوني (1990). سبع خرافات عن الأساليب الرسمية (PDF) (تقرير).
  28. ↑ نيروب، كارل (6 سبتمبر 2018). "النوى المصغرة تُحسّن الأمان فعلاً - Cog" . تم الاطلاع عليه في 3 فبراير 2026 .
  29. ↑ "إثباتات seL4 | seL4" . sel4.systems . تم الاطلاع عليه في 2 يناير 2026 .
  30. ↑ seL4. "وثيقة تُثبت وجود ثغرات أمنية معروفة في منفذ x86 · المشكلة رقم 1108 · seL4/seL4" . GitHub . تم الاطلاع عليه بتاريخ 23 فبراير 2026 .{{cite web}}: صيانة CS1: الأسماء الرقمية: قائمة المؤلفين ( رابط )
  31. ↑ "خارطة طريق التطوير | seL4" . sel4.systems . تم الاطلاع عليه في 2 يناير 2026 .
  32. 1 2 "التاريخ" . seL4 .
  33. ↑ بلاكهام، برنارد (2011). "تحليل التوقيت لنواة نظام تشغيل محمي" (PDF) . وقائع ندوة أنظمة الوقت الحقيقي IEEE (RTSS) .
  34. 1 2 "WCET: تحليل وقت التنفيذ في أسوأ الحالات لـ seL4" . أنظمة جديرة بالثقة .
  35. 1 2 "مشروع التحقق من seL4" . أنظمة جديرة بالثقة .
  36. ↑ أندرونيك، يونيو (2022)، غريجيو، ألبرتو؛ رونغتا، نيها (محررون)، رحلة التحقق من seL4: كيف تطورت التحديات والفرص ، جامعة فيينا التقنية، جامعة فيينا التقنية، ص 1، Bibcode : 2022fmca.conf....8A ، doi : 10.34727/2022/ISBN.978-3-85448-053-2_1 ، تم الاطلاع عليه في 3 فبراير 2026 
  37. ↑ ميرين، ماغنوس أو. (25 يناير 2018). التحقق من الملف الثنائي المُولّد بواسطة GCC لنواة seL4 المصغرة (ملف PDF) . مؤتمر ENTROPY 2018. كامبريدج، المملكة المتحدة: جامعة تشالمرز للتكنولوجيا . تاريخ الاسترجاع: 2 فبراير 2026 .
  38. ↑ بلاكهام، برنارد (2014). "تحليل التوقيت عالي الموثوقية لنواة الوقت الحقيقي عالية الموثوقية". أنظمة الوقت الحقيقي .
  39. ↑ "الإعلان عن إصدارات جديدة: seL4-11.0.0، camkes-3.8.0، CapDL ..." lists.sel4.systems (HyperKitty) .
  40. ↑ "ملخصات قمة seL4 لعام 2024 - التحقق من seL4: الوضع والخطط" . seL4 .
  41. ↑ "خارطة طريق التطوير" . seL4 .
  42. ↑ "التكوينات المُتحقق منها" . وثائق seL4 .
  43. ↑ "مجموعة أدوات seL4 المصغرة" . docs.sel4.systems .
  44. ↑ "مجموعة أدوات seL4 المصغرة (شرائح)" (ملف PDF) . قمة seL4 2023 .
  45. ↑ "إطار عمل برنامج تشغيل الأجهزة seL4 (sDDF) (شرائح)" (ملف PDF) . قمة seL4 2023 .
  46. ↑ "النواة المصغرة seL4 | TS" . trustworthy.systems . تم الاطلاع عليه في 3 مايو 2026 .
  47. ↑ هايزر، جيرنوت؛ فيليكوفيتش، إيفان؛ تشاب، بيتر؛ جوشي، ألوين؛ غانيش، أنوراغ؛ نغوين، بيل؛ لي، تشينغ؛ دارفيل، كورتني؛ تشو، غوانغتاو (27 مايو 2025). "سريع، آمن، قابل للتكيف: تصميم نظام التشغيل LionsOS، وتنفيذه، وأداؤه". arXiv : 2501.06234 [ cs.OS ].
  48. ↑ "مقدمة" . LionsOS 0.3.0 . تم الاطلاع عليه بتاريخ 2 فبراير 2026 .
  49. ↑ "نظام التشغيل Lions: آمن وسريع وقابل للتكيف" . معهد منصات الحوسبة - مجموعة الأنظمة . تم الاطلاع عليه في 3 مايو 2026 .
  50. ↑ "0.3.0" . LionsOS 0.3.0 . تم الاطلاع عليه بتاريخ 3 مايو 2026 .
  51. ↑ au-ts/lionsos ، أنظمة جديرة بالثقة، 1 مايو 2026 ، تم الاطلاع عليه في 3 مايو 2026
  52. ↑ "مؤسسة seL4 | seL4" . sel4.systems . تم الاطلاع عليه بتاريخ 2 فبراير 2026 .
  53. ↑ "ماذا تعني رخصة seL4؟" . microkerneldude . 9 ديسمبر 2019. تم الاطلاع عليه في 2 فبراير 2026 .
  54. ↑ "قمة seL4 لعام 2025 - حلقة نقاش: بناء دراسة جدوى لاستخدام نواة تم التحقق منها" . seL4.systems .