Organização RISC-V Foundation a verificação do microkernel em sistemas com arquitetura de conjunto de instruções RISC-V. A verificação consiste em da confiabilidade da operação do seL4, que comprova a total conformidade com as especificações definidas em uma linguagem formal. A prova de confiabilidade o seL4 em sistemas críticos baseados em processadores RISC-V RV64, que exigem um alto nível de confiabilidade e garantem a ausência de falhas. Os desenvolvedores de software que opera sobre o núcleo seL4 podem ter total confiança de que, em caso de falha em uma parte do sistema, essa falha não se espalhará para o restante do sistema e, em particular, para suas partes críticas.
O microkernel seL4 foi inicialmente verificado para processadores ARM de 32 bits e, posteriormente, para processadores x86 de 64 bits. É notável que a combinação da arquitetura de hardware aberto RISC-V com o microkernel aberto seL4 permitirá alcançar um novo nível de segurança, uma vez que os componentes de hardware também podem ser totalmente verificados no futuro, o que não é viável para arquiteturas de hardware proprietárias.
Na verificação do seL4, assume-se que o hardware opera como declarado e que a especificação descreve totalmente o comportamento do sistema, mas na realidade o hardware não está isento de erros, o que é bem demonstrado pelos problemas recorrentes que surgem no mecanismo de execução especulativa de instruções. As plataformas de hardware abertas simplificam a integração de mudanças relacionadas à segurança — por exemplo, para bloquear todos os possíveis canais de vazamento por canais colaterais, onde é muito mais eficaz resolver o problema no nível do hardware do que tentar encontrar soluções alternativas no software.
Lembramos que a arquitetura seL4 a alocação de partes para gerenciamento de recursos do núcleo no espaço do usuário e a aplicação das mesmas ferramentas de controle de acesso para esses recursos, como para recursos do usuário. O micronúcleo não fornece abstrações de alto nível prontas para gerenciamento de arquivos, processos, conexões de rede, etc., em vez disso, oferece apenas mecanismos mínimos para controlar o acesso ao espaço de endereços físico, interrupções e recursos do processador. Abstrações de alto nível e drivers para interação com hardware são implementados separadamente sobre o micronúcleo na forma de tarefas executadas em nível de usuário. O acesso a esses recursos do micronúcleo por parte dessas tarefas é organizado através da definição de regras.
O RISC-V fornece um sistema de instruções de máquina aberto e flexível, permitindo a criação de microprocessadores para diversas áreas de aplicação, sem exigir pagamentos e sem impor condições de uso. O RISC-V possibilita a criação de SoCs e processadores totalmente abertos. Atualmente, várias empresas e comunidades estão desenvolvendo com base na especificação RISC-V sob diversas licenças livres (BSD, MIT, Apache 2.0). várias dezenas de variantes de núcleos de microprocessadores, SoCs e chips já em produção. O suporte ao RISC-V está presente desde as versões Glibc 2.27, binutils 2.30, gcc 7 e do núcleo Linux 4.15.
Fonte: opennet.ru
