Google-k KataOS proiektuarekin lotutako garapenak aurkitu dituela iragarri du, txertatutako hardwarerako sistema eragile seguru bat sortzea helburu duena. KataOS sistemaren osagaiak Rust-en idatzita daude eta seL4 mikrokernelaren gainean exekutatzen dira, eta horretarako fidagarritasunaren froga matematiko bat eman da RISC-V sistemetan, kodea hizkuntza formalean zehaztutako zehaztapenak guztiz betetzen dituela adieraziz. Proiektuaren kodea Apache 2.0 lizentziarekin irekita dago.
Sistemak RISC-V eta ARM64 arkitekturan oinarritutako plataformetarako laguntza eskaintzen du. Hardwarearen gainean seL4 eta KataOS ingurunearen funtzionamendua simulatzeko, Renode esparrua erabiltzen da garapen prozesuan. Sparrow hardware eta software konplexua, KataOS OpenTitan plataforman oinarritutako txip seguruekin konbinatuz, erreferentziazko inplementazio gisa proposatzen da. Proposatutako irtenbideak logikoki egiaztatutako sistema eragilearen nukleoa konbinatzeko aukera ematen du hardware osagai fidagarriak (RoT, Root of Trust), OpenTitan plataforma eta RISC-V arkitektura erabiliz eraikia. KataOS kodeaz gain, beste Sparrow osagai guztiak irekitzea aurreikusi da etorkizunean, hardware osagaia barne.
Plataforma garatzen ari da ikaskuntza automatikorako eta informazio konfidentziala prozesatzeko aplikazioak exekutatzeko diseinatutako txip espezializatuetan aplikatzeko, babes-maila berezia eta hutsegiterik ez dagoela ziurtatzeko. Aplikazio horien adibideen artean pertsonen irudiak eta ahots-grabaketak manipulatzen dituzten sistemak daude. KataOSek fidagarritasunaren egiaztapena erabiltzeak bermatzen du sistemaren zati batek huts egiten badu, hutsegitea ez dela sistemaren gainerakoetara hedatuko eta, bereziki, nukleoetara eta zati kritikoetara.
SeL4 arkitektura nabarmena da nukleoko baliabideak kudeatzeko piezak erabiltzaileen espaziora mugitzeagatik eta baliabideetarako sarbide-kontrolerako tresna berdinak aplikatzeagatik. Mikrokernelak ez du prestatutako goi-mailako abstrakziorik eskaintzen fitxategiak, prozesuak, sare-konexioak eta antzekoak kudeatzeko; horren ordez, helbide-espazio fisikorako, etenetarako eta prozesadore-baliabideetarako sarbidea kontrolatzeko mekanismo minimoak eskaintzen ditu. Hardwarearekin elkarreragiteko goi-mailako abstrakzioak eta kontrolatzaileak mikrokernelaren gainean bereizita inplementatzen dira erabiltzaile-mailako zereginen moduan. Mikrokernelak eskura dituen baliabideetara horrelako zereginen sarbidea arauen definizioaren bidez antolatzen da.
Babes gehigarrirako, mikrokernel-a izan ezik osagai guztiak natiboki garatzen dira Rust-en, programazio-teknika seguruak erabiliz, memoria-akatsak minimizatzen dituztenak, hala nola, askatu ondoren memoria sarbidea, erakusle nuluaren deserreferentziak eta buffer-a gainditzea. Rust-en seL4 inguruneko aplikazio-kargatzailea, sistema-zerbitzuak, aplikazioak garatzeko markoa, sistema-deiak sartzeko API bat, prozesu-kudeatzailea, memoria dinamikoa esleitzeko mekanismoa, etab. Egiaztatutako muntaiak seL4 proiektuak garatutako CAmkES tresna-tresna erabiltzen du. CAmkES-erako osagaiak Rust-en ere sor daitezke.
Rust-ek memoriaren segurtasuna betetzen du konpilazio garaian erreferentzia-egiaztapenaren, objektuen jabetzaren eta objektuen bizitzaren jarraipenaren bidez (esparruak), eta exekuzioan memoria-sarbideen zuzentasuna ebaluatuz. Rust-ek zenbaki osoen gainezkatzeen aurkako babesa eskaintzen du, erabili aurretik balio aldagaiak hasieratu behar dira, erreferentzia eta aldagai aldaezinen kontzeptua erabiltzen du lehenespenez eta idazketa estatiko sendoa eskaintzen du akats logikoak minimizatzeko.
Iturria: opennet.ru