RISC-V -säätiö ilmoitti tarkistaneensa miten mikrohiiri toimii seL4 järjestelmissä, joissa on käskyjoukon arkkitehtuuri RISC-V. Jossa todentamisprosessi supistuu matemaattiseksi todistukseksi seL4: n luotettavuudesta, mikä osoittaa, että virallisella kielellä määriteltyjen eritelmien on oltava täysin yhteensopivia.
Luotettavuustestaus mahdollistaa seL4: n käytön RISC-V-prosessoreihin perustuvissa kriittisissä järjestelmissä RV64, joka edellyttää korkeampaa luotettavuutta eikä takaa epäonnistumista.
SeL4-ytimen päällä toimivat ohjelmistokehittäjät voivat olla täysin varmoja siitä, että jos jossakin järjestelmän osassa tapahtuu vika, tämä vika ei leviä muualle järjestelmään ja erityisesti sen kriittisiin osiin.
Tietoja seL4: stä
SeL4-arkkitehtuuri on merkittävä osien poistamisella ydinresurssien hallitsemiseksi käyttäjäavaruudessa ja käytä samoja pääsynvalvontamenetelmiä sellaisille resursseille kuin käyttäjäresursseille.
Mikrotuuma ei tarjoa korkean tason abstraktioita valmiina hallitsemaan tiedostoja, prosesseja, verkkoyhteyksiä jne., mutta sen sijaan tarjoaa vain vähän mekanismeja fyysisen osoitetilan pääsyn hallitsemiseksi, keskeyttää ja prosessorin resurssit.
Korkean tason abstraktit ja ohjaimet tietokoneen kanssa tapahtuvaa vuorovaikutusta varten toteutetaan erikseen mikrokernelin päällä käyttäjän tasolla suoritettavina tehtävinä.
Tällaisten tehtävien pääsy mikrokodin käytettävissä oleviin resursseihin on järjestetty sääntöjen määrittelyn avulla.
RISC-V tarjoaa avoimen ja joustavan järjestelmän koneen ohjeista mahdollistaa mikroprosessoreiden luomisen mielivaltaisille sovelluksille ilman vähennyksiä ja asettamatta käyttöehtoja.
RISC-V: n avulla voit luoda täysin avoimia prosessoreita ja SoC: ita. Tällä hetkellä RISC-V-määrittelyn perusteella eri yritykset ja yhteisöt, jotka käyttävät erilaisia ​​ilmaisia ​​lisenssejä (BSD, MIT, Apache 2.0), kehittävät useita kymmeniä variantteja jo tuotetuista mikroprosessorisydämistä, SoC: ista ja siruista.
RISC-V-tuki on ollut käytössä Glibc 2.27-, binutils 2.30-, gcc 7- ja Linux 4.15 -ydinten julkaisemisesta lähtien.
Tietoja seL4-mikrotuen testauksesta
Aluksi mikrokerneli seL4 vahvistettiin 32-bittisille ARM-prosessoreilleJa myöhemmin 86-bittisille x64-prosessoreille.
On havaittu, että RISC-V: n avoimen laitteistoarkkitehtuurin yhdistelmä avoimen mikrohiiren kanssa seL4 saavuttaa uuden turvallisuustason, koska laitteistokomponentit voidaan tulevaisuudessa myös täysin tarkistaa, mikä on mahdotonta saavuttaa omistetuille laitteistoarkkitehtuureille.
Kun tarkistamme seL4: n, meidän on oletettava, että laitteisto toimii oikein (eli kuten määritelty). Tämä edellyttää, että ensinnäkin on yksiselitteinen eritelmä, mikä ei ole kaikkien laitteistojen tapaus.
Mutta vaikka tällainen eritelmä on olemassa ja se on muodollinen (eli matematiikan formalismi, joka tukee sen ominaisuuksien matemaattista päättelyä), mistä tiedämme, että se todella vangitsee laitteiston toiminnan?
Todellisuus on, että voimme olla melko varmoja, ettei se ole. Laitteisto ei eroa ohjelmistosta, koska molemmat ovat viallisia.
Mutta avoimella ISA: lla on etuja, jotka ylittävät rojaltivapauden. Yksi on se, että se sallii avoimen lähdekoodin laitteistototeutukset.
SeL4: n tarkistamisen yhteydessä oletetaan, että laite toimii ilmoitetulla tavalla ja spesifikaatio kuvaa täysin järjestelmän käyttäytymisen, mutta itse asiassa laite ei ole virheetön, mikä näkyy hyvin spekulatiivisessa toteutusmekanismissa säännöllisesti esiintyvissä ongelmissa. .
Avoin laitteistoalusta yksinkertaistaa muutosten integrointia liittyvät esimerkiksi suojaamaan kaikki mahdolliset vuotokanavat kolmansien osapuolten kanavien kautta, missä on paljon tehokkaampaa päästä eroon ongelmasta laitteistolla kuin yrittää löytää ratkaisuja ohjelmistokohtaisesti.
Lopuksi, jos haluat tietää enemmän siitä, voit tutustua muistiinpanoon seuraava linkki.