Il lavoro sulla verifica formale matematica della robustezza e della sicurezza del funzionamento del microkernel seL4 su sistemi con architettura del set di istruzioni AArch64 è stato completato. La verifica consiste nella dimostrazione matematica della correttezza del funzionamento di seL4, che attesta la piena conformità alle specifiche stabilite in linguaggio formale. La dimostrazione di robustezza consente di utilizzare seL4 in sistemi critici basati su processori ARM64, che richiedono un livello elevato di sicurezza e garantiscono l'assenza di guasti.
Inizialmente, il microkernel seL4 è stato verificato per processori ARM a 32 bit, e in seguito per processori a 64 bit x86 e RISC-V. La verifica garantisce che, in caso di guasto in una parte del sistema, tale guasto non si propagherà al resto del sistema e alle sue parti critiche. Nel contesto della sicurezza, la verifica conferma che il nucleo fornisce un adeguato livello di isolamento delle applicazioni, impedendo loro di accedere alle informazioni senza autorizzazione e garantendo che, in caso di compromissione delle applicazioni secondarie, l'attacco non si propaghi alle applicazioni critiche.
L'architettura del microkernel seL4 è notevole per il trasferimento di parti per la gestione delle risorse del nucleo nello spazio utente e per l'applicazione delle stesse modalità di controllo degli accessi per tali risorse come per le risorse utente. Il microkernel non fornisce astrattezze ad alto livello pronte per la gestione di file, processi, connessioni di rete, ecc., ma offre solo meccanismi minimi per gestire l'accesso allo spazio indirizzi fisici, alle interruzioni e alle risorse del processore. Le astrattezze ad 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 del microkernel è organizzato attraverso la definizione di regole.
Fonte: opennet.ru
