Fondazione RISC-V sulla verifica del funzionamento del microkernel su sistemi con architettura del set di istruzioni RISC-V. La verifica si riduce a affidabilità del funzionamento di seL4, che indica il pieno rispetto delle specifiche specificate nel linguaggio formale. Prova di affidabilità seL4 in sistemi mission-critical basati su processori RISC-V RV64 che richiedono un maggiore livello di affidabilità e garantiscono l'assenza di guasti. Gli sviluppatori di software in esecuzione sul kernel seL4 possono essere completamente sicuri che se si verifica un guasto in una parte del sistema, questo guasto non si diffonderà al resto del sistema e, in particolare, alle sue parti critiche.
Il microkernel seL4 è stato inizialmente verificato per processori ARM a 32 bit e successivamente per processori x64 a 86 bit. Va notato che la combinazione dell'architettura hardware aperta RISC-V con il microkernel aperto seL4 consentirà di raggiungere un nuovo livello di sicurezza, poiché in futuro anche i componenti hardware potranno essere completamente verificati, cosa impossibile per le architetture hardware proprietarie.
Quando si verifica seL4, si presuppone che l'apparecchiatura funzioni come dichiarato e che le specifiche descrivano completamente il comportamento del sistema, ma in realtà l'apparecchiatura non è esente da errori, il che è chiaramente dimostrato dai problemi che emergono regolarmente nel meccanismo di esecuzione speculativa di Istruzioni. Le piattaforme hardware aperte semplificano l'integrazione delle modifiche relative alla sicurezza, ad esempio per bloccare tutte le possibili perdite di dati nei canali laterali, dove è molto più efficiente eliminare il problema nell'hardware piuttosto che cercare soluzioni alternative nel software.
Ricordiamo che l'architettura seL4 spostare parti per la gestione delle risorse del kernel nello spazio utente e applicare gli stessi mezzi di controllo dell'accesso per tali risorse come per le risorse utente. Il microkernel non fornisce astrazioni di alto livello già pronte per la gestione di file, processi, connessioni di rete e simili; fornisce invece solo meccanismi minimi per controllare l'accesso allo spazio degli indirizzi fisici, agli interrupt e alle risorse del processore. Astrazioni e driver di alto livello per l'interazione con l'hardware sono implementati separatamente sul microkernel sotto forma di attività a livello utente. L'accesso di tali compiti alle risorse a disposizione del microkernel è organizzato attraverso la definizione di regole.
RISC-V fornisce un sistema di istruzioni macchina aperto e flessibile che consente di costruire microprocessori per applicazioni arbitrarie senza richiedere royalties o vincoli per l'uso. RISC-V consente di creare SoC e processori completamente aperti. Attualmente basato sulla specifica RISC-V di diverse aziende e comunità con varie licenze libere (BSD, MIT, Apache 2.0) diverse dozzine di varianti di core di microprocessori, SoC e chip già prodotti. Il supporto RISC-V è presente sin dai rilasci di Glibc 2.27, binutils 2.30, gcc 7 e del kernel Linux 4.15.
Fonte: opennet.ru