El proyecto de microkernel abierto seL4 ha recibido el ACM Software System Award, un premio anual que otorga la Association for Computing Machinery (ACM), la organización internacional más respetada en el campo de los sistemas informáticos. El premio se otorga por los logros en el campo de la prueba matemática de operación, que indica el pleno cumplimiento de las especificaciones dadas en un lenguaje formal y reconoce la preparación para su uso en aplicaciones de misión crítica. El proyecto seL4 ha demostrado que no solo es posible verificar formalmente la confiabilidad y la seguridad de los proyectos a nivel de sistemas operativos industriales, sino también lograr esto sin sacrificar el rendimiento y la versatilidad.
El premio ACM Software System Award se presenta anualmente para reconocer el desarrollo de sistemas de software que han tenido un impacto decisivo en la industria, introduciendo nuevos conceptos o abriendo nuevas aplicaciones comerciales. El monto del premio es de 35 mil dólares estadounidenses. En los últimos años, los premios ACM se otorgaron a los proyectos GCC y LLVM, y a sus fundadores, Richard Stallman y Chris Latner. Otros proyectos y tecnologías que también fueron premiados fueron UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB y eclipse .
La arquitectura del microkernel seL4 se destaca por la eliminación de partes para administrar los recursos del kernel en el espacio del usuario y por aplicar los mismos medios de control de acceso para dichos recursos que para los recursos del usuario. El microkernel no proporciona abstracciones de alto nivel listas para usar para administrar archivos, procesos, conexiones de red y similares, sino que solo proporciona mecanismos mínimos para controlar el acceso al espacio de direcciones físicas, las interrupciones y los recursos del procesador. Las abstracciones de alto nivel y los controladores para interactuar con el hardware se implementan por separado en la parte superior del microkernel en forma de tareas a nivel de usuario. El acceso de tales tareas a los recursos disponibles para el microkernel se organiza a través de la definición de reglas.
Fuente: opennet.ru