Hibátlan operációs rendszeren dolgoznak

A NICTA technológiai kutatócég, az ausztráliai Új Dél-Wales Egyetem, és az Open Kernel Labs pont ezen dolgozik. Az seL4 nevű kernel fejlesztésénél az volt a céljuk, hogy a kód feladatait minimalizálják, és az alkalmazások futtatását lehetővé tegyék a hardveren. Korábban a hasonló célokat kitűző projektekkel az volt a probléma, hogy a vírusok elleni immunitás miatt, feláldozták a funkciók nagy részét, és csak kevés fajta feladatot tudott ellátni a gép.

A kernel kódjának biztonságosságát Gerwin Klein a NICTA-tól, és csapata bizonyította. A 7500 sornyi kódot matematikai módon bizonyította. “Végső soron a programírás is csak matematika, ezért matematikailag bizonyíthatóak” – mondta el Klein. Felállítottak egy modellt, amiben 200 ezer logikai lépésen keresztül bebizonyították, hogy a program működése mindig az alkotók szándéka szerint fog működni. A kernel potenciálisan kiterjeszthető lesz komplexebb rendszerré, amire már teljes operációs rendszerek épülhetnek.

Tom In Der Rieden, a német kormányzat Verisoft projektjének vezetője elmondta, hogy a formális verifikáció egyre nagyobb népszerűségre tesz szert a szoftvertervezés során. “Ez a végső eszköz a bizonyításra” – mondta el Rieden. A Verisoft egy hasonló projekten dolgozott 2006-ban, de csak tudományos célokkal, írta meg a New Scientist.