Työ seL4-mikroytimen luotettavuuden ja turvallisuuden muodollisen matemaattisen verifioinnin parissa AArch64-käskykanta-arkkitehtuuria käyttävissä järjestelmissä on saatu päätökseen. Verifikaatio koostuu matemaattisesta todistuksesta seL4:n toiminnan oikeellisuudesta, joka osoittaa täyden yhteensopivuuden muodollisessa kielessä määriteltyjen spesifikaatioiden kanssa. Tämä luotettavuuden todistus mahdollistaa seL4:n käytön ARM64-prosessoreihin perustuvissa kriittisissä järjestelmissä, jotka vaativat korkeaa turvallisuustasoa ja takaavat virheiden puuttumisen.
seL4-mikroydin varmennettiin alun perin 32-bittisille ARM-prosessoreille ja myöhemmin 64-bittisille x86- ja RISC-V-prosessoreille. Varmennus varmistaa, että jos järjestelmän yhdessä osassa ilmenee vika, se ei leviä muuhun järjestelmään ja sen kriittisiin komponentteihin. Tietoturvan yhteydessä varmennus varmistaa, että ydin tarjoaa asianmukaisen sovellusten eristämisen tason, estää niitä pääsemästä tietoihin luvattomasti ja varmistaa, että jos toissijaiset sovellukset vaarantuvat, hyökkäys ei leviä kriittisiin sovelluksiin.
Mikroytimen seL4:n arkkitehtuuri on huomionarvoinen osien poistamisesta ytimen resurssien hallintaa varten käyttäjätilassa ja samojen pääsynvalvontamenetelmien 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 käytön hallitsemiseksi. 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.
Lähde: opennet.ru
