RISC-V fondas paskelbė, kad patikrino seL4 mikrobranduolio funkcionalumą sistemose su RISC-V instrukcijų rinkinio architektūra . Patikrinti tereikia matematinio seL4 patikimumo įrodymo, rodančio visišką atitiktį formalioje kalboje apibrėžtoms specifikacijoms.
Patikimumo testas leidžia naudoti seL4 kritinėse sistemose, pagrįstose RV64 RISC-V procesoriais , kurioms reikalingas didesnis patikimumo lygis ir kurios negarantuoja gedimų.
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 pasižymi tuo, kad iš vartotojo erdvės pašalina dalis, skirtas branduolio ištekliams valdyti , ir tokiems ištekliams naudoja tuos pačius prieigos kontrolės metodus kaip ir vartotojo ištekliams.
Mikrobranduolys nepateikia paruoštų aukšto lygio abstrakcijų failams, procesams, tinklo ryšiams ir pan. valdyti, o tik minimalius mechanizmus, skirtus valdyti prieigą prie fizinės adresų erdvės , pertraukimų ir procesoriaus išteklių.
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ą mašininių instrukcijų sistemą, leidžiančią kurti mikroprocesorius bet kokioms reikmėms, nereikalaujant išvadų ir nenustatant 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ų seL4 mikrobranduolys buvo patikrintas 32 bitų ARM procesoriams , o vėliau – 64 bitų x86 procesoriams.
Pastebėta, kad atviros RISC-V aparatinės įrangos architektūros ir atviro seL4 mikrobranduolio derinys pasieks naują saugumo lygį , nes ateityje aparatinės įrangos komponentai taip pat galės būti visiškai patikrinti, ko neįmanoma pasiekti naudojant patentuotas aparatinės įrangos architektūras.
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 su saugumu susijusių pakeitimų integravimą , pavyzdžiui, siekiant užblokuoti visus galimus nutekėjimo kanalus per trečiųjų šalių kanalus, kur daug efektyviau atsikratyti problemos aparatine įranga, nei bandyti rasti sprendimus programine įranga.
Galiausiai, jei norite sužinoti daugiau, galite perskaityti straipsnį, pateiktą šioje nuorodoje.