RISC-V fonds par mikrokodola darbības pārbaudi sistēmās ar RISC-V instrukciju kopas arhitektūru. Pārbaude tiek veikta seL4 darbības uzticamība, kas liecina par pilnīgu atbilstību oficiālajā valodā norādītajām specifikācijām. Uzticamības pierādījums seL4 misijai kritiskajās sistēmās, kuru pamatā ir RISC-V RV64 procesori, kam nepieciešams paaugstināts uzticamības līmenis un garantēt kļūmju neesamību. Programmatūras izstrādātāji, kas darbojas virs seL4 kodola, var būt pilnīgi pārliecināti, ka, ja vienā sistēmas daļā ir kļūme, šī kļūme netiks izplatīta pārējā sistēmā un jo īpaši tās kritiskajās daļās.
SeL4 mikrokodolu sākotnēji verificēja 32 bitu ARM procesoriem un vēlāk 64 bitu x86 procesoriem. Tiek atzīmēts, ka, apvienojot atvērto RISC-V aparatūras arhitektūru ar atvērto mikrokodolu seL4, tiks sasniegts jauns drošības līmenis, jo aparatūras komponentus var pilnībā pārbaudīt arī nākotnē, ko nav iespējams sasniegt patentētām aparatūras arhitektūrām.
Pārbaudot seL4, tiek pieņemts, ka iekārta darbojas kā norādīts un specifikācija pilnībā apraksta sistēmas uzvedību, taču patiesībā iekārta nav brīva no kļūdām, par ko skaidri liecina regulāri parādās problēmas spekulatīvās izpildes mehānismā. instrukcijas. Atvērtās aparatūras platformas ļauj vienkāršāk integrēt ar drošību saistītās izmaiņas – piemēram, bloķēt visas iespējamās sānu kanālu noplūdes, kur daudz efektīvāk ir atbrīvoties no aparatūras problēmas, nevis mēģināt atrast risinājumus programmatūrā.
Atgādiniet, ka seL4 arhitektūra pārvietojot daļas kodola resursu pārvaldīšanai lietotāja telpā un tādu pašu piekļuves kontroles līdzekļu izmantošanai šādiem resursiem kā lietotāju resursiem. Mikrokodolis nenodrošina gatavas augsta līmeņa abstrakcijas failu, procesu, tīkla savienojumu un tamlīdzīgu pārvaldīšanai; tā vietā tas nodrošina tikai minimālus mehānismus, lai kontrolētu piekļuvi fiziskajai adrešu telpai, pārtraukumiem un procesora resursiem. Augsta līmeņa abstrakcijas un draiveri mijiedarbībai ar aparatūru tiek ieviesti atsevišķi virs mikrokodola lietotāja līmeņa uzdevumu veidā. Šādu uzdevumu piekļuve mikrokodola rīcībā esošajiem resursiem tiek organizēta, definējot noteikumus.
RISC-V nodrošina atvērtu un elastīgu mašīnu instrukciju sistēmu, kas ļauj izveidot mikroprocesorus patvaļīgiem lietojumiem, neprasot izmantošanai honorārus vai pievienotās virknes. RISC-V ļauj izveidot pilnīgi atvērtus SoC un procesorus. Pašlaik pamatā ir dažādu uzņēmumu un kopienu RISC-V specifikācija saskaņā ar dažādām bezmaksas licencēm (BSD, MIT, Apache 2.0). vairāki desmiti mikroprocesoru kodolu, SoC un jau ražotu mikroshēmu variantu. RISC-V atbalsts ir pieejams kopš Glibc 2.27, binutils 2.30, gcc 7 un Linux kodola 4.15 izlaišanas.
Avots: opennet.ru