Jádro systému obsahuje pouze nezbytné minimum kódu (7 500 řádek) pro kontakt mezi hardwarem a aplikacemi. Dosavadní pokusy v tomto směru přinesly pouze jádra omezená na několik typů systémů nebo jednoúčelové počítače, nově vyvinutý kernel by však měl být univerzální.
Gerwin Klein ze společnosti Nicta tvrdí, že se mu bezpečnost kódu jádra podařilo dokázat rigorózně matematicky – v tom smyslu, že by kód vždy provádí pouze to, co zamýšleli jeho autoři. Metoda důkazu bezpečnosti je možná ještě důležitější než vlastní systém, mohla by totiž být použita i pro analýzu jádra současných operačních systémů (jejich budoucích verzí) a sloužit jako osvědčení (formální verifikace) všude tam, kde se na zabezpečení klade zvláštní důraz.
V rámci německého vládního projektu Verisoft byl už v roce 2006 vyvinut první bezpečný mikrokernel, pro praktické nasazení byl však příliš pomalý. Nicta se naopak snaží, aby její projekt neměl jen akademický/teoretický význam.
Zdroj: New Scientist
PŘEDPLATNÉ
ČLÁNKY DO MAILU