RISC-V verificou o microkernel seL4 em seus processadores RV64

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


2 comentários, deixe o seu

Deixe um comentário

Seu endereço de email não será publicado. Campos obrigatórios são marcados com *

*

*

  1. Responsável pelos dados: Miguel Ángel Gatón
  2. Finalidade dos dados: Controle de SPAM, gerenciamento de comentários.
  3. Legitimação: Seu consentimento
  4. Comunicação de dados: Os dados não serão comunicados a terceiros, exceto por obrigação legal.
  5. Armazenamento de dados: banco de dados hospedado pela Occentus Networks (UE)
  6. Direitos: A qualquer momento você pode limitar, recuperar e excluir suas informações.

  1.   um de alguns dito

    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.

    1.    Gregory Ros dito

      +10