عائلة النواة الدقيقة L4

الموسوعة الحرة

L4 هي عائلة من النوى المصغرة من الجيل الثاني ، وتستخدم لتنفيذ مجموعة متنوعة من أنواع أنظمة التشغيل (OS)، على الرغم من أنها في الغالب لأنواع أنظمة التشغيل الشبيهة بنظام Unix والمتوافقة مع واجهة نظام التشغيل المحمولة ( POSIX ).

تم ابتكار النواة المصغرة L4، مثل سابقتها L3 ، على يد عالم الحاسوب الألماني يوشين ليدتكه استجابةً للأداء الضعيف لأنظمة التشغيل السابقة القائمة على النواة المصغرة. كان ليدتكه يعتقد أن النظام المصمم منذ البداية لتحقيق أداء عالٍ، بدلاً من أهداف أخرى، قادر على إنتاج نواة مصغرة ذات فائدة عملية. وقد لفت تطبيقه الأصلي، المكتوب يدويًا بلغة التجميع الخاصة بمعالجات Intel i386، الأنظار عام 1993 لكونه أسرع بعشرين ضعفًا من نظام Mach . [ 2 ] واعتُبر المنشور اللاحق بعد عامين [ 3 ] مؤثرًا للغاية لدرجة أنه فاز بجائزة قاعة مشاهير ACM SIGOPS لعام 2015. ومنذ إطلاقها، جرى تطوير L4 لتكون متعددة المنصات ولتحسين الأمان والعزل والمتانة .

شهدت واجهة التطبيق الثنائية (ABI) الأصلية لنواة L4 ، وما تلاها من إصدارات، العديد من عمليات إعادة التنفيذ، بما في ذلك L4Ka::Pistachio (التي نفذها ليدتك وطلابه في معهد كارلسروه للتكنولوجيا )، و L4/MIPS ( جامعة نيو ساوث ويلز )، و Fiasco ( جامعة دريسدن للتكنولوجيا ). ولهذا السبب، أصبح مصطلح L4 أكثر شمولاً، ولم يعد يقتصر على تنفيذ ليدتك الأصلي، بل يشمل الآن عائلة النوى المصغرة بأكملها، بما في ذلك واجهة نواة L4 وإصداراتها المختلفة.

تُستخدم الطبقة الرابعة (L4) على نطاق واسع. وقد تم شحن أحد إصداراتها، OKL4 من مختبرات Open Kernel Labs، في مليارات الأجهزة المحمولة. [ 4 ] [ 5 ]

نموذج التصميم

يوضح ليدتك الفكرة العامة للنواة المصغرة قائلاً :

لا يُسمح بمفهوم ما داخل النواة المصغرة إلا إذا كان نقله خارج النواة، أي السماح بتنفيذات منافسة، سيمنع تنفيذ الوظائف المطلوبة للنظام. [ 3 ]

وانطلاقاً من هذا المبدأ، توفر النواة المصغرة L4 بعض الآليات الأساسية: مساحات العناوين (تجريد جداول الصفحات وتوفير حماية الذاكرة)، والخيوط والجدولة ( تجريد التنفيذ وتوفير الحماية الزمنية)، والاتصال بين العمليات (للاتصال المتحكم به عبر حدود العزل).

يُقدّم نظام التشغيل المبني على نواة مصغّرة مثل L4 خدماتٍ كخوادم في مساحة المستخدم ، وهي خدماتٌ تتضمنها داخليًا أنويةٌ متجانسة مثل لينكس أو أنوية مصغّرة من الأجيال السابقة. على سبيل المثال، لتنفيذ نظام آمن شبيه بنظام يونكس ، يجب أن تُوفّر الخوادم إدارة الصلاحيات التي أدرجها Mach داخل النواة.

تاريخ

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

أظهر تحليلٌ مُفصّلٌ لعنق الزجاجة في نظام ماخ، من بين أمور أخرى، أن مجموعة العمل فيه كبيرةٌ جدًا: إذ يُظهر رمز الاتصال بين العمليات ضعفًا في التوطين المكاني؛ أي أنه يُؤدي إلى عددٍ كبيرٍ جدًا من حالات عدم العثور على البيانات في ذاكرة التخزين المؤقت ، ومعظمها داخل النواة. [ 3 ] وقد أدى هذا التحليل إلى ظهور مبدأ مفاده أن النواة المصغّرة الفعّالة يجب أن تكون صغيرةً بما يكفي بحيث تتناسب غالبية التعليمات البرمجية ذات الأهمية البالغة للأداء مع ذاكرة التخزين المؤقت (من المستوى الأول) (ويُفضّل أن تكون جزءًا صغيرًا منها).

المستوى 3

