Fundación RISC-V sobre a verificación do funcionamento do micronúcleo en sistemas con arquitectura de conxunto de instrucións RISC-V. A verificación redúcese a fiabilidade do funcionamento seL4, que indica o cumprimento total das especificacións especificadas na linguaxe formal. Proba de fiabilidade seL4 en sistemas de misión crítica baseados en procesadores RISC-V RV64 que requiren un maior nivel de fiabilidade e garanten a ausencia de fallos. Os desenvolvedores de software que se executan sobre o núcleo seL4 poden estar completamente seguros de que se hai un fallo nunha parte do sistema, este fallo non se estenderá ao resto do sistema e, en particular, ás súas partes críticas.
O microkernel seL4 verificouse inicialmente para procesadores ARM de 32 bits, e posteriormente para procesadores x64 de 86 bits. Nótase que a combinación da arquitectura de hardware aberta RISC-V co micronúcleo aberto seL4 acadará un novo nivel de seguridade, xa que os compoñentes de hardware tamén se poden verificar completamente no futuro, o que é imposible de conseguir para as arquitecturas de hardware propietarias.
Ao verificar seL4, asúmese que o equipo funciona como se indica e que a especificación describe completamente o comportamento do sistema, pero en realidade o equipo non está exento de erros, o que se demostra claramente polos problemas que aparecen regularmente no mecanismo de execución especulativa de instrucións. As plataformas de hardware abertas facilitan a integración de cambios relacionados coa seguridade, por exemplo, para bloquear todas as posibles fugas de canles laterais, onde é moito máis eficiente desfacerse do problema no hardware que tratar de buscar solucións no software.
Lembremos que a arquitectura seL4 movendo partes para xestionar os recursos do núcleo no espazo do usuario e aplicar os mesmos medios de control de acceso para tales recursos que para os recursos do usuario. O micronúcleo non ofrece abstraccións de alto nivel preparadas para xestionar ficheiros, procesos, conexións de rede e similares; en cambio, ofrece só mecanismos mínimos para controlar o acceso ao espazo de enderezo físico, interrupcións e recursos do procesador. As abstraccións de alto nivel e os controladores para interactuar co hardware impléntanse por separado encima do micronúcleo en forma de tarefas a nivel de usuario. O acceso destas tarefas aos recursos dispoñibles para o micronúcleo organízase mediante a definición de regras.
RISC-V ofrece un sistema de instrución de máquina aberto e flexible que permite construír microprocesadores para aplicacións arbitrarias sen necesidade de dereitos ou cadeas para o seu uso. RISC-V permítelle crear SoC e procesadores completamente abertos. Actualmente baseado na especificación RISC-V de diferentes empresas e comunidades baixo varias licenzas libres (BSD, MIT, Apache 2.0) varias ducias de variantes de núcleos de microprocesadores, SoC e chips xa producidos. O soporte RISC-V estivo presente dende os lanzamentos de Glibc 2.27, binutils 2.30, gcc 7 e o núcleo de Linux 4.15.
Fonte: opennet.ru