Projek mikrokernel terbuka seL4 telah menerima Anugerah Sistem Perisian ACM, anugerah tahunan yang diberikan oleh Association for Computing Machinery (ACM), organisasi antarabangsa yang paling dihormati dalam bidang sistem komputer. Anugerah diberikan untuk pencapaian dalam bidang bukti operasi matematik, yang menunjukkan pematuhan penuh dengan spesifikasi yang diberikan dalam bahasa formal dan mengiktiraf kesediaan untuk digunakan dalam aplikasi kritikal misi. Projek seL4 telah menunjukkan bahawa bukan sahaja mungkin untuk mengesahkan sepenuhnya kebolehpercayaan dan keselamatan untuk projek di peringkat sistem pengendalian industri, tetapi juga untuk mencapainya tanpa mengorbankan prestasi dan serba boleh.
Anugerah Sistem Perisian ACM dipersembahkan setiap tahun untuk mengiktiraf pembangunan sistem perisian yang mempunyai kesan yang jelas terhadap industri, memperkenalkan konsep baharu atau membuka aplikasi komersial baharu. Jumlah anugerah ialah 35 ribu dolar AS. Pada tahun-tahun lepas, anugerah ACM telah diberikan kepada projek GCC dan LLVM, dan pengasasnya Richard Stallman dan Chris Latner. Projek dan teknologi lain yang turut dianugerahkan ialah UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB dan eclipse .
Seni bina mikrokernel seL4 terkenal kerana penyingkiran bahagian untuk menguruskan sumber kernel dalam ruang pengguna dan untuk menggunakan kaedah kawalan capaian yang sama untuk sumber tersebut seperti sumber pengguna. Mikrokernel tidak menyediakan abstraksi peringkat tinggi di luar kotak untuk mengurus fail, proses, sambungan rangkaian dan seumpamanya, sebaliknya ia hanya menyediakan mekanisme minimum untuk mengawal akses kepada ruang alamat fizikal, gangguan dan sumber pemproses. Abstraksi peringkat tinggi dan pemacu untuk berinteraksi dengan perkakasan dilaksanakan secara berasingan di atas mikrokernel dalam bentuk tugas peringkat pengguna. Capaian tugas tersebut kepada sumber yang tersedia untuk mikrokernel diatur melalui definisi peraturan.
Sumber: opennet.ru