Organizzazione RISC-V Foundation sulla verifica del funzionamento del microkernel su sistemi con architettura del set di istruzioni RISC-V. La verifica consiste in dell'affidabilità di seL4, che attesta la piena conformità alle specifiche formalmente definite. La dimostrazione dell'affidabilità seL4 in sistemi critici basati su processori RISC-V RV64, che richiedono un elevato livello di affidabilità e garantiscono l'assenza di guasti. 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 propagherà al resto del sistema e, in particolare, alle sue parti critiche.
Originariamente, il microkernel seL4 è stato verificato per processori ARM a 32 bit, e successivamente per processori x86 a 64 bit. Si osserva che la combinazione dell'architettura hardware open source RISC-V con il microkernel open source seL4 consentirà di raggiungere un nuovo livello di sicurezza, poiché i componenti hardware potrebbero anche essere completamente verificati, cosa non ottenibile con architetture hardware proprietarie.
Durante la verifica di seL4 si presume che l'hardware funzioni come dichiarato e che le specifiche descrivano completamente il comportamento del sistema, ma in realtà l'hardware non è esente da errori, come dimostrano regolarmente i problemi nel meccanismo di esecuzione speculativa delle istruzioni. Le piattaforme hardware open source semplificano l'integrazione delle modifiche relative alla sicurezza: ad esempio, per bloccare tutti i possibili canali di fuga attraverso canali secondari, è molto più efficace risolvere il problema a livello hardware piuttosto che cercare soluzioni software.
Ricordiamo che l'architettura seL4 con estrazione di parti per la gestione delle risorse del kernel nello spazio utente e utilizzo per tali risorse degli stessi strumenti di accesso controllato come per le risorse utente. Il microkernel non fornisce astrazioni di alto livello pronte per la gestione di file, processi, connessioni di rete, ecc.; invece, offre solo meccanismi minimi per la gestione dell'accesso allo spazio indirizzi fisico, alle interruzioni e alle risorse della CPU. Le astrazioni di alto livello e i driver per l'interazione con l'hardware vengono implementati separatamente sopra il microkernel sotto forma di task eseguiti a livello utente. L'accesso di tali task alle risorse disponibili del microkernel è organizzato attraverso la definizione di regole.
RISC-V offre un'architettura aperta e flessibile per set di istruzioni, consentendo la creazione di microprocessori per applicazioni diverse senza costi di licenza né condizioni restrittive sull'uso. RISC-V permette lo sviluppo di SoC e processori completamente aperti. Attualmente, sulla base della specifica RISC-V, diverse aziende e comunità stanno lavorando a chip già prodotti con diverse licenze aperte (BSD, MIT, Apache 2.0). un'ampia gamma di core di microprocessori, SoC e chip già in produzione. Il supporto per RISC-V è disponibile a partire dalle versioni di Glibc 2.27, binutils 2.30, gcc 7 e del kernel Linux 4.15.
Fonte: opennet.ru
