Fundació RISC-V sobre la verificació del funcionament del micronucli en sistemes amb arquitectura de conjunt d'instruccions RISC-V. La verificació es redueix a fiabilitat del funcionament seL4, que indica el compliment total de les especificacions especificades en el llenguatge formal. Prova de fiabilitat seL4 en sistemes de missió crítica basats en processadors RISC-V RV64 que requereixen un major nivell de fiabilitat i garanteixen l'absència de fallades. Els desenvolupadors de programari que s'executen a la part superior del nucli seL4 poden estar completament segurs que si hi ha una fallada en una part del sistema, aquesta fallada no s'estendrà a la resta del sistema i, en particular, a les seves parts crítiques.
El micronucli seL4 es va verificar inicialment per als processadors ARM de 32 bits, i més tard per als processadors x64 de 86 bits. Cal assenyalar que la combinació de l'arquitectura de maquinari oberta RISC-V amb el micronucli obert seL4 aconseguirà un nou nivell de seguretat, ja que els components de maquinari també es podran verificar completament en el futur, cosa que és impossible d'aconseguir per a arquitectures de maquinari propietàries.
Quan es verifica seL4, s'assumeix que l'equip funciona tal com s'indica i que l'especificació descriu completament el comportament del sistema, però en realitat l'equip no està exempt d'errors, cosa que es demostra clarament pels problemes que apareixen regularment en el mecanisme d'execució especulativa de instruccions. Les plataformes de maquinari obertes faciliten la integració de canvis relacionats amb la seguretat, per exemple, bloquejar totes les possibles filtracions de canals laterals, on és molt més eficient desfer-se del problema en el maquinari que intentar trobar solucions al programari.
Recordem que l'arquitectura seL4 moure parts per gestionar els recursos del nucli a l'espai d'usuari i aplicar els mateixos mitjans de control d'accés per a aquests recursos que per als recursos d'usuari. El micronucli no proporciona abstraccions d'alt nivell ja fetes per gestionar fitxers, processos, connexions de xarxa i similars; en canvi, només proporciona mecanismes mínims per controlar l'accés a l'espai d'adreces físiques, interrupcions i recursos del processador. Les abstraccions d'alt nivell i els controladors per interaccionar amb el maquinari s'implementen per separat a la part superior del micronucli en forma de tasques a nivell d'usuari. L'accés d'aquestes tasques als recursos disponibles per al micronucli s'organitza mitjançant la definició de regles.
RISC-V proporciona un sistema d'instrucció de màquines obert i flexible que permet construir microprocessadors per a aplicacions arbitràries sense requerir drets d'autor o cadenes adjuntes per utilitzar-los. RISC-V us permet crear SoC i processadors completament oberts. Actualment basat en l'especificació RISC-V de diferents empreses i comunitats sota diverses llicències lliures (BSD, MIT, Apache 2.0) diverses desenes de variants de nuclis de microprocessador, SoC i xips ja produïts. El suport RISC-V ha estat present des dels llançaments de Glibc 2.27, binutils 2.30, gcc 7 i el nucli Linux 4.15.
Font: opennet.ru