سعى يوشين ليدتكه إلى إثبات أن طبقة اتصال بين العمليات (IPC) مصممة بشكل جيد وأقل سمكًا، مع إيلاء اهتمام دقيق للأداء والتصميم الخاص بكل جهاز (على عكس البرامج متعددة المنصات )، يمكن أن تُحقق تحسينات كبيرة في الأداء الفعلي. فبدلاً من نظام IPC المعقد الذي ابتكره ماخ، كانت نواة L3 المصغرة الخاصة به تُمرر الرسالة ببساطة دون أي تكلفة إضافية. واعتُبر تحديد وتنفيذ سياسات الأمان المطلوبة من مهام خوادم مساحة المستخدم . واقتصر دور النواة على توفير الآلية اللازمة لتمكين خوادم مستوى المستخدم من تطبيق هذه السياسات. وقد أثبتت L3، التي طُوّرت عام 1988، أنها نظام تشغيل آمن وقوي ، واستُخدمت لسنوات عديدة، على سبيل المثال من قِبل جمعية التفتيش الفني (Technischer Überwachungsverein ).

شجرة عائلة L4 (تشير الأسهم السوداء إلى وراثة الكود، وتشير الأسهم الخضراء إلى وراثة ABI)

المستوى 4

بعد اكتساب بعض الخبرة في استخدام طبقة L3، توصل ليدتكه إلى استنتاج مفاده أن العديد من مفاهيم ماخ الأخرى كانت في غير محلها. ومن خلال تبسيط مفاهيم النواة المصغرة بشكل أكبر، طور أول نواة L4، المصممة أساسًا لتحقيق أداء عالٍ. ولتحقيق أقصى قدر من الأداء، كُتبت النواة بالكامل بلغة التجميع ، وكان معدل تنفيذ التعليمات لكل دورة (IPC) فيها أسرع بعشرين مرة من ماخ. [ 2 ] تُعد هذه الزيادات الهائلة في الأداء حدثًا نادرًا في أنظمة التشغيل، وقد حفز عمل ليدتكه تطبيقات جديدة لطبقة L4، وأبحاثًا على أنظمة قائمة على هذه الطبقة في عدد من الجامعات ومعاهد البحوث، بما في ذلك شركة IBM ، حيث بدأ ليدتكه العمل عام 1996، وجامعة دريسدن التقنية، وجامعة نيو ساوث ويلز. وفي مركز توماس ج. واتسون للأبحاث التابع لشركة IBM ، واصل ليدتكه وزملاؤه أبحاثهم حول طبقة L4 والأنظمة القائمة على النواة المصغرة بشكل عام، وخاصة نظام التشغيل Sawmill. [ 6 ]

L4Ka::Hazelnut

في عام ١٩٩٩، تولى ليدتكه قيادة مجموعة هندسة النظم في جامعة كارلسروه ، حيث واصل أبحاثه في أنظمة النواة المصغرة. ولإثبات إمكانية بناء نواة مصغرة عالية الأداء باستخدام لغة برمجة عالية المستوى، طورت المجموعة L4Ka::Hazelnut ، وهي نسخة من النواة مكتوبة بلغة C++ تعمل على أجهزة IA-32 و ARM . وقد تكللت الجهود بالنجاح، إذ ظل الأداء مقبولاً، ومع إصدارها، توقف تطوير نسخ النواة المكتوبة بلغة التجميع فقط.

L4/فشل

بالتوازي مع تطوير L4Ka::Hazelnut، بدأ فريق أنظمة التشغيل TUD:OS التابع لجامعة دريسدن التقنية في عام 1998 بتطوير تطبيقهم الخاص بلغة C++ لواجهة نواة L4، والذي أطلقوا عليه اسم L4/Fiasco. وعلى عكس L4Ka::Hazelnut، الذي لا يسمح بالتزامن في النواة، وخليفته L4Ka::Pistachio، الذي يسمح بالمقاطعات في النواة فقط عند نقاط استباق محددة، كان L4/Fiasco قابلاً للاستباق بشكل كامل (باستثناء العمليات الذرية القصيرة للغاية) لتحقيق زمن استجابة منخفض للمقاطعات . وقد اعتُبر هذا ضروريًا لأن L4/Fiasco يُستخدم كأساس لنظام DROPS [ 7 ] ، وهو نظام تشغيل قادر على الحوسبة في الوقت الحقيقي الصارم ، والذي طُوّر أيضًا في جامعة دريسدن التقنية. ومع ذلك، فإن تعقيدات التصميم القابل للمقاطعة بالكامل دفعت الإصدارات اللاحقة من Fiasco إلى العودة إلى نهج L4 التقليدي لتشغيل النواة مع تعطيل المقاطعات، باستثناء عدد محدود من نقاط المقاطعة.

متعدد المنصات

L4Ka::Pistachio

