seL4 nejbezpečnější mikrojádro dneška?

Včera | 08:20 | novomente | Michal Petrenka

Google AI mi řekla, že mikrojádro operačního systému seL4 je do dnešního dne nepřekonané v bezpečnosti. Zajímalo by mě, zdali jste ho někdo zkoušel přímo na hardwaru (na železe) a zdali se někde ve východní Evropě snaží o jeho překonání.

seL4 (security enhanced L4) je svobodné jádro operačního systému, přesněji mikrojádro třetí generace, zaměřené na vysokou bezpečnost a spolehlivost...

...seL4 je vyvíjen se zvláštním přihlédnutím k otázkám bezpečnosti a formální bezchybnosti mikrojádra organizací NICTA a dalšími vývojáři. Právě kvůli těmto vlastnostem byl vytvořen vývojový model, který umožňuje ověřit zdrojový kód seL4 ve funkcionálním jazyce Haskell pomocí formálních (matematických) důkazů...

více na české wikipedii