RISC-V säätiö mikroytimen toiminnan tarkistamisesta järjestelmissä, joissa on RISC-V-käskysarjaarkkitehtuuri. Vahvistus tulee seL4-toiminnan luotettavuus, mikä osoittaa täydellistä noudattamista virallisella kielellä määritettyjen määritelmien kanssa. Todiste luotettavuudesta seL4 kriittisissä RISC-V RV64 -prosessoreihin perustuvissa järjestelmissä, jotka vaativat parempaa luotettavuutta ja takaavat vikojen puuttumisen. SeL4-ytimen päällä toimivien ohjelmistojen kehittäjät voivat olla täysin varmoja siitä, että jos jossakin järjestelmän osassa on vika, tämä vika ei leviä muuhun järjestelmään ja erityisesti sen kriittisiin osiin.
SeL4-mikroydin vahvistettiin alun perin 32-bittisille ARM-prosessoreille ja myöhemmin 64-bittisille x86-prosessoreille. On huomattava, että avoimen RISC-V-laitteistoarkkitehtuurin ja avoimen seL4-mikroytimen yhdistäminen saavuttaa uuden turvallisuustason, koska laitteistokomponentit voidaan myös tulevaisuudessa täysin varmentaa, mikä on mahdotonta saavuttaa patentoiduilla laitteistoarkkitehtuureilla.
SeL4:n varmentamisessa oletetaan, että laite toimii ilmoitetulla tavalla ja spesifikaatio kuvaa täysin järjestelmän käyttäytymistä, mutta todellisuudessa laite ei ole virheetön, minkä osoittavat selvästi säännöllisesti ilmenevät ongelmat spekulatiivisen suoritusmekanismin mekanismissa. ohjeet. Avoimet laitealustat helpottavat tietoturvaan liittyvien muutosten integrointia - esimerkiksi kaikkien mahdollisten sivukanavavuotojen estämistä, jolloin on paljon tehokkaampaa päästä eroon laitteiston ongelmasta kuin yrittää löytää ratkaisuja ohjelmistosta.
Muista, että seL4-arkkitehtuuri siirtävät osia ydinresurssien hallitsemiseksi käyttäjätilaan ja samojen kulunvalvontavälineiden käyttämiseksi tällaisille resursseille kuin käyttäjäresursseille. 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.
RISC-V tarjoaa avoimen ja joustavan konekäskyjärjestelmän, joka mahdollistaa mikroprosessorien rakentamisen mielivaltaisiin sovelluksiin ilman, että käyttö edellyttää rojalteja tai merkkijonoja. RISC-V:n avulla voit luoda täysin avoimia SoC:ita ja prosessoreita. Perustuu tällä hetkellä eri yritysten ja yhteisöjen RISC-V-spesifikaatioihin useilla ilmaisilla lisensseillä (BSD, MIT, Apache 2.0) useita kymmeniä muunnelmia mikroprosessoriytimistä, SoC:ista ja jo tuotetuista siruista. RISC-V-tuki on ollut olemassa Glibc 2.27:n, binutils 2.30:n, gcc 7:n ja Linux-ytimen 4.15:n julkaisujen jälkeen.
Lähde: opennet.ru