حتى إصدار L4Ka::Pistachio والإصدارات الأحدث من Fiasco، كانت جميع النوى المصغرة من الطبقة الرابعة (L4) مرتبطة ارتباطًا وثيقًا ببنية وحدة المعالجة المركزية الأساسية. تمثل التحول الكبير التالي في تطوير L4 في استحداث واجهة برمجة تطبيقات ( API ) متعددة المنصات (مستقلة عن المنصة) حافظت على خصائص الأداء العالي رغم مستوى قابليتها العالية للنقل. على الرغم من أن المفاهيم الأساسية للنواة ظلت كما هي، إلا أن واجهة برمجة التطبيقات الجديدة قدمت العديد من التغييرات الهامة مقارنةً بإصدارات L4 السابقة، بما في ذلك دعم أفضل لأنظمة المعالجات المتعددة، وروابط أقل ترابطًا بين الخيوط ومساحات العناوين، وإدخال كتل التحكم في الخيوط على مستوى المستخدم (UTCBs) والسجلات الافتراضية. بعد إصدار واجهة برمجة تطبيقات L4 الجديدة (الإصدار X.2 المعروف أيضًا بالإصدار 4) في أوائل عام 2001، قام فريق هندسة النظم في جامعة كارلسروه بتنفيذ نواة جديدة، L4Ka::Pistachio ، من الصفر تمامًا، مع التركيز الآن على كل من الأداء العالي وقابلية النقل. تم إصدارها بموجب ترخيص BSD ذي البندين . [ 8 ]

إصدارات فياسكو الأحدث

شهدت نواة L4/Fiasco المصغرة تحسينات كبيرة على مر السنين، وهي تدعم الآن العديد من منصات الأجهزة، بدءًا من x86 مرورًا بـ AMD64 وصولًا إلى العديد من منصات ARM. والجدير بالذكر أن إصدارًا من Fiasco (Fiasco-UX) يمكن تشغيله كتطبيق على مستوى المستخدم في نظام Linux.

يُطبّق نظام L4/Fiasco العديد من الإضافات لواجهة برمجة تطبيقات L4v2. تُمكّن خاصية Exception IPC النواة من إرسال استثناءات وحدة المعالجة المركزية إلى تطبيقات معالجة مستوى المستخدم. وبمساعدة الخيوط الخارجية ، يُمكن التحكم بدقة في استدعاءات النظام. كما أُضيفت وحدات التحكم في الاستثناءات الموحدة (UTCBs) بنمط X.2. ويحتوي Fiasco أيضًا على آليات للتحكم في حقوق الاتصال واستخدام موارد مستوى النواة. في Fiasco، طُوّرت مجموعة من خدمات مستوى المستخدم الأساسية (تُسمى L4Env) والتي تُستخدم، من بين أمور أخرى، لمحاكاة نظام Linux الحالي (4.19 اعتبارًا من مايو 2019) افتراضيًا. ) (يسمى L 4 Linux ).

جامعة نيو ساوث ويلز و NICTA

جرى تطوير L4 أيضًا في جامعة نيو ساوث ويلز (UNSW)، حيث قام المطورون بتنفيذها على عدة منصات 64 بت. أسفر عملهم عن L4/MIPS و L4/Alpha ، مما أدى إلى تسمية نسخة ليدتك الأصلية لاحقًا بـ L4/x86 . ومثل نواة ليدتك الأصلية، كانت نواة جامعة نيو ساوث ويلز (المكتوبة بمزيج من لغة التجميع ولغة C) غير قابلة للنقل، وقد تم تنفيذ كل منها من الصفر. مع إصدار L4Ka::Pistachio، وهي نواة قابلة للنقل بدرجة عالية، تخلت مجموعة جامعة نيو ساوث ويلز عن نواة الخاصة بها لصالح إنتاج نسخ مُحسّنة للغاية من L4Ka::Pistachio، بما في ذلك أسرع تنفيذ مُسجّل على الإطلاق لتمرير الرسائل (36 دورة على معمارية إيتانيوم ). [ 9 ] وقد أثبت الفريق أيضًا أن برامج تشغيل الأجهزة يمكن أن تعمل بكفاءة مماثلة على مستوى المستخدم كما في نواة النظام، [ 10 ] وطوّروا Wombat ، وهي نسخة محمولة للغاية من Linux على الطبقة الرابعة (L4) تعمل على معالجات x86 و ARM و MIPS . على معالجات XScale ، تكون تكاليف تبديل السياق في Wombat أقل بما يصل إلى 50 مرة من تكاليفها في Linux الأصلي. [ 11 ]

لاحقًا، قام فريق جامعة نيو ساوث ويلز، الذي يعمل الآن في NICTA (المعروفة سابقًا باسم National ICT Australia, Ltd. )، بتطوير نسخة جديدة من L4 باسم NICTA::L4-embedded، مستوحاة من L4Ka::Pistachio . كان الهدف من هذه النسخة استخدامها في الأنظمة المدمجة التجارية ، ولذلك ركزت المفاضلات التنفيذية على تقليل حجم الذاكرة وخفض التعقيد. تم تعديل واجهة برمجة التطبيقات (API) للحفاظ على قصر معظم استدعاءات النظام بحيث لا تحتاج إلى نقاط مقاطعة، وذلك لضمان استجابة عالية في الوقت الفعلي. [ 12 ]

النشر التجاري

