RISC-V patikrino seL4 mikrobranduolį savo RV64 procesoriuose

RISC-V fondas paskelbė, kad patikrino kaip veikia mikrobranduolys seL4 sistemose su instrukcijų rinkinio architektūra RISC-V. Atliekant patikros procesą sutrumpinamas matematinis seL4 patikimumo testas, kuris rodo visišką atitikimą oficialia kalba nurodytoms specifikacijoms.

Patikimumo testavimas leidžia seL4 naudoti kritinėms misijos sistemoms, pagrįstoms RISC-V procesoriais RV64, kuris reikalauja aukštesnio patikimumo lygio ir negarantuoja nesėkmės.

Programinės įrangos kūrėjai, veikiantys ant „seL4“ branduolio, gali būti visiškai tikri, kad sugedus vienai sistemos daliai, šis gedimas nebus išplitęs visoje kitoje sistemoje ir ypač jos kritinėse dalyse.

Apie seL4

SeL4 architektūra yra pastebimas pašalinant dalis, kad būtų galima tvarkyti branduolio išteklius vartotojo erdvėje ir tokiems ištekliams naudoti tuos pačius prieigos kontrolės metodus kaip ir vartotojų ištekliams.

Mikrobranduolys nepateikia aukšto lygio abstrakcijų jau pasirengęs tvarkyti failus, procesus, tinklo ryšius ir pan., bet vietoj to suteikia tik minimalius mechanizmus, leidžiančius kontroliuoti prieigą prie fizinio adreso, pertraukia ir procesoriaus išteklius.

Aukšto lygio abstrakcijos ir valdikliai, skirti sąveikai su kompiuteriu, atskirai įgyvendinami ant mikrobranduolio kaip vartotojo lygiu atliekamos užduotys.

Tokių užduočių prieiga prie turimų išteklių yra organizuojama apibrėžiant taisykles.

RISC-V teikia atvirą ir lanksčią sistemą mašinų instrukcijas leidžia sukurti mikroprocesorius savavališkoms programoms, nereikalaujant atskaitymų ir nenustačius naudojimo sąlygų.

RISC-V leidžia jums sukurti visiškai atvirus procesorius ir SoC. Šiuo metu, remiantis RISC-V specifikacija, kelios įmonės ir bendruomenės, turinčios įvairias nemokamas licencijas (BSD, MIT, Apache 2.0), kuria kelias dešimtis jau pagamintų mikroprocesorinių branduolių, SoC ir lustų variantų.

RISC-V palaikymas egzistuoja nuo „Glibc 2.27“, „binutils 2.30“, „gcc 7“ ir „Linux 4.15“ branduolio išleidimo.

Apie „seL4“ mikrobranduolių testavimą

Iš pradžių mikrokernelis seL4 buvo patikrintas 32 bitų ARM procesoriamsIr vėliau x86 64 bitų procesoriams.

Pastebima, kad RISC-V atviros aparatinės įrangos architektūros derinys su atviru mikrobrandeliu „seL4“ pasieks naują saugumo lygį, nes ateityje taip pat galima visiškai patikrinti aparatūros komponentus, ko neįmanoma pasiekti nuosavybės teise priklausančioms aparatūros architektūroms.

Patikrinę „seL4“, turime manyti, kad aparatinė įranga veikia tinkamai (tai yra, kaip nurodyta). Tai daro prielaidą, kad visų pirma yra nedviprasmiška specifikacija, o tai ne visos aparatūros atveju. 

Bet net jei egzistuoja tokia specifikacija ir ji yra formali (t. Y. Suskirstyta į matematinį formalizmą, kuris palaiko matematinius argumentus apie jo savybes), iš kur mes žinome, kad ji iš tikrųjų fiksuoja aparatūros elgesį? 

Realybė yra ta, kad galime būti tikri, jog taip nėra. Aparatinė įranga niekuo nesiskiria nuo to, kad abi yra klaidingos.

Tačiau turint atvirą ISA yra privalumų, kurie apima ne tik nemokamą atlygį. Vienas iš jų yra tai, kad jis leidžia įdiegti atvirojo kodo aparatūrą.

Tikrinant seL4 daroma prielaida, kad įranga veikia taip, kaip nurodyta, o specifikacijoje visiškai aprašomas sistemos elgesys, tačiau iš tikrųjų įranga nėra be klaidų, ką gerai parodo problemos, kurios reguliariai kyla spekuliaciniame vykdymo mechanizme. .

Atviros aparatinės įrangos platformos supaprastina pakeitimų integravimą susijusių su saugumu, pavyzdžiui, blokuoti visus įmanomus nuotėkio kanalus per trečiųjų šalių kanalus, kur daug efektyviau yra atsikratyti problemos aparatine įranga, nei bandyti ieškoti sprendimų pagal programinę įrangą.

Galiausiai, jei norite sužinoti daugiau apie tai, galite peržiūrėti pastabą sekanti nuoroda.