Fundação RISC-V sobre como verificar a operação do microkernel em sistemas com arquitetura de conjunto de instruções RISC-V. A verificação se resume a confiabilidade da operação do seL4, o que indica total conformidade com as especificações especificadas na linguagem formal. Prova de confiabilidade seL4 em sistemas de missão crítica baseados em processadores RISC-V RV64 que exigem maior nível de confiabilidade e garantem ausência de falhas. Os desenvolvedores de software executado no kernel seL4 podem estar completamente confiantes de que, se houver uma falha em uma parte do sistema, essa falha não se espalhará para o resto 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 x64 de 86 bits. Observa-se que a combinação da arquitetura de hardware aberta RISC-V com o microkernel seL4 aberto alcançará um novo nível de segurança, uma vez que os componentes de hardware também poderão ser totalmente verificados no futuro, o que é impossível de alcançar para arquiteturas de hardware proprietárias.
Ao verificar o seL4, assume-se que o equipamento funciona conforme declarado e a especificação descreve completamente o comportamento do sistema, mas na realidade o equipamento não está isento de erros, o que é claramente demonstrado pelos problemas emergentes regularmente no mecanismo de execução especulativa de instruções. Plataformas de hardware abertas facilitam a integração de mudanças relacionadas à segurança – por exemplo, para bloquear todos os possíveis vazamentos de canal lateral, onde é muito mais eficiente se livrar do problema no hardware do que tentar encontrar soluções alternativas no software.
Lembre-se de que a arquitetura seL4 mover partes para gerenciar recursos do kernel no espaço do usuário e aplicar os mesmos meios de controle de acesso para tais 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.
O RISC-V fornece um sistema de instrução de máquina aberto e flexível que permite que microprocessadores sejam construídos para aplicações arbitrárias sem a necessidade de royalties ou restrições de uso. RISC-V permite criar SoCs e processadores completamente abertos. Atualmente baseado na especificação RISC-V por diferentes empresas e comunidades sob diversas licenças gratuitas (BSD, MIT, Apache 2.0) várias dezenas de variantes de núcleos de microprocessadores, SoCs e chips já produzidos. O suporte RISC-V está presente desde os lançamentos do Glibc 2.27, binutils 2.30, gcc 7 e do kernel Linux 4.15.
Fonte: opennet.ru