في نوفمبر 2005، أعلنت الهيئة الوطنية لتكنولوجيا المعلومات والاتصالات (NICTA) [ 13 ] أن شركة كوالكوم بدأت بنشر نسخة الطبقة الرابعة (L4) الخاصة بها على شرائح مودم محطات الهاتف المحمول . أدى ذلك إلى استخدام الطبقة الرابعة في الهواتف المحمولة التي طُرحت للبيع منذ أواخر عام 2006. في أغسطس 2006، أسس جيرنوت هايزر ، قائد مشروع ERTOS وأستاذ جامعة نيو ساوث ويلز، شركةً باسم Open Kernel Labs (OK Labs) لدعم مستخدمي الطبقة الرابعة تجاريًا ومواصلة تطويرها للاستخدام التجاري تحت العلامة التجارية OKL4 ، بالتعاون الوثيق مع الهيئة الوطنية لتكنولوجيا المعلومات والاتصالات. كانت نسخة OKL4 μKernel 2.1، التي صدرت في أبريل 2008، أول نسخة متاحة للعموم من الطبقة الرابعة تتميز بأمان قائم على القدرات . أما نسخة OKL4 μKernel 3.0، التي صدرت في أكتوبر 2008، فكانت آخر نسخة مفتوحة المصدر من OKL4 μKernel. الإصدارات الأحدث مغلقة المصدر وتعتمد على إعادة كتابة لدعم نسخة مُعدّلة من برنامج إدارة الأجهزة الافتراضية تُسمى OKL4 Microvisor . كما وزّعت شركة OK Labs نظام لينكس شبه افتراضي يُسمى OK:Linux، وهو مُشتق من Wombat، بالإضافة إلى إصدارات شبه افتراضية من SymbianOS و Android . واستحوذت OK Labs أيضًا على حقوق seL4 من NICTA.

تجاوزت شحنات OKL4 مليار ونصف المليار وحدة في أوائل عام 2012، [ 5 ] معظمها على رقائق مودم كوالكوم اللاسلكية. وتشمل التطبيقات الأخرى أنظمة المعلومات والترفيه في السيارات . [ 14 ]

تحتوي معالجات سلسلة A من Apple، بدءًا من A7، على معالج مساعد Secure Enclave يعمل بنظام تشغيل من الطبقة الرابعة [ 15 ] يُسمى sepOS (نظام تشغيل معالج Secure Enclave)، وهو مبني على نواة L4 المدمجة التي طُوّرت في NICTA عام 2006. [ 16 ] ونتيجةً لذلك، يُزوّد ​​نظام L4 جميع أجهزة Apple الحديثة، بما في ذلك أجهزة Mac المزودة بمعالجات Apple Silicon . وفي عام 2015 وحده، قُدّر إجمالي شحنات iPhone بنحو 310 ملايين جهاز. [ 17 ]

ضمان عالي: seL4

في عام ٢٠٠٦، شرعت مجموعة NICTA في تصميم نواة مصغرة من الجيل الثالث ، أُطلق عليها اسم seL4، بهدف توفير أساس لأنظمة عالية الأمان والموثوقية، تفي بمتطلبات الأمان مثل معايير Common Criteria وما بعدها. ومنذ البداية، استهدف التطوير التحقق الرسمي من النواة. ولتسهيل تلبية متطلبات الأداء والتحقق، التي قد تتعارض أحيانًا، استخدم الفريق عملية برمجية وسيطة تبدأ من مواصفات قابلة للتنفيذ مكتوبة بلغة Haskell . [ ١٨ ] تستخدم seL4 نظام تحكم في الوصول الأمني ​​قائم على القدرات لتمكين الاستدلال الرسمي حول إمكانية الوصول إلى الكائنات.

أُنجز برهان رسمي على صحة وظائف النظام في عام ٢٠٠٩. [ ١٩ ] يضمن هذا البرهان صحة تنفيذ النواة وفقًا لمواصفاتها، ويشير إلى خلوها من أخطاء التنفيذ مثل حالات التعطل التام ، وحالات التعطل المستمر ، وتجاوزات سعة المخزن المؤقت ، والاستثناءات الحسابية، أو استخدام متغيرات غير مهيأة . يُزعم أن seL4 هي أول نواة نظام تشغيل للأغراض العامة يتم التحقق منها. [ ١٩ ] وقد فاز العمل على seL4 بجائزة قاعة مشاهير ACM SIGOPS لعام ٢٠١٩.

يتبنى نظام seL4 نهجًا مبتكرًا لإدارة موارد النواة، [ 20 ] حيث ينقل إدارة موارد النواة إلى مستوى المستخدم ويخضعها لنفس نظام التحكم في الوصول القائم على الصلاحيات المطبق على موارد المستخدم. هذا النموذج، الذي تبناه أيضًا نظام Barrelfish ، يُبسط عملية فهم خصائص العزل، وكان عاملًا مساعدًا لإثباتات لاحقة تُؤكد أن seL4 يُطبق خصائص الأمان الأساسية المتمثلة في النزاهة والسرية. [ 21 ] كما أثبت فريق NICTA صحة الترجمة من لغة البرمجة C إلى رمز الآلة القابل للتنفيذ ، مما أدى إلى إخراج المُترجم من قاعدة الحوسبة الموثوقة لنظام seL4. [ 22 ] وهذا يعني أن إثباتات الأمان عالية المستوى تنطبق على ملف النواة القابل للتنفيذ. يُعد seL4 أيضًا أول نواة نظام تشغيل منشورة تعمل في الوضع المحمي مع تحليل كامل ودقيق لوقت التنفيذ في أسوأ الحالات (WCET)، وهو شرط أساسي لاستخدامها في الحوسبة في الوقت الحقيقي الصارم . [ 21 ]

