O proxecto de microkernel aberto seL4 recibiu o ACM Software System Award, un premio anual que outorga a Association for Computing Machinery (ACM), a organización internacional máis respectada no campo dos sistemas informáticos. O premio concédese aos logros no campo da proba matemática de funcionamento, que indica o cumprimento total das especificacións dadas nunha linguaxe formal e recoñece a dispoñibilidade para o seu uso en aplicacións de misión crítica. O proxecto seL4 demostrou que non só é posible verificar de xeito totalmente formal a fiabilidade e a seguridade dos proxectos a nivel de sistemas operativos industriais, senón tamén logralo sen sacrificar o rendemento e a versatilidade.
O ACM Software System Award preséntase anualmente para recoñecer o desenvolvemento de sistemas de software que tiveron un impacto definitorio na industria, introducindo novos conceptos ou abrindo novas aplicacións comerciais. O importe do premio é de 35 mil dólares estadounidenses. Nos últimos anos, entregáronse premios ACM aos proxectos GCC e LLVM, e aos seus fundadores Richard Stallman e Chris Latner. Outros proxectos e tecnoloxías que tamén foron premiados foron UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB e eclipse. .
A arquitectura do micronúcleo seL4 destaca pola eliminación de partes para xestionar os recursos do núcleo no espazo do usuario e pola aplicación dos mesmos medios de control de acceso para tales recursos que para os recursos do usuario. O micronúcleo non ofrece abstraccións de alto nivel listas para xestionar ficheiros, procesos, conexións de rede e similares, senón que ofrece só mecanismos mínimos para controlar o acceso ao espazo de enderezos físicos, interrupcións e recursos do procesador. As abstraccións de alto nivel e os controladores para interactuar co hardware impléntanse por separado encima do micronúcleo en forma de tarefas a nivel de usuario. O acceso destas tarefas aos recursos dos que dispón o micronúcleo organízase mediante a definición de regras.
Fonte: opennet.ru