El proyecto que desarrolla el microkernel abierto seL4 ha recibido el premio ACM Software System Award, otorgado anualmente por la Asociación de Maquinaria Computacional (ACM), la organización internacional más reconocida en el ámbito de los sistemas informáticos. El premio se concede por logros en la prueba matemática de la fiabilidad operativa, que demuestra el cumplimiento total de las especificaciones dadas en un lenguaje formal y reconoce su preparación para su uso en aplicaciones críticas. El proyecto seL4 ha demostrado que es posible realizar una verificación formal completa de la fiabilidad y seguridad para proyectos a nivel de sistemas operativos industriales, sin comprometer el rendimiento y la versatilidad.
El premio ACM Software System Award se otorga anualmente por el desarrollo de sistemas de software que han tenido un impacto significativo en la industria, introduciendo nuevos conceptos o descubriendo nuevas áreas de aplicación comercial. El monto del premio es de 35,000 dólares estadounidenses. En años anteriores, los premios ACM han sido otorgados a proyectos como GCC y LLVM, así como a sus fundadores Richard Stallman y Chris Lattner. También se han reconocido proyectos y tecnologías como 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 es notable por la delegación de partes de la gestión de recursos del núcleo al espacio del usuario y por el uso de los mismos mecanismos de control de acceso para estos recursos que para los recursos de usuario. El microkernel no proporciona abstracciones de alto nivel listas para gestionar archivos, procesos, conexiones de red, etc. En su lugar, ofrece solo mecanismos mínimos para gestionar el acceso al espacio de direcciones físicas, interrupciones y recursos del procesador. Las abstracciones de alto nivel y los controladores para interactuar con el hardware se implementan por separado sobre el microkernel en forma de tareas que se ejecutan en el nivel de usuario. El acceso de estas tareas a los recursos disponibles en el microkernel se organiza mediante la definición de reglas.
Fuente: opennet.ru
