La Fondazione RISC-V ha annunciato di aver verificato la funzionalità del microkernel seL4 su sistemi con architettura del set di istruzioni RISC-V . Il processo di verifica si riduce a una dimostrazione matematica dell'affidabilità di seL4, che indica la piena conformità alle specifiche definite in un linguaggio formale.
Il test di affidabilità consente l'utilizzo di seL4 in sistemi mission-critical basati su processori RISC-V RV64 , che richiedono un livello di affidabilità superiore e non garantiscono l'assenza di guasti.
Gli sviluppatori di software che eseguono il kernel seL4 possono essere completamente sicuri che in caso di guasto in una parte del sistema, questo guasto non si diffonderà al resto del sistema e, in particolare, alle sue parti critiche.
Informazioni su seL4
L'architettura seL4 si distingue per aver rimosso le parti relative alla gestione delle risorse del kernel dallo spazio utente e per aver utilizzato gli stessi metodi di controllo degli accessi per tali risorse impiegati per le risorse utente.
Il microkernel non fornisce astrazioni di alto livello predefinite per la gestione di file, processi, connessioni di rete, ecc., ma offre solo meccanismi minimi per il controllo dell'accesso allo spazio degli indirizzi fisici , agli interrupt e alle risorse del processore.
Astrazioni e controller di alto livello per l'interazione con il computer vengono implementati separatamente sopra il microkernel sotto forma di attività eseguite a livello utente.
L'accesso di tali task alle risorse disponibili nel microkernel è organizzato attraverso la definizione di regole.
RISC-V offre un sistema di istruzioni macchina aperto e flessibile che consente la creazione di microprocessori per applicazioni arbitrarie, senza richiedere deduzioni e senza imporre condizioni d'uso.
RISC-V ti consente di creare processori e SoC completamente aperti. Attualmente, sulla base della specifica RISC-V, diverse società e comunità con varie licenze libere (BSD, MIT, Apache 2.0) stanno sviluppando diverse dozzine di varianti di core di microprocessore, SoC e chip già prodotti.
Il supporto RISC-V esiste dal rilascio di Glibc 2.27, binutils 2.30, gcc 7 e il kernel Linux 4.15.
Informazioni sul test del microkernel seL4
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 dell'architettura hardware aperta RISC-V con il microkernel aperto seL4 consentirà di raggiungere un nuovo livello di sicurezza , poiché in futuro sarà possibile verificare completamente anche i componenti hardware, cosa impossibile da ottenere con architetture hardware proprietarie.
Quando controlliamo seL4, dobbiamo presumere che l'hardware funzioni correttamente (cioè come specificato). Ciò presuppone che ci sia una specifica inequivocabile in primo luogo, il che non è il caso di tutto l'hardware.
Ma anche quando una tale specifica esiste, ed è formale (cioè, scritta in un formalismo matematico che supporta il ragionamento matematico sulle sue proprietà ), come facciamo a sapere che cattura effettivamente il comportamento dell'hardware?
La realtà è che possiamo essere abbastanza sicuri che non lo sia. L'hardware non è diverso dal software in quanto entrambi sono difettosi.
Ma avere un ISA aperto ha vantaggi che vanno oltre l'essere esenti da royalty. Uno è che consente implementazioni hardware open source.
Durante il controllo di seL4, si presume che l'apparecchiatura funzioni come indicato e la specifica descriva completamente il comportamento del sistema, ma in realtà l'apparecchiatura non è esente da errori, il che è ben dimostrato dai problemi che si presentano regolarmente nel meccanismo di esecuzione speculativa Istruzioni .
Le piattaforme hardware aperte semplificano l'integrazione delle modifiche relative alla sicurezza, ad esempio per bloccare tutti i possibili canali di fuga di dati attraverso terze parti, laddove è molto più efficiente risolvere un problema tramite hardware piuttosto che cercare soluzioni tramite software.
Infine, se desiderate approfondire l'argomento, potete consultare l'articolo al seguente link.