Il progetto seL4 open microkernel ha ricevuto l'ACM Software System Award, un premio annuale assegnato dall'Association for Computing Machinery (ACM), l'organizzazione internazionale più rispettata nel campo dei sistemi informatici. Il premio viene assegnato per i risultati nel campo della prova matematica di funzionamento, che indica la piena conformità alle specifiche fornite in un linguaggio formale e riconosce la prontezza per l'uso in applicazioni mission-critical. Il progetto seL4 ha dimostrato che non solo è possibile verificare completamente formalmente l'affidabilità e la sicurezza dei progetti a livello di sistemi operativi industriali, ma anche ottenere ciò senza sacrificare prestazioni e versatilità.
L'ACM Software System Award viene assegnato ogni anno per riconoscere lo sviluppo di sistemi software che hanno avuto un impatto decisivo sul settore, introducendo nuovi concetti o aprendo nuove applicazioni commerciali. L'importo del premio è di 35 mila dollari USA. Negli anni passati, i premi ACM sono stati assegnati ai progetti GCC e LLVM e ai loro fondatori Richard Stallman e Chris Latner. Altri progetti e tecnologie premiati sono stati 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 si distingue per la rimozione di parti per la gestione delle risorse del kernel nello spazio utente e per l'applicazione degli stessi mezzi di controllo degli accessi per tali risorse come per le risorse utente. Il microkernel non fornisce astrazioni di alto livello pronte all'uso per la gestione di file, processi, connessioni di rete e simili, ma fornisce solo meccanismi minimi per controllare l'accesso allo spazio degli indirizzi fisici, agli interrupt e alle risorse del processore. Astrazioni e driver di alto livello per l'interazione con l'hardware sono implementati separatamente sopra il microkernel sotto forma di attività a livello di utente. L'accesso di tali task alle risorse a disposizione del microkernel è organizzato attraverso la definizione di regole.
Fonte: opennet.ru