في 29 يوليو 2014، أعلنت كل من NICTA وشركة General Dynamics C4 Systems عن إطلاق برنامج seL4، مع إثباتات شاملة، بموجب تراخيص مفتوحة المصدر . [ 23 ] يخضع كود مصدر النواة والإثباتات لترخيص GNU العام الإصدار 2 (GPLv2)، بينما تخضع معظم المكتبات والأدوات لترخيص BSD ذي البندين . في أبريل 2020، أُعلن عن إنشاء مؤسسة seL4 تحت مظلة مؤسسة Linux لتسريع تطوير ونشر برنامج seL4. [ 24 ]

يذكر الباحثون أن تكلفة التحقق الرسمي من البرمجيات أقل من تكلفة هندسة البرمجيات التقليدية "عالية الموثوقية"، على الرغم من أنها توفر نتائج أكثر موثوقية. [ 25 ] وعلى وجه التحديد، قُدّرت تكلفة سطر واحد من التعليمات البرمجية أثناء تطوير seL4 بحوالي 400 دولار أمريكي ، مقارنةً بـ 1000 دولار أمريكي للأنظمة التقليدية عالية الموثوقية. [ 26 ]

في إطار برنامج أنظمة الأمن السيبراني العسكرية عالية الموثوقية (HACMS) التابع لوكالة مشاريع البحوث الدفاعية المتقدمة ( DARPA )، طوّر المركز الوطني لتكنولوجيا المعلومات والاتصالات (NICTA) بالتعاون مع شركاء المشروع : روكويل كولينز ، وغالوا، وجامعة مينيسوتا، وبوينغ ، طائرة مسيّرة عالية الموثوقية باستخدام برنامج seL4، إلى جانب أدوات وبرامج أخرى لضمان الموثوقية، مع خطة لنقل التكنولوجيا إلى طائرة بوينغ AH-6 بدون طيار ذاتية القيادة، والتي تُطوّرها بوينغ. وقد أُجري العرض النهائي لتقنية HACMS في ستيرلينغ، بولاية فرجينيا، في أبريل 2017. [ 27 ] كما موّلت DARPA العديد من عقود برنامج أبحاث الابتكار للشركات الصغيرة (SBIR) المتعلقة ببرنامج seL4، وذلك ضمن برنامج أطلقه جون لانشبري . وشملت الشركات الصغيرة التي حصلت على تمويل من برنامج SBIR المتعلق ببرنامج seL4: دورنر وركس، وتيكشوت، وويرابل، وريل تايم إنوفيشنز، وكريتيكال تكنولوجيز. [ 28 ]

في أكتوبر 2023، أعلنت شركة Nio Inc. أن أنظمة التشغيل SkyOS القائمة على seL4 ستكون موجودة في السيارات الكهربائية المنتجة بكميات كبيرة اعتبارًا من عام 2024. [ 29 ]

في عام 2023، فاز برنامج seL4 بجائزة ACM لأنظمة البرمجيات .

أبحاث وتطوير أخرى

استهدف نظام التشغيل Osker، المكتوب بلغة Haskell ، مواصفات الطبقة الرابعة (L4)؛ على الرغم من أن هذا المشروع ركز بشكل أساسي على استخدام لغة برمجة وظيفية لتطوير أنظمة التشغيل، وليس على أبحاث النواة المصغرة. [ 30 ]

RedoxOS [ 31 ] هو نظام تشغيل قائم على لغة Rust، وهو مستوحى أيضًا من seL4، ويستخدم تصميم النواة المصغرة.

CodeZero [ 32 ] عبارة عن نواة مصغرة من الطبقة الرابعة (L4) للأنظمة المدمجة، تركز على المحاكاة الافتراضية وتنفيذ خدمات نظام التشغيل الأصلية. يوجد إصدار مرخص بموجب رخصة جنو العمومية (GPL) [ 33 ] ، وإصدار آخر أعادت شركة B Labs Ltd. ترخيصه، واستحوذت عليه شركة Nvidia ، كمصدر مغلق، وتم تطوير نسخة منه في عام 2010 [ 34 ] [ 35 ].

F9 microkernel، [ 36 ] وهو تطبيق L4 مرخص بموجب BSD، مخصص لمعالجات ARM Cortex-M للأجهزة المدمجة بعمق مع حماية الذاكرة.

يُعدّ نظام التشغيل NOVA OS Virtualization Architecture [ 37 ] مشروعًا بحثيًا يركز على بناء بيئة افتراضية آمنة وفعّالة [ 38 ] [ 39 ] مع قاعدة حوسبة موثوقة صغيرة. يتكون NOVA من مُشرف افتراضي مصغر، ومُشرف افتراضي على مستوى المستخدم ( مراقب الآلة الافتراضية )، وبيئة مستخدم متعددة الخوادم مُجزأة وغير مُميزة تعمل عليه تُسمى NUL. يعمل NOVA على أنظمة ARMv8-A وأنظمة x86 متعددة النوى.

