Projekt vyvíjející otevřené mikrojádro seL4 získal cenu ACM Software System Award, kterou každoročně uděluje Asociace výpočetní techniky (ACM), nejuznávanější mezinárodní organizace v oblasti počítačových systémů. Cena byla udělena za úspěchy v oblasti matematického důkazu spolehlivosti, který potvrzuje plnou shodu se specifikacemi stanovenými v formálním jazyce a uznává připravenost k využití v kriticky důležitých aplikacích. Projekt seL4 ukázal, že je možné nejen plně provést formální verifikaci spolehlivosti a bezpečnosti pro projekty úrovně průmyslových operačních systémů, ale také dosáhnout toho bez ztráty výkonu a versatility.
Cena ACM Software System Award se každoročně uděluje za vývoj softwarových systémů, které měly zásadní vliv na odvětví, přinesly nové koncepty nebo odhalily nové oblasti komerčního využití. Výše ceny je 35 tisíc dolarů USA. V minulých letech byly ceny ACM uděleny projektům GCC a LLVM, a jejich zakladatelům Richardu Stallmanovi a Chrisu Latnerovi. Cenu také získaly projekty a technologie, jako jsou UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB a Eclipse.
Architektura mikrojádra seL4 je pozoruhodná tím, že odděluje části pro správu prostředků jádra do prostoru uživatele a aplikuje na tyto prostředky stejná přístupová omezení jako na uživatelské prostředky. Mikrojádro neposkytuje hotové vysoceúrovňové abstrakce pro správu souborů, procesů, síťových připojení atd., místo toho poskytuje pouze minimální mechanismy pro správu přístupu k fyzickému adresnímu prostoru, přerušením a prostředkům procesoru. Vysoceúrovňové abstrakce a ovladače pro interakci s hardwarem jsou implementovány samostatně nad mikrojádrém ve formě úloh prováděných na uživatelské úrovni. Přístup těchto úloh k prostředkům, které má mikrojádro k dispozici, je organizován prostřednictvím stanovení pravidel.
Zdroj: opennet.ru
