RISC-V Fondi Organisatsioon mikrojaotuse verifikatsioonist RISC-V käskude komplekti arhitektuuriga süsteemides. Verifikatsioon piirdub seL4 töökindluse kohta, mis tõendab täielikku vastavust vormingus spetsifikatsioonidele. Töökindluse tõestamine seL4 RISC-V RV64 protsessorite baasil olulistes süsteemides, mis nõuavad kõrget töökindlust ja tagavad tõrgete puudumise. seL4 tuuma peal töötavate tarkvarade arendajad võivad olla täiesti kindlad, et kui ühe osa süsteemist tekib tõrge, ei levi see ülejäänud süsteemi, sealhulgas selle kriitilistesse osadesse.
Alguses oli mikrokiip seL4 verifitseeritud 32-bitiste ARM-protsessorite jaoks ja hiljem 64-bitiste x86-protsessorite jaoks. Tulemuseks on see, et avatud RISC-V riistvara arhitektuuri ja avatud mikrokiibi seL4 kombinatsioon võimaldab saavutada uue taseme turvalisust, kuna tulevikus on võimalik täielikult verifitseerida ka riistvaralisi komponente, mida ei saa saavutada erakontrolli all olevate riistvara arhitektuuride puhul.
seL4 verifitseerimisel oletatakse, et riistvara töötab nagu lubatud ja spetsifikatsioon kirjeldab süsteemi käitumist täielikult, kuid tegelikkuses ei ole riistvara vigadest vaba, mida näitavad regulaarselt esinevad probleemid spetsiifiliste täitmisjuhiste mehanismides. Avatud riistvaraalused platvormid lihtsustavad turvalisust muudetud integreerimist — näiteks kõigi võimalike kanali lekete peatamist, kus on tõhusam probleem lahendada riistvaraliselt kui proovida otsida tarkvaraliselt võimalusi.
Tuletame meelde, et seL4 arhitektuur tuumade eraldamine mikrokernelis, et hallata ressursse kasutajatasemel ja rakendada sellistele ressurssidele samu juurdepääsukontrolli meetodeid nagu kasutajaressurssidele. Mikrokernel ei paku valmis kõrgtaseme abstraktsioone failide, protsesside, võrguside jne haldamiseks. Selle asemel annab see vaid minimaalsed mehhanismid füüsilise aadressiruumi, katkemiste ja protsessori ressursside haldamiseks. Kõrgtaseme abstraktsioonid ja draiverid riistvaraga suhtlemiseks rakendatakse eraldi mikrokernelitest, kasutajatase ülesande vormis. Selliste ülesannete juurdepääs mikrokernelis olevatele ressurssidele korraldatakse reeglite määramise kaudu.
RISC-V pakub avatud ja paindlikku masinakeelte süsteemi, mis võimaldab luua mikropersetoreid igasuguste rakenduste jaoks, ilma litsentsitasudeta ja kasutustingimusteta. RISC-V võimaldab luua täielikult avatud SoC ja protsessoreid. Praegu on RISC-V spetsifikatsiooni alusel erinevad ettevõtted ja kogukonnad välja töötanud mitmesuguseid avatud litsentse (BSD, MIT, Apache 2.0). mitmeid tosinad mikropersetoreid, SoC ja juba tootmisse läinud kiipe. RISC-V tugi on olemas alates Glibc 2.27, binutils 2.30, gcc 7 ja Linuxi tuuma 4.15 väljalasetest.
Allikas: opennet.ru
