O projeto que desenvolve o microkernel aberto seL4 recebeu o prêmio ACM Software System Award, concedido anualmente pela Association for Computing Machinery (ACM), a mais autoritária organização internacional na área de sistemas computacionais. O prêmio foi atribuído por conquistas em provas matemáticas de confiabilidade, que atestam a total conformidade às especificações definidas em linguagem formal e reconhecem a prontidão para uso em aplicações críticas. O projeto seL4 demonstrou que é possível realizar uma verificação formal completa da confiabilidade e segurança para projetos de sistemas operacionais industriais, alcançando isso sem comprometer o desempenho e a versatilidade.
O prêmio ACM Software System Award é anualmente entregue por inovações no desenvolvimento de sistemas de software que impactaram significativamente o setor, introduzindo novos conceitos ou explorando novas áreas de aplicação comercial. O valor do prêmio é de 35 mil dólares americanos. Em anos anteriores, o prêmio ACM foi concedido a projetos como GCC e LLVM, e seus fundadores Richard Stallman e Chris Lattner. Além disso, 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 também foram homenageados.
A arquitetura do microkernel seL4 se destaca pela deslocação de partes para o gerenciamento de recursos do núcleo para o espaço do usuário e a aplicação das mesmas ferramentas de controle de acesso para esses recursos, assim como para os recursos do usuário. O microkernel não oferece abstrações de alto nível prontas para o gerenciamento de arquivos, processos, conexões de rede, etc.; em vez disso, fornece apenas mecanismos mínimos para o controle de acesso ao espaço de endereçamento físico, interrupções e recursos do processador. Abstrações de alto nível e drivers para interagir com hardware são implementados separadamente sobre o microkernel na forma de tarefas executadas no nível do usuário. O acesso dessas tarefas aos recursos disponíveis do microkernel é organizado através da definição de regras.
Fonte: opennet.ru
