Fondazione RISC-V circa a verificazione di u funziunamentu di u microkernel nantu à i sistemi cù l'architettura di set di istruzioni RISC-V. A verificazione vene à affidabilità di l'operazione seL4, chì indica u cumpletu cumpletu cù e specificazioni specificate in a lingua formale. Prova di affidabilità seL4 in sistemi di missione critica basati nantu à i processori RISC-V RV64 chì necessitanu un livellu aumentatu di affidabilità è guarantisci l'assenza di fallimenti. I sviluppatori di u software chì currenu nantu à u kernel seL4 ponu esse cumplettamente cunfidenti chì s'ellu ci hè un fallimentu in una parte di u sistema, questu fallimentu ùn si sparghjerà à u restu di u sistema è, in particulare, i so parti critichi.
U microkernel seL4 hè stata verificata inizialmente per i prucessori ARM 32-bit, è più tardi per i processori x64 86-bit. Hè nutatu chì a cumminazzioni di l'architettura hardware aperta RISC-V cù u microkernel apertu seL4 uttene un novu livellu di sicurità, postu chì i cumpunenti di hardware ponu ancu esse verificati cumplettamente in u futuru, chì hè impussibile di ottene per l'architetture hardware proprietarie.
Quandu verificate seL4, si assume chì l'equipaggiu funziona cum'è dichjaratu è a specificazione descrive cumplettamente u cumpurtamentu di u sistema, ma in realtà l'equipaggiu ùn hè micca liberu di errori, chì hè chjaramente dimustratu da prublemi regularmente emergenti in u mecanismu di esecuzione speculativa di istruzioni. I plataformi di hardware aperti facenu più faciule per integrà i cambiamenti legati à a sicurità - per esempiu, per bluccà tutte e fughe di canali laterali pussibuli, induve hè assai più efficaci per sbarazzarsi di u prublema in hardware cà di pruvà à truvà solu solu in u software.
Ricurdativi chì l'architettura seL4 muvimenti parti per a gestione di e risorse di u kernel in u spaziu di l'utilizatori è l'applicà i stessi mezi di cuntrollu d'accessu per tali risorse cum'è per e risorse di l'utilizatori. U microkernel ùn furnisce micca astrazioni d'altu livellu prontu per a gestione di fugliali, prucessi, cunnessione di rete, è simili; invece, furnisce solu miccanismi minimi per cuntrullà l'accessu à u spaziu di indirizzu fisicu, interruzioni è risorse di processore. L'astrazioni d'altu livellu è i driver per l'interazzione cù u hardware sò implementati separatamente nantu à u microkernel in forma di attività à livellu d'utilizatore. L'accessu di tali compiti à e risorse dispunibili à u microkernel hè urganizatu per mezu di a definizione di regule.
RISC-V furnisce un sistema d'istruzzioni di a macchina aperta è flessibile chì permette à i microprocessori di esse custruitu per applicazioni arbitrarie senza bisognu di royalties o strings attaccati à l'usu. RISC-V permette di creà SoC è processori completamente aperti. Attualmente basatu annantu à a specificazione RISC-V da diverse cumpagnie è cumunità sottu diverse licenze libere (BSD, MIT, Apache 2.0) parechje decine di varianti di nuclei di microprocessori, SoC è chips digià pruduciuti. U supportu RISC-V hè presente da i versioni di Glibc 2.27, binutils 2.30, gcc 7, è u kernel Linux 4.15.
Source: opennet.ru