SeL4 mikrotuum on RISC-V arhitektuuri jaoks matemaatiliselt kinnitatud

RISC-V sihtasutus teatatud mikrokerneli töö kontrollimise kohta seL4 RISC-V käsukomplekti arhitektuuriga süsteemides. Kinnitamine taandub matemaatiline tõestus seL4 töökindlus, mis näitab täielikku vastavust ametlikus keeles määratud spetsifikatsioonidele. Usaldusväärsuse tõend võimaldab kasutada seL4 missioonikriitilistes süsteemides, mis põhinevad RISC-V RV64 protsessoritel, mis nõuavad suuremat töökindlust ja tagavad rikete puudumise. SeL4 kerneli peal töötava tarkvara arendajad võivad olla täiesti kindlad, et kui süsteemi ühes osas esineb tõrge, ei levi see rike ülejäänud süsteemile ja eriti selle kriitilistele osadele.

SeL4 mikrotuum kontrolliti algselt 32-bitiste ARM-protsessorite jaoks ja hiljem 64-bitiste x86-protsessorite jaoks. Märgitakse, et avatud RISC-V riistvaraarhitektuuri kombineerimine avatud seL4 mikrokerneliga saavutab uue turvalisuse taseme, kuna riistvarakomponente saab ka tulevikus täielikult kontrollida, mida patenteeritud riistvaraarhitektuuride puhul on võimatu saavutada.

SeL4 kontrollimisel eeldatakse, et seade töötab nii, nagu on öeldud ja spetsifikatsioon kirjeldab täielikult süsteemi käitumist, kuid tegelikkuses ei ole seadmed vigadest vabad, mida näitavad selgelt regulaarselt ilmnevad probleemid spekulatiivse täitmise mehhanismis. juhiseid. Avatud riistvaraplatvormid muudavad turvalisusega seotud muudatuste integreerimise lihtsamaks – näiteks blokeerivad kõik võimalikud külgkanalite lekked, kus riistvaralisest probleemist on palju tõhusam vabaneda, kui proovida tarkvaras lahendusi leida.

Tuletame meelde, et seL4 arhitektuur tähelepanuväärne osade liigutamine tuumaressursside haldamiseks kasutajaruumi ja selliste ressursside jaoks samade juurdepääsukontrollivahendite rakendamiseks nagu kasutajaressursside jaoks. Mikrotuum ei paku valmis kõrgetasemelisi abstraktsioone failide, protsesside, võrguühenduste jms haldamiseks, selle asemel pakub see vaid minimaalseid mehhanisme juurdepääsu kontrollimiseks füüsilisele aadressiruumile, katkestustele ja protsessori ressurssidele. Kõrgetasemelised abstraktsioonid ja draiverid riistvaraga suhtlemiseks rakendatakse mikrokerneli peale eraldi kasutajataseme ülesannete kujul. Selliste ülesannete juurdepääs mikrokernelile kättesaadavatele ressurssidele on korraldatud reeglite määratlemise kaudu.

RISC-V pakub avatud ja paindlikku masinakäskluste süsteemi, mis võimaldab luua mikroprotsessoreid suvaliste rakenduste jaoks, ilma et oleks vaja kasutada autoritasusid või stringe. RISC-V võimaldab luua täiesti avatud SoC-sid ja protsessoreid. Praegu põhineb erinevate ettevõtete ja kogukondade RISC-V spetsifikatsioon erinevate tasuta litsentside alusel (BSD, MIT, Apache 2.0) areneb mitukümmend varianti mikroprotsessori südamikest, SoC-sid ja juba toodetud kiipe. RISC-V tugi on olnud olemas alates versioonide Glibc 2.27, binutils 2.30, gcc 7 ja Linuxi kerneli versiooni 4.15 väljalaskmisest.

Allikas: opennet.ru

Lisa kommentaar