Google'i ettevõte kuulutas välja projekti KataOS, mis on suunatud turvalise operatsioonisüsteemi loomisele sisseehitatud seadmete jaoks. KataOS-i süsteemi komponente on kirjutatud Rust keeles ja need töötavad mikrokern seL4 peal, millele on RISC-V süsteemides esitatud matemaatiline tõend usaldusväärsusest, mis tõendab, et kood vastab spetsifikatsioonidele, mis on määratletud formaalses keeles. Projekti kood on avatud Apache 2.0 litsentsi all.
Süsteem toetab RISC-V ja ARM64 arhitektuuride põhiseid plaate. SeL4 ja KataOS-i keskkonna simuleerimiseks seadmele arendusprotsessis kasutatakse Renode raamistikku. Etalonrealiseerimiseks on pakutud tarkvara-riistvara kompleksi Sparrow, mis ühendab KataOS-i OpenTitani platvormi põhiste turvaliste kiipidega. Pakutud lahendus võimaldab ühendada loogiliselt kontrollitud operatsioonisüsteemi tuuma usaldusväärsete riistvarakomponentidega (RoT, Root of Trust), mis on loodud OpenTitani platvormi ja RISC-V arhitektuuri abil. Peale KataOS-i koodi on tulevikus plaanis avada ka kõik ülejäänud Sparrowi komponendid, sealhulgas riistvara.
Platvorm areneb silmas pidades spetsialiseeritud kiipide kasutamist, mis on mõeldud masinõppe ja konfidentsiaalse teabe töötlemiseks, mille puhul on nõutud eriline kaitse ja veatu tõendamine. Näideteks sellistest rakendustest on süsteemid, mis töötlevad inimeste pilte ja häält. KataOS-is usaldusväärsuse kontrollimise kasutamine tagab, et kui ühes süsteemi osas esineb rike, ei laiene see rike ülejäänud süsteemile, sealhulgas tuumale ja kriitilistele osadele.
seL4 arhitektuur on märkimisväärne, kuna see eristab täiendavaid komponente mäluhalduse jaoks kernelist kasutajaruumi ning rakendab nende ressursside jaoks samu juurdepääsukontrolli meetodeid nagu kasutajate ressursse. Mikrokernel ei paku valmis kõrgetasemelisi abstraktsioone failide, protsesside, võrguühenduste jne haldamiseks; selle asemel pakub see vaid minimaalset mehhanismi füüsilise aadressiruumi, katkestuste ja protsessori ressursside juurdepääsu haldamiseks. Kõrgetasemelised abstraktsioonid ja seadme draiverid luuakse eraldi mikrokernele toetudes kasutajatase ülesannete vormis. Selliste ülesannete juurdepääs mikrokernele kergesti saatmiseks korraldatakse reeglite määratlemise kaudu.
Lisakaitseks arendatakse kõik komponendid, välja arvatud mikrokernel, algselt Rusti keeles, kasutades turvalisi programmeerimistehnikaid, mis vähendavad mäluhaldusega seotud vigu, nagu näiteks mälu vabastamise järel sellele juurde pääsemine, nullviidete de-referentseerimine ja mälubufferi ületamine. Rusti keeles on kirjutatud ka seL4 keskkonnas rakenduste laadija, süsteemiteenused, rakenduste arendamise raamistik, API süsteemikõnedele juurdepääsuks, protsessihaldur, dünaamilise mälja jagamise mehhanism jne. Verifitseeritud koostamiseks kasutatakse CAmkES tööriistu, mida arendab seL4 projekt. CAmkES komponentide loomine on samuti võimalik Rusti keeles.
Rust tagab mälu turvalise käsitlemise kompileerimise ajal viidete kontrolli, objektide omandi jälgimise ja objektide eluea (nähtavuse) arvestamise kaudu, samuti mälu juurdepääsu õigsuse hindamise ajal koodi käitamise ajal. Rust pakub ka vahendeid täisarvude ületäitumise kaitsmiseks, nõuab muutuja väärtuste kohustuslikku initsialiseerimist enne nende kasutamist, rakendab vaikimisi muutumatute (immutable) viidete ja muutujate kontseptsiooni ning pakub tugevat staatilist tüüpimist, et minimeerida loogilisi vigu.
Allikas: opennet.ru
