RISC-V fondas apie mikrobranduolių veikimo patikrinimą sistemose su RISC-V instrukcijų rinkinio architektūra. Patvirtinimas vyksta iki seL4 veikimo patikimumas, o tai rodo visišką atitikimą formalioje kalboje nurodytoms specifikacijoms. Patikimumo įrodymas seL4 itin svarbiose sistemose, pagrįstose RISC-V RV64 procesoriais, kurioms reikalingas didesnis patikimumo lygis ir kurios garantuoja gedimų nebuvimą. SeL4 branduolio viršuje veikiančios programinės įrangos kūrėjai gali būti visiškai tikri, kad įvykus gedimui vienoje sistemos dalyje, šis gedimas neišplis į likusią sistemos dalį ir ypač svarbias jos dalis.
SeL4 mikrobranduolis iš pradžių buvo patikrintas 32 bitų ARM procesoriams, o vėliau – 64 bitų x86 procesoriams. Pažymima, kad derinant atvirą RISC-V aparatinės įrangos architektūrą su atviru seL4 mikrobranduoliu, bus pasiektas naujas saugumo lygis, nes aparatinės įrangos komponentai taip pat gali būti visiškai patikrinti ateityje, o tai neįmanoma pasiekti patentuotoms techninės įrangos architektūroms.
Tikrinant seL4, daroma prielaida, kad įranga veikia taip, kaip nurodyta, o specifikacija visiškai apibūdina sistemos elgseną, tačiau iš tikrųjų įranga nėra be klaidų, o tai aiškiai įrodo reguliariai kylančios problemos spekuliacinio vykdymo mechanizme. nurodymus. Atviros aparatinės įrangos platformos leidžia lengviau integruoti su saugumu susijusius pakeitimus – pavyzdžiui, blokuoti visus galimus šoninių kanalų nutekėjimus, kur daug efektyviau yra atsikratyti aparatinės įrangos problemos, nei bandyti ieškoti sprendimų programinėje įrangoje.
Prisiminkite, kad seL4 architektūra perkeliamos dalys branduolio ištekliams valdyti į vartotojo erdvę ir tokiems ištekliams taikyti tas pačias prieigos kontrolės priemones kaip ir vartotojo ištekliams. Mikrobranduolys nesuteikia paruoštų aukšto lygio abstrakcijų failams, procesams, tinklo ryšiams ir panašiai tvarkyti; vietoj to jis suteikia tik minimalius mechanizmus, skirtus kontroliuoti prieigą prie fizinės adresų erdvės, pertraukimus ir procesoriaus išteklius. Aukšto lygio abstrakcijos ir sąveikos su aparatine įranga tvarkyklės yra įdiegtos atskirai ant mikrobranduolių, vartotojo lygio užduočių pavidalu. Tokių užduočių prieiga prie mikrobranduoliui prieinamų išteklių organizuojama apibrėžiant taisykles.
RISC-V suteikia atvirą ir lanksčią mašinų instrukcijų sistemą, kuri leidžia kurti mikroprocesorius savavališkoms programoms nereikalaujant honorarų ar priedų naudoti. RISC-V leidžia sukurti visiškai atvirus SoC ir procesorius. Šiuo metu pagrįsta RISC-V specifikacija, kurią sudaro įvairios įmonės ir bendruomenės pagal įvairias nemokamas licencijas (BSD, MIT, Apache 2.0). kelios dešimtys mikroprocesorių branduolių, SoC ir jau pagamintų lustų variantų. RISC-V palaikymas teikiamas nuo Glibc 2.27, binutils 2.30, gcc 7 ir Linux branduolio 4.15 išleidimo.
Šaltinis: opennet.ru