A Fundação RISC-V anunciou que verificou como funciona o microkernel seL4 em sistemas com a arquitetura do conjunto de instruções RISC-V. Em que o processo de verificação é reduzido à prova matemática da confiabilidade de seL4, que indica o cumprimento integral das especificações especificadas em linguagem formal.
O teste de confiabilidade permite que o seL4 seja usado em sistemas de missão crítica baseados em processadores RISC-V RV64, o que requer um nível mais alto de confiabilidade e não garante falha.
Os desenvolvedores de software executados sobre o kernel seL4 podem ter certeza absoluta de que, no caso de 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. .
Sobre seL4
A arquitetura seL4 é notável por remover partes para gerenciar recursos do kernel no espaço do usuário e usar os mesmos métodos de controle de acesso para esses recursos e para os recursos do usuário.
O microkernel não fornece abstrações de alto nível já preparado para gerenciar arquivos, processos, conexões de rede, etc., mas em vez 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 controladores de alto nível para interagir com o computador são implementados separadamente no topo do microkernel na forma de tarefas realizadas no nível do usuário.
O acesso de tais tarefas aos recursos disponíveis no microkernel é organizado por meio da definição de regras.
RISC-V fornece um sistema aberto e flexível de instruções da máquina que permite criar microprocessadores para aplicações arbitrárias, sem exigir deduções e sem impor condições de uso.
O RISC-V permite que você crie SoCs e processadores completamente abertos. Atualmente, com base na especificação RISC-V, várias empresas e comunidades sob várias licenças gratuitas (BSD, MIT, Apache 2.0) estão desenvolvendo várias dezenas de variantes de núcleos de microprocessador, SoCs e chips já produzidos.
O suporte RISC-V existe desde o lançamento do Glibc 2.27, binutils 2.30, gcc 7 e o kernel Linux 4.15.
Sobre o teste de microkernel seL4
Inicialmente, o microkernel seL4 foi verificado para processadores ARM de 32 bitse mais tarde para processadores x86 de 64 bits.
Observa-se que a combinação da arquitetura de hardware aberto RISC-V com o microkernel aberto seL4 alcançará um novo nível de segurança, já que os futuros componentes de hardware também podem ser totalmente verificados, o que é impossível de se conseguir para arquiteturas de hardware proprietárias.
Quando verificamos seL4, devemos assumir que o hardware está funcionando corretamente (ou seja, conforme especificado). Isso assume que há uma especificação inequívoca em primeiro lugar, o que não é o caso para todo hardware.
Mas mesmo quando essa especificação existe e é formal (isto é, escrita em um formalismo matemático que apóia o raciocínio matemático sobre suas propriedades), como sabemos que ela realmente captura o comportamento do hardware?
A realidade é que podemos ter certeza de que não é. O hardware não é diferente do software porque ambos apresentam erros.
Mas ter um ISA aberto tem vantagens que vão além de ser isento de royalties. Uma é que permite implementações de hardware de código aberto.
Ao verificar seL4, assume-se que o equipamento funciona conforme indicado e a especificação descreve totalmente o comportamento do sistema, mas na verdade o equipamento não está livre de erros, o que é bem demonstrado por problemas que surgem regularmente no mecanismo de execução especulativa Instruções.
Plataformas de hardware abertas simplificam a integração de mudanças relacionados à segurança, por exemplo, para bloquear todos os canais de vazamento possíveis através de canais de terceiros, onde é muito mais eficiente se livrar de um problema por hardware do que tentar encontrar soluções por software.
Por fim, se quiser saber mais sobre o assunto, pode consultar a nota no link a seguir
Para mim, esse processador é algo que me chama muito. Resta apenas um cão gordo de computador fazer um computador que possamos comprar.
A questão do ARM é uma coisa que me incomoda, vocês já viram o que aconteceu com a Huawei com as sanções. Estou certo de que, para meu RISC-V, é uma solução muito melhor em todos os níveis. No momento a Huawei já está de olho nele e talvez no futuro tenham equipamentos com este micro. Se for assim, com certeza haverá mais empresas que irão adotá-lo e para mim esse seria o ideal e acima de tudo que as distros o apoiem e não apenas o ARM como acontece com a maioria.
+10