نظام التشغيل WrmOS [ 40 ] هو نظام تشغيل في الوقت الحقيقي مبني على نواة L4 المصغرة. يحتوي على تطبيقات خاصة به للنواة والمكتبات القياسية ومكدس الشبكة، ويدعم معمارية ARM وSPARC وx86 وx86-64. كما يتضمن نواة لينكس شبه افتراضية (w4linux [ 41 ] ) تعمل على WrmOS.

هيليوس عبارة عن نواة مصغرة مستوحاة من seL4. [ 42 ] وهي جزء من نظام التشغيل Ares، وتدعم x86-64 و aarch64، ولا تزال قيد التطوير النشط حتى فبراير 2023. [ 43 ]

انظر أيضاً

مراجع

  1. ^ "كيرنكونزبت/إخفاق تام" . جيثب .
  2. 1 2 ليدتك، يوشين (ديسمبر 1993). "تحسين أداء الاتصال بين العمليات من خلال تصميم النواة" . الندوة الرابعة عشرة لجمعية الحوسبة الآلية حول مبادئ أنظمة التشغيل . آشفيل، كارولاينا الشمالية، الولايات المتحدة الأمريكية. الصفحات 175-188 . 
  3. 1 2 3 ليدتك، يوشين (ديسمبر 1995). "حول بناء النواة μ" . وقائع الندوة الخامسة عشرة لجمعية ACM حول مبادئ أنظمة التشغيل (SOSP) . الصفحات 237-250 . مؤرشف من الأصل في 25 أكتوبر 2015. 
  4. ↑ "منتجات برنامج إدارة الأنظمة: أنظمة مهام جنرال دايناميكس" . أنظمة مهام جنرال دايناميكس . مؤرشف من الأصل بتاريخ 15 نوفمبر 2017. تم الاطلاع عليه بتاريخ 26 أبريل 2018 .
  5. ١ ٢ "تجاوزت برمجيات Open Kernel Labs حاجز شحن ١.٥ مليار جهاز محمول" (بيان صحفي). Open Kernel Labs. ١٩ يناير ٢٠١٢. مؤرشف من الأصل في ١١ فبراير ٢٠١٢.
  6. ^ جيفلوت، آلان. جايجر، ترينت؛ بارك، يونهو؛ الأماكن القريبة : إلفينستون، كيفن؛ أوليج، فولكمار؛ تيدزويل، جوناثان. ديلر، لوك؛ رويثر، لارس (2000). "نهج الخوادم المتعددة للمنشرة" . ورشة عمل ACM SIGOPS الأوروبية . كولدينج، الدنمارك. ص 109 – 114. 
  7. ↑ "نظرة عامة على برنامج DROPS" . جامعة دريسدن للتكنولوجيا . مؤرشف من الأصل بتاريخ 7 أغسطس 2011. تم الاطلاع عليه بتاريخ 10 أغسطس 2011 .
  8. ↑ l4ka.org: L4Ka::Pistachio microkernel اقتباس: "...إن تنوع البنى المدعومة يجعل L4Ka::Pistachio منصة مثالية للبحث والتطوير لمجموعة واسعة من الأنظمة..."
  9. ↑ غراي، تشارلز؛ تشابمان، ماثيو؛ تشاب، بيتر؛ موسبرغر-تانغ، ديفيد؛ هايزر، غيرنوت (أبريل 2005). "إيتانيوم: قصة مُنفِّذ نظام" . المؤتمر التقني السنوي لـ USENIX . أناهايم، كاليفورنيا، الولايات المتحدة الأمريكية. الصفحات 264-278 . مؤرشف من الأصل في 17 فبراير 2007. 
  10. ↑ ليزلي، بن؛ تشاب، بيتر؛ فيتزروي-ديل، نيكولاس؛ غوتز، ستيفان؛ غراي، تشارلز؛ ماكفيرسون، لوك؛ بوتس، دانيال؛ شين، يويتينغ؛ إلفينستون، كيفن؛ هايزر، غيرنوت (سبتمبر 2005). "برامج تشغيل الأجهزة على مستوى المستخدم: الأداء المُحقق". مجلة علوم وتكنولوجيا الحاسوب . 20 (5): 654-664 . CiteSeerX 10.1.1.59.6766 . doi : 10.1007/s11390-005-0654-4 . S2CID 1121537 .  
  11. ↑ فان شايك، كارل؛ هايزر، غيرنوت (يناير 2007). "النوى المصغرة عالية الأداء والافتراضية على معمارية ARM والمعمارية المجزأة" . ورشة العمل الدولية الأولى حول النوى المصغرة للأنظمة المدمجة . سيدني، أستراليا: NICTA . الصفحات 11-21 . مؤرشف من الأصل في 1 مارس 2015. تم الاطلاع عليه في 25 أكتوبر 2015 . 
  12. ↑ روكو، سيرجيو (أكتوبر 2008). "جولة لمبرمج الوقت الحقيقي في النوى المصغرة للأغراض العامة من الطبقة الرابعة". مجلة EURASIP للأنظمة المدمجة . 2008 : 1-14 . doi : 10.1155/2008/234710 (غير نشط في 12 يوليو 2025). S2CID 7430332 . {{cite journal}}: صيانة CS1: تم تعطيل DOI اعتبارًا من يوليو 2025 ( رابط )
  13. ↑ «سيتم استخدام النواة المصغرة من الطبقة الرابعة (L4) التابعة لهيئة الاتصالات وتقنية المعلومات (NICTA) في حلول مختارة من شرائح كوالكوم» (بيان صحفي). هيئة الاتصالات وتقنية المعلومات (NICTA ). 24 نوفمبر 2005. مؤرشف من الأصل في 25 أغسطس 2006.
  14. ↑ «شركة بوش تختار تقنية المحاكاة الافتراضية للسيارات من Open Kernel Labs لأنظمة المعلومات والترفيه» (بيان صحفي). Open Kernel Labs. 27 مارس 2012. مؤرشف من الأصل في 2 يوليو 2012.
  15. ↑ "أمان نظام التشغيل iOS، الإصدار 12.3" (ملف PDF) . شركة آبل، مايو 2019. مؤرشف (ملف PDF) من النسخة الأصلية بتاريخ 24 يونيو 2020.
  16. ^ مانت، تارجي. سولنيك، ماثيو. وانغ ، ديفيد (2016-07-31). "إزالة الغموض عن معالج المنطقة الآمنة" (PDF) . بلاك هات الولايات المتحدة الأمريكية . لاس فيغاس، نيفادا، الولايات المتحدة الأمريكية. أرشفة (PDF) من الأصلي في 21 أكتوبر 2016.
  17. ↑ إلمر-ديويت، فيليب (28 أكتوبر 2014). "توقعات: ستشحن آبل 310 ملايين جهاز يعمل بنظام iOS في عام 2015" . مجلة فورتشن . مؤرشف من الأصل في 27 سبتمبر 2015. تم الاطلاع عليه في 25 أكتوبر 2015 .
  18. ↑ ديرين، فيليب؛ إلفينستون، كيفن؛ كلاين، جيروين؛ كوك، ديفيد؛ تشاكرافارتي، مانويل إم تي (سبتمبر 2006). "تشغيل الدليل: منهج لتطوير النواة المصغرة عالية الموثوقية" . ورشة عمل ACM SIGPLAN Haskell . بورتلاند، أوريغون . الصفحات 60-71 . 
  19. 1 2 كلاين، جيروين؛ إلفينستون، كيفن؛ هايزر، جيرنوت ؛ أندرونيك، جون؛ كوك، ديفيد؛ ديرين، فيليب؛ إلكادوي، داميكا؛ إنجلهارت، كاي؛ كولانسكي، رافال؛ نورش، مايكل؛ سيويل، توماس؛ توش، هارفي؛ وينوود، سيمون (أكتوبر 2009). "seL4: التحقق الرسمي من نواة نظام التشغيل" (ملف PDF) . المؤتمر الثاني والعشرون لجمعية ACM حول مبادئ أنظمة التشغيل . بيج سكاي، مونتانا، الولايات المتحدة الأمريكية. مؤرشف (ملف PDF) من الأصل في 28 يوليو 2011.
  20. ↑ إلكادوي، داميكا؛ ديرين، فيليب؛ إلفينستون، كيفن (أبريل 2008). تصميم النواة لعزل وضمان الذاكرة الفعلية . ورشة العمل الأولى حول العزل والتكامل في الأنظمة المدمجة. غلاسكو، المملكة المتحدة. doi : 10.1145/1435458 . مؤرشف من الأصل في 22 فبراير 2020. تم الاسترجاع في 22 فبراير 2020 .
  21. 1 2 كلاين، جيروين؛ أندرونيك، جون؛ إلفينستون، كيفن؛ موراي، توبي؛ سيويل، توماس؛ كولانسكي، رافال؛ هايزر، جيرنوت (فبراير 2014). "التحقق الرسمي الشامل من النواة المصغرة لنظام التشغيل". معاملات ACM لأنظمة الحاسوب . 32 (1): 2:1–2:70. CiteSeerX 10.1.1.431.9140 . doi : 10.1145/2560537 . S2CID 4474342 .  
  22. ↑ سيويل، توماس؛ ميرين، ماغنوس؛ كلاين، جيروين (يونيو 2013). "التحقق من صحة الترجمة لنواة نظام تشغيل مُدققة" . مؤتمر ACM SIGPLAN حول تصميم وتنفيذ لغات البرمجة . سياتل، واشنطن، الولايات المتحدة الأمريكية. doi : 10.1145/2491956.2462183 .
  23. ↑ «نظام تشغيل آمن طورته الهيئة الوطنية لتكنولوجيا المعلومات والاتصالات يصبح مفتوح المصدر» (بيان صحفي). الهيئة الوطنية لتكنولوجيا المعلومات والاتصالات . 29 يوليو 2014. مؤرشف من الأصل في 15 مارس 2016.
  24. ↑ «الأمن يحظى بدعم مؤسسة لينكس» (بيان صحفي). مؤسسة لينكس . 7 أبريل 2020. مؤرشف من الأصل بتاريخ 15 مارس 2016.
  25. ↑ كلاين، جيروين؛ أندرونيك، جون؛ إلفينستون، كيفن؛ موراي، توبي؛ سيويل، توماس؛ كولانسكي، رافال؛ هايزر، جيرنوت (2014). "التحقق الرسمي الشامل من النواة المصغرة لنظام التشغيل" ( ملف PDF) . معاملات ACM لأنظمة الحاسوب . 32 : 64. CiteSeerX 10.1.1.431.9140 . doi : 10.1145/2560537 . S2CID 4474342. مؤرشف (ملف PDF) من الأصل في 3 أغسطس 2014.  
  26. ↑ هايزر، جيرنوت (16 يناير 2015). seL4 مجاني: ماذا يعني هذا بالنسبة لك؟ . أوكلاند، نيوزيلندا: Linux.conf.au.
  27. ↑ «وكالة مشاريع الأبحاث الدفاعية المتقدمة (DARPA) تختار شركة روكويل كولينز لتطبيق تكنولوجيا الأمن السيبراني على منصات جديدة» (بيان صحفي). روكويل كولينز . ​​٢٤ أبريل ٢٠١٧. مؤرشف من الأصل في ١١ مايو ٢٠١٧.
  28. ↑ «الدكتور جون لانشبري، الراعي لوكالة داربا» . SBIRSource . 2017. مؤرشف من الأصل في 29 سبتمبر 2017. تم الاطلاع عليه في 16 مايو 2017 .
  29. ↑ "أخبار حول seL4 ومؤسسة seL4" . sel4.systems . تم الاطلاع عليه بتاريخ 20 سبتمبر 2024 .
  30. ↑ هالغريين، ت.؛ جونز، م.ب.؛ ليزلي، ر.؛ تولماش، أ. (2005). "نهج مبدئي لبناء أنظمة التشغيل في لغة هاسكل" (ملف PDF) . نشرة ACM SIGPLAN . 40 (9): 116-128 . doi : 10.1145/1090189.1086380 . ISSN 0362-1340 . مؤرشف (ملف PDF) من الأصل في 15 يونيو 2010. تم الاطلاع عليه في 24 يونيو 2010 . 
  31. ↑ "RedoxOS" . RedoxOS .
  32. ↑ "إعلان: تقديم Codezero" . جامعة دريسدن للتكنولوجيا .
  33. ↑ "jserv/codezero: Codezero Microkernel" . GitHub . مؤرشف من الأصل في 15 أغسطس 2015. تم الاطلاع عليه في 20 أكتوبر 2020 .
  34. ↑ "كود زيرو : نظام التشغيل والمشرف المدمج" . مؤرشف من الأصل بتاريخ 11 يناير 2016. تم الاطلاع عليه بتاريخ 25 يناير 2016 . 
  35. ↑ "مختبرات بي | حلول المحاكاة الافتراضية للأجهزة المحمولة، محاكاة افتراضية لأنظمة أندرويد ولينكس لبنية ARM" . مؤرشف من الأصل في 2 فبراير 2014. تم الاطلاع عليه في 2 فبراير 2014 .
  36. ↑ "F9 Microkernel" . GitHub . تم الاطلاع عليه بتاريخ 20 أكتوبر 2020 .
  37. ↑ "موقع NOVA Microhypervisor الإلكتروني" . تم الاطلاع عليه بتاريخ 9 يناير 2021 .
  38. ↑ شتاينبرغ، أودو؛ كاور، برنارد (أبريل 2010). "نوفا: بنية افتراضية آمنة قائمة على المشرف المصغر". يوروسيس '10: وقائع المؤتمر الأوروبي الخامس لأنظمة الحاسوب . باريس، فرنسا .
  39. ↑ شتاينبرغ، أودو؛ كاور، برنارد (أبريل 2010). "نحو بيئة متعددة المعالجات قابلة للتوسع على مستوى المستخدم". مؤتمر IIDS'10: ورشة عمل حول العزل والتكامل للأنظمة الموثوقة . باريس، فرنسا .
  40. ↑ "WrmOS" . تم الاطلاع عليه بتاريخ 20 أكتوبر 2020 .
  41. ↑ "w4linux هو نواة لينكس شبه افتراضية تعمل على نظام التشغيل WrmOS" . تم الاطلاع عليه بتاريخ 20 أكتوبر 2020 .
  42. ↑ "~sircmpwn/helios – نواة مصغرة تجريبية – مستودع git الخاص بـ sourcehut" . git.sr.ht. تم الاطلاع عليه بتاريخ 20 فبراير 2023 .
  43. ↑ "هيليوس" . ares-os.org . تم الاطلاع عليه بتاريخ 20 فبراير 2023 .

للمزيد من القراءة