حصل مشروع النواة الصغيرة seL4 open microkernel على جائزة ACM Software System Award ، وهي جائزة سنوية تمنحها جمعية ماكينات الحوسبة (ACM) ، وهي المنظمة الدولية الأكثر احترامًا في مجال أنظمة الكمبيوتر. تُمنح الجائزة للإنجازات التي تحققت في مجال الإثبات الرياضي للعملية ، مما يشير إلى الامتثال الكامل للمواصفات الواردة بلغة رسمية ويعترف بالاستعداد للاستخدام في التطبيقات ذات المهام الحرجة. أظهر مشروع seL4 أنه ليس من الممكن فقط التحقق رسميًا بشكل كامل من الموثوقية والأمان للمشاريع على مستوى أنظمة التشغيل الصناعية ، ولكن أيضًا لتحقيق ذلك دون التضحية بالأداء والتنوع.
تُمنح جائزة ACM Software System سنويًا للاعتراف بتطوير أنظمة البرمجيات التي كان لها تأثير محدد على الصناعة ، أو تقديم مفاهيم جديدة أو فتح تطبيقات تجارية جديدة. مبلغ الجائزة 35 ألف دولار أمريكي. في السنوات الماضية ، مُنحت جوائز ACM لمشاريع دول مجلس التعاون الخليجي و LLVM ومؤسسيها ريتشارد ستالمان وكريس لاتنر. تشمل المشاريع والتقنيات الأخرى التي تم التعرف عليها UNIX و Java و Apache و Mosaic و WWW و Smalltalk و PostScript و TeX و Tcl / Tk و RPC و Make و DNS و AFS و Eiffel و VMware و Wireshark و Jupyter Notebooks و Berkeley DB و Eclipse.
تتميز بنية النواة الدقيقة seL4 بإزالة أجزاء لإدارة موارد النواة في مساحة المستخدم ولتطبيق نفس وسائل التحكم في الوصول لموارد مثل موارد المستخدم. لا يوفر microkernel أفكارًا تجريدية عالية المستوى خارج الصندوق لإدارة الملفات والعمليات واتصالات الشبكة وما شابه ، بل يوفر فقط الحد الأدنى من الآليات للتحكم في الوصول إلى مساحة العنوان الفعلية والمقاطعات وموارد المعالج. يتم تنفيذ التجريدات والمحركات عالية المستوى للتفاعل مع الأجهزة بشكل منفصل أعلى النواة الدقيقة في شكل مهام على مستوى المستخدم. يتم تنظيم وصول مثل هذه المهام إلى الموارد المتاحة للنواة الدقيقة من خلال تعريف القواعد.
المصدر: opennet.ru