Proyek mikrokernel terbuka sel4 telah menerima ACM Software System Award, sebuah penghargaan tahunan yang diberikan oleh Association for Computing Machinery (ACM), organisasi internasional yang paling dihormati di bidang sistem komputer. Penghargaan ini diberikan untuk prestasi di bidang bukti operasi matematis, yang menunjukkan kepatuhan penuh dengan spesifikasi yang diberikan dalam bahasa formal dan mengakui kesiapan untuk digunakan dalam aplikasi kritis. Proyek SEL4 telah menunjukkan bahwa tidak hanya mungkin untuk secara formal memverifikasi keandalan dan keamanan untuk proyek di tingkat sistem operasi industri, tetapi juga untuk mencapainya tanpa mengorbankan kinerja dan keserbagunaan.
Penghargaan Sistem Perangkat Lunak ACM diberikan setiap tahun untuk mengenali pengembangan sistem perangkat lunak yang memiliki dampak yang menentukan pada industri, memperkenalkan konsep baru atau membuka aplikasi komersial baru. Jumlah penghargaan adalah 35 ribu dolar AS. Dalam beberapa tahun terakhir, penghargaan ACM telah diberikan kepada proyek GCC dan LLVM, serta pendirinya Richard Stallman dan Chris Latner. Penghargaan juga diberikan untuk proyek dan teknologi seperti UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB dan gerhana.
Arsitektur mikrokernel seL4 terkenal karena penghapusan bagian untuk mengelola sumber daya kernel di ruang pengguna dan untuk menerapkan cara kontrol akses yang sama untuk sumber daya seperti untuk sumber daya pengguna. Mikrokernel tidak menyediakan abstraksi tingkat tinggi untuk mengelola file, proses, koneksi jaringan, dan sejenisnya, melainkan hanya menyediakan mekanisme minimal untuk mengontrol akses ke ruang alamat fisik, interupsi, dan sumber daya prosesor. Abstraksi tingkat tinggi dan driver untuk berinteraksi dengan perangkat keras diimplementasikan secara terpisah di atas mikrokernel dalam bentuk tugas tingkat pengguna. Akses tugas tersebut ke sumber daya yang tersedia untuk mikrokernel diatur melalui definisi aturan.
Sumber: opennet.ru