RISC-V Foundationi organisatsioon mikrojaotuse töö verifitseerimisest RISC-V käsu komplekti arhitektuuril. Verifitseerimine seisneb seL4 töö usaldusväärsuse kohta, mis näitab täielikku vastavust ametlikul keelel formuleeritud spetsifikatsioonidele. Usaldusväärsuse tõendamine seL4 RISC-V RV64 protsessorite baasil asuvates kriitilistes süsteemides, mis nõuavad kõrget usaldusväärsust ja garanteerivad tõrgete puudumise. Tarkvaraarendajad, kes töötavad seL4 tuuma kohal, võivad olla täiesti kindlad, et kui üks osa süsteemist ebaõnnestub, siis see ebaõnnestumine ei leki ülejäänud süsteemi, sealhulgas selle kriitilistesse osadesse.
Alguses oli mikrojaot seL4 verifitseeritud 32-bitiste ARM protsessorite jaoks ning hiljem 64-bitiste x86 protsessorite jaoks. Täheldatakse, et avatud RISC-V arhitektuuri ja avatud mikrojaot seL4 kombinatsioon võimaldab saavutada uue turvalisuse taseme, kuna riistvara koostisosad võivad tulevikus samuti täielikult kinnitatud olla, mis ei ole võimalik patenteeritud riistvaraarhitektuuride puhul.
seL4 verifitseerimise raames eeldatakse, et riistvara töötab nagu deklareeritud ja spetsifikatsioon kirjeldab süsteemi käitumist täielikult, kuid tegelikkuses ei ole riistvara vigadest vaba, mida demonstreerivad regulaarselt esinevad probleemid spekulatiivsete käskude täitmise mehhanismis. Avatud riistvaraplatvormid lihtsustavad turvalisuse muutustega seotud muudatuste integreerimist — näiteks, et blokeerida kõik võimalikud lekete kanalid kolmandate osapoolte kaudu, kus on palju tõhusam probleem riistvaralise lahendusega kõrvaldada kui proovida leida tarkvaralisi ringteid.
Tuletame meelde, et seL4 arhitektuur kernelite ressursside haldamise osade viimine kasutajara, kasutades sama juurdepääsukontrolli vahendeid nagu kasutajate ressursside jaoks. Mikroüdamik ei paku valmis kõrgetasemelisi abstraktsioone failide, protsesside, võrguühenduste jne haldamiseks; selle asemel pakub see ainult minimaalset mehhanismi füüsilise aadressiruumi, katkestuste ja protsessori ressursside haldamiseks. Kõrgetasemelised abstraktsioonid ja seadme draiverid rakendatakse eraldi mikroüdamiku peal ülesanne kujul, mis toimub kasutajatasemel. Selliste ülesannete juurdepääs mikroüdamiku ressurssidele korraldatakse reeglite määratlemise kaudu.
RISC-V pakub avatud ja paindlikku masinainstruktsioonide süsteemi, mis võimaldab luua mikroprotsessoreid erinevates kasutusvaldkondades, ilma litsentsitasudeta ja ilma kasutustingimusteta. RISC-V võimaldab luua täiesti avatud SoC ja protsessoreid. Praegu on RISC-V spetsifikatsiooni alusel erinevad ettevõtted ja kogukonnad välja töötanud mitmesuguseid tasuta litsentse (BSD, MIT, Apache 2.0). mõnikümmend erinevat mikroprotsessori tuuma, SoC ja juba tootmisse viidud kiipe. RISC-V tugi on olemas alates Glibc 2.27, binutils 2.30, gcc 7 ja Linuxi tuuma 4.15 väljaandmisest.
Allikas: opennet.ru
