پروژه میکروکرنل باز seL4 جایزه سیستم نرم افزاری ACM را دریافت کرده است، جایزه سالانه ای که توسط انجمن ماشین های محاسباتی (ACM)، معتبرترین سازمان بین المللی در زمینه سیستم های کامپیوتری اعطا می شود. این جایزه برای دستاوردهایی در زمینه اثبات عملیات ریاضی اعطا می شود که نشان دهنده انطباق کامل با مشخصات ارائه شده به زبان رسمی است و آمادگی برای استفاده در برنامه های کاربردی حیاتی را به رسمیت می شناسد. پروژه seL4 نشان داده است که نه تنها می‌توان به طور رسمی قابلیت اطمینان و امنیت پروژه‌ها را در سطح سیستم‌عامل‌های صنعتی تأیید کرد، بلکه می‌توان به این هدف بدون به خطر انداختن عملکرد و تطبیق‌پذیری دست یافت.
جایزه سیستم نرم افزاری ACM سالانه به منظور قدردانی از توسعه سیستم های نرم افزاری که تأثیر تعیین کننده ای بر صنعت داشته اند، معرفی مفاهیم جدید یا باز کردن برنامه های تجاری جدید ارائه می شود. مبلغ جایزه 35 هزار دلار آمریکا است. در سال های گذشته، جوایز ACM به پروژه های GCC و LLVM و بنیانگذاران آنها ریچارد استالمن و کریس لاتنر داده شده است. پروژه ها و فناوری های دیگری که شناخته شده اند عبارتند از UNIX، Java، Apache، Mosaic، WWW، Smalltalk، PostScript، TeX، Tcl/Tk، RPC، Make، DNS، AFS، Eiffel، VMware، Wireshark، Jupyter Notebooks، Berkeley DB و Eclipse.
معماری میکروکرنل seL4 به دلیل حذف قطعات برای مدیریت منابع هسته در فضای کاربر و برای اعمال همان ابزار کنترل دسترسی برای چنین منابعی مانند منابع کاربر قابل توجه است. میکروکرنل انتزاعات سطح بالا خارج از جعبه را برای مدیریت فایل‌ها، فرآیندها، اتصالات شبکه و موارد مشابه ارائه نمی‌کند، در عوض تنها مکانیزم‌های حداقلی را برای کنترل دسترسی به فضای آدرس فیزیکی، وقفه‌ها و منابع پردازنده فراهم می‌کند. انتزاعات و درایورهای سطح بالا برای تعامل با سخت افزار به صورت جداگانه در بالای میکروکرنل در قالب وظایف در سطح کاربر پیاده سازی می شوند. دسترسی چنین وظایفی به منابع موجود در میکروکرنل از طریق تعریف قوانین سازماندهی می شود.
منبع: opennet.ru