Il progetto che sviluppa il microkernel open source seL4 ha ricevuto il premio ACM Software System Award, assegnato annualmente dall'Associazione per la Computazione (ACM), l'organizzazione internazionale più autorevole nel campo dei sistemi informatici. Il premio è stato conferito per i risultati ottenuti nella dimostrazione matematica dell'affidabilità operativa, che testimonia la piena conformità alle specifiche scritte in un linguaggio formale e riconosce la prontezza all'uso in applicazioni critiche. Il progetto seL4 ha dimostrato che è possibile eseguire una verifica formale completa dell'affidabilità e della sicurezza per progetti a livello di sistemi operativi industriali, senza compromettere le prestazioni e l'universalità.
Il premio ACM Software System Award viene assegnato annualmente per lo sviluppo di sistemi software che hanno avuto un impatto decisivo nel settore, introducendo nuove concetti o rivelando nuove aree di applicazione commerciale. L'importo del premio è di 35.000 dollari americani. Negli anni passati, i premi ACM sono stati conferiti ai progetti GCC e LLVM e ai loro fondatori Richard Stallman e Chris Lattner. Il premio ha inoltre riconosciuto progetti e tecnologie come UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB ed Eclipse.
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
