La Fundació RISC-V va anunciar que ha verificat el funcionament de l'microkernel seL4 en sistemes amb l'arquitectura del conjunt d'instruccions RISC-V. En la qual el procés de verificació es redueix a la prova matemàtica de la fiabilitat de seL4, el que indica el ple compliment de les especificacions especificades en un llenguatge formal.
La prova de fiabilitat permet usar seL4 en sistemes de missió crítica basats en processadors RISC-V RV64, El que requereix un major nivell de fiabilitat i no garanteix falles.
Els desenvolupadors de programari que s'executen a la part superior de l'nucli seL4 poden estar completament segurs que, en cas d'una falla en una part de el sistema, aquesta falla no s'estendrà a la resta de sistema i, en particular, a les seves parts crítiques .
sobre seL4
L'arquitectura seL4 és notable per l'eliminació de parts per administrar els recursos de l'nucli en l'espai de l'usuari i usar els mateixos mètodes de control d'accés per a tals recursos com per als recursos de l'usuari.
el microkernel no proporciona abstraccions d'alt nivell ja preparades per administrar arxius, processos, connexions de xarxa, etc., sinó que només proporciona mecanismes mínims per controlar l'accés a l'espai d'adreces físiques, Les interrupcions i els recursos de l'processador.
Les abstraccions d'alt nivell i els controladors per interactuar amb l'equip s'implementen per separat en la part superior de l'microkernel en forma de tasques realitzades a nivell d'usuari.
L'accés d'aquests tasques als recursos disponibles al microkernel s'organitza a través de la definició de regles.
RISC-V proporciona un sistema obert i flexible d'instruccions de màquina que permet crear microprocessadors per a aplicacions arbitràries, sense requerir deduccions i sense imposar condicions d'ús.
RISC-V permet crear SoCs i processadors completament oberts. Actualment, sobre la base de l'especificació RISC-V, diverses companyies i comunitats sota diverses llicències gratuïtes (BSD, MIT, Apache 2.0) estan desenvolupant diverses dotzenes de variants de nuclis de microprocessador, SoC i xips ja produïts.
El suport RISC-V ha estat present des del llançament de Glibc 2.27, binutils 2.30, gcc 7 i el nucli Linux 4.15.
Sobre la proves de l'microkernel seL4
Inicialment, el microkernel seL4 va ser verificat per a processadors ARM de 32 bits i més tard per a processadors x86 de 64 bits.
S'observa que la combinació de l'arquitectura de maquinari obert RISC-V amb el microkernel obert seL4 aconseguirà un nou nivell de seguretat, Ja que els components de maquinari en el futur també poden verificar completament, el que és impossible d'aconseguir per a les arquitectures de maquinari patentades.
Quan verifiquem seL4, hem de suposar que el maquinari funciona correctament (és a dir, com s'especifica). Això suposa que hi ha una especificació inequívoca en primer lloc, que no és el cas per a tot el maquinari.
Però fins i tot quan existeix tal especificació, i és formal (és a dir, Ritten en un formalisme matemàtic que admet el raonament matemàtic sobre les seves propietats), com sabem que realment captura el comportament de el maquinari?
La realitat és que podem estar bastant segurs que no és així. El maquinari no és diferent del programari en què tots dos tenen errors.
Però tenir un ISA obert té avantatges que van més enllà d'estar lliures de regalies. Una és que permet tenir implementacions de maquinari de codi obert.
A l'verificar seL4, se suposa que l'equip funciona com s'indica i l'especificació descriu completament el comportament de sistema, però de fet l'equip no està lliure d'errors, la qual cosa està ben demostrat per problemes que sorgeixen regularment en el mecanisme d'execució especulativa d'instruccions.
Les plataformes de maquinari obertes simplifiquen la integració dels canvis relacionats amb la seguretat, per exemple, per a bloquejar tots els canals de fugida possibles a través de canals de tercers, en els quals és molt més eficient desfer-se d'un problema per maquinari que tractar de trobar solucions per programari.
Finalment, si vols conèixer més a l'respecte, pots consultar la nota al següent enllaç.
A mi el d'aquest processador és una cosa que em crida molt. Només falta que algun gos gros de la computacion faci un ordinador que puguem comprar.
Al meu el tema ARM és una cosa que em grinyola, ja es va veure el que va passar amb Huawei amb les sancions. Tinc clar que per a mi RISC-V és una solució molt millor a tots els nivells. De moment Huawei ja li ha posat l'ull i potser en un futur tinguin equips amb aquest micro. De ser així segur que hi haurà més empreses que l'adoptin i per a mi això seria l'ideal i sobretot que les distros li donin suport i no només a ARM com passa amb la majoria.
+ 10