Finalizou-se o trabalho de verificação formal matemática da confiabilidade e segurança do microkernel seL4 em sistemas com arquitetura de conjunto de instruções AArch64. A verificação consiste em uma prova matemática da correção do funcionamento do seL4, que atesta a total conformidade com as especificações definidas em linguagem formal. A prova de confiabilidade permite o uso do seL4 em sistemas críticos baseados em processadores ARM64, que exigem um nível elevado de segurança e garantem a ausência de falhas.
Inicialmente, o microkernel seL4 foi verificado para processadores ARM de 32 bits, e posteriormente para processadores de 64 bits x86 e RISC-V. A verificação garante que, em caso de falha em uma parte do sistema, essa falha não se espalhe para o restante do sistema e suas partes críticas. No contexto da segurança, a verificação confirma que o núcleo proporciona o devido nível de isolamento das aplicações, não permitindo que elas acessem informações sem autorização e garantindo que, em caso de comprometimento de aplicações secundárias, o ataque não se espalhe para aplicações críticas.
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
