Il progetto che sviluppa il microkernel open source seL4 ha ricevuto il premio ACM Software System Award, assegnato annualmente dall'Associazione per l'Informativa Computazionale (ACM), l'organizzazione internazionale più autorevole nel campo dei sistemi informatici. Il premio è stato conferito per i risultati ottenuti nella dimostrazione matematica della affidabilità operativa, che attesta la completa conformità alle specifiche definite in linguaggio formale e riconosce la prontezza all'uso in applicazioni critiche. Il progetto seL4 ha dimostrato che è possibile effettuare una verifica formale completa di affidabilità e sicurezza per progetti di livello sistemi operativi industriali, ottenendo questo senza compromettere le prestazioni e la versatilità.
Il premio ACM Software System Award viene assegnato ogni anno per lo sviluppo di sistemi software che hanno avuto un impatto significativo nel settore, introducendo nuove concetti o rivelando nuove aree di applicazione commerciale. L'ammontare del premio è di 35.000 dollari statunitensi. 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 l'allocazione delle parti di gestione delle risorse del kernel nello spazio utente, utilizzando gli stessi strumenti di separazione degli accessi per tali risorse come per le risorse utente. Il microkernel non offre astrazioni di alto livello pronte per la gestione di file, processi, connessioni di rete, ecc.; al contrario, fornisce solo meccanismi minimi per la gestione dell'accesso allo spazio di indirizzamento 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 in forma di task eseguiti a livello utente. L'accesso di tali task alle risorse disponibili del microkernel è organizzato attraverso la definizione di regole.
Fonte: opennet.ru
