U prughjettu di u microkernel apertu seL4 hà ricevutu u ACM Software System Award, un premiu annuale datu da l'Associazione per Computing Machinery (ACM), l'urganisazione internaziunale più rispettata in u campu di i sistemi di computer. U premiu hè datu per i successi in u campu di a prova matematica di u funziunamentu, chì indica u cumpletu cumpletu cù e specificazioni date in una lingua formale è ricunnosce a prontezza per l'usu in applicazioni critiche di missione. U prughjettu seL4 hà dimustratu chì ùn hè micca solu pussibule di verificà in modu cumpletu l'affidabilità è a sicurità per i prughjetti à u livellu di i sistemi operativi industriali, ma ancu per ottene questu senza sacrificà u rendiment è a versatilità.
U Premiu ACM Software System Award hè presentatu annu per ricunnosce u sviluppu di sistemi di software chì anu avutu un impattu definitu in l'industria, introducendu novi cuncetti o aprendu novi applicazioni cummerciale. A quantità di u premiu hè di 35 mila dollari americani. In l'ultimi anni, i premii ACM sò stati dati à i prughjetti GCC è LLVM, è i so fundatori Richard Stallman è Chris Latner. U premiu hè statu ancu datu à prughjetti è tecnulugia cum'è UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl / Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB è Eclipse.
L'architettura di u microkernel seL4 hè notevule per a rimuzione di parti per a gestione di risorse di u kernel in u spaziu di l'utilizatori è per applicà i stessi mezi di cuntrollu d'accessu per tali risorse cum'è per i risorse di l'utilizatori. U microkernel ùn furnisce micca astrazioni d'altu livellu fora di a scatula per a gestione di fugliali, prucessi, cunnessione di rete, è simili, invece furnisce solu miccanismi minimi per cuntrullà l'accessu à u spaziu di l'indirizzu fisicu, interruzioni è risorse di processore. L'astrazioni d'altu livellu è i driver per l'interazzione cù u hardware sò implementati separatamente nantu à u microkernel in forma di attività à livellu d'utilizatore. L'accessu di tali compiti à e risorse dispunibuli à u microkernel hè urganizatu per mezu di a definizione di regule.
Source: opennet.ru