A Fundação RISC-V anunciou que verificou a funcionalidade do micronúcleo seL4 em sistemas com a arquitetura de conjunto de instruções RISC-V . O processo de verificação se resume a uma prova matemática da confiabilidade do seL4, indicando total conformidade com as especificações definidas em uma linguagem formal.
O teste de confiabilidade permite o uso do seL4 em sistemas de missão crítica baseados em processadores RISC-V RV64 , que exigem um nível mais alto de confiabilidade e não garantem a ausência de falhas.
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 destaca-se por remover partes responsáveis pelo gerenciamento de recursos do kernel no espaço do usuário e por utilizar os mesmos métodos de controle de acesso para esses recursos que são utilizados para recursos do usuário.
O micronúcleo não fornece abstrações de alto nível prontas para uso para gerenciar arquivos, processos, conexões de rede, etc., mas apenas mecanismos mínimos para controlar o acesso ao espaço de endereçamento 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.
O RISC-V oferece um sistema de instruções de máquina aberto e flexível que permite a criação de microprocessadores para aplicações arbitrárias, sem exigir adaptaçõ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 bits e, posteriormente, para processadores x86 de 64 bits.
Observa-se que a combinação da arquitetura de hardware aberta RISC-V com o microkernel aberto seL4 permitirá alcançar um novo nível de segurança , uma vez que os componentes de hardware no futuro também poderão ser totalmente verificados, o que é impossível de se obter com 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.
As plataformas de hardware aberto simplificam a integração de alterações relacionadas à segurança, por exemplo, para bloquear todos os possíveis canais de vazamento por meio de terceiros, onde é muito mais eficiente eliminar um problema por meio de hardware do que tentar encontrar soluções por software.
Por fim, se quiser saber mais sobre o assunto, pode consultar o artigo no seguinte link.