Google on ilmoittanut löytäneensä KataOS-projektiin liittyvää kehitystä, jonka tarkoituksena on luoda turvallinen käyttöjärjestelmä sulautetuille laitteille. KataOS-järjestelmän komponentit on kirjoitettu rust-kielellä ja ajetaan seL4-mikroytimen päällä, jonka luotettavuudesta on matemaattinen todiste RISC-V-järjestelmissä, mikä osoittaa, että koodi on täysin muodollisen kielen spesifikaatioiden mukainen. Projektikoodi on avoinna Apache 2.0 -lisenssillä.
Järjestelmä tukee RISC-V- ja ARM64-arkkitehtuureihin perustuvia alustoja. SeL4:n ja KataOS-ympäristön toiminnan simuloimiseksi laitteiston päällä käytetään Renode-kehystä kehitysprosessin aikana. Referenssitoteutuksena ehdotetaan Sparrow-ohjelmisto- ja laitteistokompleksia, joka yhdistää KataOS:n OpenTitan-alustaan perustuviin suojattuihin siruihin. Ehdotettu ratkaisu mahdollistaa loogisesti varmennetun käyttöjärjestelmän ytimen yhdistämisen luotettaviin laitteistokomponentteihin (RoT, Root of Trust), jotka on rakennettu käyttäen OpenTitan-alustaa ja RISC-V-arkkitehtuuria. KataOS-koodin lisäksi on tarkoitus avata tulevaisuudessa kaikki muut Sparrow-komponentit, mukaan lukien laitteistokomponentti.
Alustaa kehitetään silmällä sovellukseen erikoistuneissa siruissa, jotka on suunniteltu suorittamaan koneoppimiseen ja luottamuksellisten tietojen käsittelyyn tarkoitettuja sovelluksia, jotka edellyttävät erityistä suojaustasoa ja vahvistusta virheiden puuttumisesta. Esimerkkejä tällaisista sovelluksista ovat järjestelmät, jotka käsittelevät ihmisten kuvia ja äänitallenteita. KataOS:n luotettavuusvarmennus varmistaa, että jos jokin järjestelmän osa epäonnistuu, vika ei leviä muuhun järjestelmään ja etenkään ytimeen ja kriittisiin osiin.
SeL4-arkkitehtuuri on huomionarvoinen osien siirtämisessä ytimen resurssien hallintaan käyttäjätilaan ja samojen kulunvalvontatyökalujen soveltamisesta tällaisiin resursseihin kuin käyttäjäresursseihin. Mikroydin ei tarjoa valmiita korkean tason abstraktioita tiedostojen, prosessien, verkkoyhteyksien ja vastaavien hallintaan, vaan se tarjoaa vain minimaalisia mekanismeja fyysisen osoiteavaruuden, keskeytysten ja prosessoriresurssien hallintaan. Korkean tason abstraktiot ja ajurit laitteiston kanssa vuorovaikutusta varten toteutetaan erikseen mikroytimen päälle käyttäjätason tehtävien muodossa. Tällaisten tehtävien pääsy mikroytimen käytettävissä oleviin resursseihin on järjestetty sääntöjen määrittelyn kautta.
Lisäsuojauksen vuoksi kaikki komponentit paitsi mikroydin on kehitetty natiivisti Rustissa käyttämällä turvallisia ohjelmointitekniikoita, jotka minimoivat muistivirheet, jotka johtavat ongelmiin, kuten muistin käyttöön vapautumisen jälkeen, nollaosoittimen viittauksiin ja puskurin ylityksiin. Rustissa kirjoitettiin sovelluslataaja seL4-ympäristössä, järjestelmäpalvelut, sovelluskehityksen viitekehys, API järjestelmäkutsuihin pääsyä varten, prosessinhallinta, mekanismi dynaamiseen muistin varaamiseen jne. Tarkistettu kokoonpano käyttää seL4-projektin kehittämää CAmkES-työkalupakkia. CamkES-komponentteja voidaan luoda myös Rustissa.
Rust varmistaa muistin turvallisuuden käännöshetkellä viitteiden tarkistuksen, objektin omistajuuden ja objektin eliniän seurannan (scopes) avulla sekä arvioimalla muistin käytön oikeellisuutta ajon aikana. Rust tarjoaa myös suojan kokonaislukujen ylivuodoilta, vaatii muuttujien arvojen alustamisen ennen käyttöä, käyttää oletuksena muuttumattomien viittausten ja muuttujien käsitettä ja tarjoaa vahvan staattisen kirjoituksen minimoimaan loogiset virheet.
Lähde: opennet.ru