Organizzazione RISC-V Foundation sulla verifica del funzionamento del microkernel su sistemi con architettura del set di istruzioni RISC-V. La verifica consiste in della robustezza del funzionamento di seL4, che attesta la piena conformità alle specifiche date in un linguaggio formale. La dimostrazione della robustezza seL4 in sistemi critici basati su processori RISC-V RV64, che richiedono un livello elevato di affidabilità e garantiscono l'assenza di malfunzionamenti. Gli sviluppatori di software che operano sopra il kernel seL4 possono essere completamente certi che in caso di guasto in una parte del sistema, tale guasto non si diffonderà al restante sistema e, in particolare, alle sue parti critiche.
Inizialmente, il microkernel seL4 è stato verificato per processori ARM a 32 bit, e successivamente per processori x86 a 64 bit. Si osserva che la combinazione di un'architettura hardware aperta RISC-V con un microkernel aperto seL4 porterà a un nuovo livello di sicurezza, poiché i componenti hardware potrebbero, in prospettiva, essere completamente verificati, cosa impossibile da ottenere per le architetture hardware proprietarie.
Nella verifica di seL4 si presuppone che l'hardware funzioni come dichiarato e che le specifiche descrivano completamente il comportamento del sistema, ma di fatto l'hardware non è esente da errori, come dimostrano bene i problemi ricorrenti nel meccanismo di esecuzione speculativa delle istruzioni. Le piattaforme hardware aperte semplificano l'integrazione delle modifiche relative alla sicurezza — ad esempio, per bloccare tutti i possibili canali di fuga attraverso canali esterni, dove è molto più efficace risolvere il problema a livello hardware piuttosto che cercare di trovare soluzioni software.
Ricordiamo che l'architettura seL4 la gestione delle risorse di sistema del kernel nello spazio utente e l'applicazione per tali risorse degli stessi strumenti di controllo degli accessi utilizzati per le risorse dell'utente. Il microkernel non fornisce astrazioni ad alto livello pronte all'uso per la gestione di file, processi, connessioni di rete, ecc., ma fornisce solo i meccanismi minimi per la gestione dell'accesso allo spazio indirizzamento fisico, alle interruzioni e alle risorse della CPU. Le astrazioni ad alto livello e i driver per l'interazione con l'hardware vengono implementati separatamente sopra il microkernel sotto forma di attività eseguite a livello utente. L'accesso di tali attività alle risorse del microkernel è organizzato tramite la definizione di regole.
RISC-V fornisce un sistema di istruzioni macchina aperto e flessibile, consentendo la creazione di microprocessori per applicazioni diverse senza richiedere royalties e senza vincoli d'uso. RISC-V consente la creazione di SoC e processori completamente aperti. Attualmente, sulla base della specifica RISC-V, varie aziende e comunità stanno sviluppando diversi spin-off con varie licenze open source (BSD, MIT, Apache 2.0) decine di varianti di nuclei di microprocessori, SoC e chip già prodotti. Il supporto per RISC-V è disponibile a partire dalle versioni Glibc 2.27, binutils 2.30, gcc 7 e del kernel Linux 4.15.
Fonte: opennet.ru
