Fond RISC-V teatas, et on kontrollinud kuidas mikrotuum töötab seL4 süsteemidega käskude arhitektuuri RISC-V. Kui taandamisprotsess on taandatud seL4 usaldusväärsuse matemaatiliseks tõendiks, mis näitab täielikku vastavust ametlikus keeles täpsustatud spetsifikatsioonidele.
Usaldusväärsuse testimine võimaldab seL4 kasutada missioonikriitilistes süsteemides, mis põhinevad RISC-V protsessoritel RV64, mis nõuab kõrgemat usaldusväärsust ja ei taga ebaõnnestumist.
SeL4 kerneli peal töötavad tarkvaraarendajad võivad olla täiesti kindlad, et süsteemi ühe osa rikke korral ei levi see rike ülejäänud süsteemi ja eriti selle kriitilistesse osadesse.
SeL4 kohta
SeL4 arhitektuur on märkimisväärne osade eemaldamise abil tuumaressursside haldamiseks kasutajaruumis ja kasutage selliste ressursside jaoks samu juurdepääsu kontrollimeetodeid kui kasutaja ressursside puhul.
Mikrotuum ei paku kõrgetasemelisi abstraktsioone on juba valmis faile, protsesse, võrguühendusi jne haldama, kuid selle asemel pakub ainult minimaalseid mehhanisme, et kontrollida juurdepääsu füüsilisele aadressiruumile, katkestab ja töötleb ressursse.
Kõrgetasemelised abstraktsioonid ja draiverid arvutiga suhtlemiseks rakendatakse mikrotasandi peal eraldi kasutaja tasemel tehtavate ülesannete kujul.
Selliste ülesannete juurdepääs mikrotuuma ressurssidele on korraldatud reeglite määratlemise kaudu.
RISC-V pakub avatud ja paindlikku süsteemi masina juhiseid võimaldab luua meelevaldsete rakenduste jaoks mikroprotsessoreid ilma mahaarvamisi nõudmata ja kasutustingimusi kehtestamata.
RISC-V võimaldab teil luua täiesti avatud protsessoreid ja SoC-sid. Praegu töötavad mitmed erinevate tasuta litsentside (BSD, MIT, Apache 2.0) ettevõtted ja kogukonnad RISC-V spetsifikatsiooni alusel välja mitukümmend juba toodetud mikroprotsessorituuma, SoC-i ja kiibi varianti.
RISC-V tugi on olnud olemas alates Glibc 2.27, binutils 2.30, gcc 7 ja Linux 4.15 kerneli väljaandmisest.
SeL4 mikrotuumade testimise kohta
Esialgu mikrotuum seL4 kontrolliti 32-bitiste ARM-protsessorite jaoks, Ja hiljem x86 64-bitiste protsessorite jaoks.
Täheldatakse, et RISC-V avatud riistvara arhitektuuri ja avatud mikrotuuma kombinatsioon seL4 saavutab uue turvalisuse taseme, kuna ka tulevasi riistvarakomponente saab täielikult kontrollida, mida on võimatu omandis olevate riistvaraarhitektuuride puhul saavutada.
SeL4 kontrollimisel peame eeldama, et riistvara töötab korralikult (see tähendab, nagu täpsustatud). See eeldab, et esiteks on üheselt mõistetav spetsifikatsioon, mis ei kehti kogu riistvara puhul.
Kuid isegi kui selline spetsifikatsioon on olemas ja see on formaalne (st matemaatilises formalismis, mis toetab selle omaduste matemaatilist põhjendamist), kuidas me teame, et see haarab tegelikult riistvara käitumist?
Reaalsus on see, et võime olla üsna kindlad, et see pole nii. Riistvara ei erine tarkvarast selle poolest, et mõlemad on lollakad.
Kuid avatud ISA omamisel on eeliseid, mis lähevad kaugemale autoritasuta olemisest. Üks on see, et see võimaldab avatud lähtekoodiga riistvara juurutamist.
SeL4 kontrollimisel eeldatakse, et seadmed töötavad nii, nagu on näidatud, ja spetsifikatsioon kirjeldab süsteemi käitumist täielikult, kuid tegelikult pole seade vigadeta, mida näitavad hästi probleemid, mis regulaarselt tekivad spekulatiivses täitemehhanismis. .
Avatud riistvara platvormid lihtsustavad muudatuste integreerimist turvalisusega seotud, näiteks kõigi võimalike lekkekanalite blokeerimine kolmandate osapoolte kanalite kaudu, kus on palju tõhusam probleemist riistvara abil lahti saada kui proovida lahendusi leida tarkvara järgi.
Lõpuks, kui soovite selle kohta rohkem teada saada, saate tutvuda märkuses järgmine link.