Egy ausztrál tervezésű mikrokernelt bocsátottak ki, amely garantálja a szoftver biztonságot.
Titka a formális metódusok matematikai tétele, amely megbizonyosodik arról, hogy a SeL4 mikrokernel mindig pontosan úgy települ, ahogyan azt specifikálták. Az elképzelést a Carnegie Mellon University definiálta, mint egy technikát, amelynek segítségével komplex rendszerek matematikai entitásként kezelhetők. Mindez lehetővé teszi, hogy egy rendszer tulajdonságainak ellenőrzése sokkal mélyrehatóbb módon történjék, mint az empirikus tesztelés során.
A mikrokernel létrehozása egy lendületes csapást mér a világ vezető operációs rendszereire (Microsoft Windows, Linux, Apple), amelyet a SeL4 vezető tervezője, Dr. Gerwin Klein a következőképpen látja.
“Mindenütt észlelhető, a magas szintű Linuxtól a Windowsig, teljesen egyformák — valamilyen téren túl nagyra nőttek”.
“Elfelejtették, hogy milyen célt szolgáltak az operációs rendszerek; hátrahagyták a múltjukat.”
http://www.zdnet.com.au/aussie-microkernel-sets-security-in-stone-339308818.htm
http://ertos.nicta.com.au/software/seL4/home.pyl