O projeto que desenvolve o microkernel seL4 aberto recebeu o ACM Software System Award, concedido anualmente pela Association for Computing Machinery (ACM), a organização internacional de maior autoridade na área de sistemas computacionais. O prêmio é concedido por conquistas na área de prova matemática de confiabilidade de operação, que demonstra total conformidade com especificações especificadas em linguagem formal e reconhece a prontidão para uso em aplicações de missão crítica. O projeto seL4 mostrou que não só é possível verificar formalmente a confiabilidade e a segurança para projetos em nível de sistema operacional industrial, mas também conseguir isso sem comprometer o desempenho e a versatilidade.
O ACM Software System Award é concedido anualmente para reconhecer o desenvolvimento de sistemas de software que tiveram um impacto decisivo na indústria, introduzindo novos conceitos ou abrindo novas áreas de aplicação comercial. O valor do prêmio é de 35 mil dólares americanos. Nos últimos anos, os prêmios ACM foram concedidos aos projetos GCC e LLVM e aos seus fundadores Richard Stallman e Chris Latner. O prêmio também reconheceu projetos e tecnologias como UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB e Eclipse. .
A arquitetura do microkernel seL4 é notável por mover partes para gerenciar recursos do kernel no espaço do usuário e usar as mesmas ferramentas de controle de acesso para esses recursos e para recursos do usuário. O microkernel não fornece abstrações de alto nível prontas para gerenciar arquivos, processos, conexões de rede e similares; em vez disso, ele fornece apenas mecanismos mínimos para controlar o acesso ao espaço de endereço físico, interrupções e recursos do processador. Abstrações e drivers de alto nível para interação com o hardware são implementados separadamente no microkernel na forma de tarefas no nível do usuário. O acesso de tais tarefas aos recursos disponíveis ao microkernel é organizado através da definição de regras.
Fonte: opennet.ru