RISC-V հիմնադրամ միկրոմիջուկի աշխատանքը ստուգելու մասին RISC-V հրահանգների հավաքածուի ճարտարապետությամբ համակարգերի վրա: Ստուգումը իջնում է seL4-ի շահագործման հուսալիությունը, որը ցույց է տալիս պաշտոնական լեզվով սահմանված բնութագրերի ամբողջական համապատասխանությունը: Հուսալիության ապացույց seL4 առաքելության կարևոր համակարգերում, որոնք հիմնված են RISC-V RV64 պրոցեսորների վրա, որոնք պահանջում են հուսալիության բարձր մակարդակ և երաշխավորում են խափանումների բացակայությունը: seL4 միջուկի վերևում աշխատող ծրագրակազմի մշակողները կարող են լիովին վստահ լինել, որ եթե համակարգի մի մասում խափանում է, այս ձախողումը չի տարածվի համակարգի մնացած մասի և, մասնավորապես, նրա կարևոր մասերի վրա:
seL4 միկրոմիջուկը սկզբում ստուգվել է 32-բիթանոց ARM պրոցեսորների համար, իսկ ավելի ուշ՝ 64-բիթանոց x86 պրոցեսորների համար։ Նշվում է, որ բաց RISC-V ապարատային ճարտարապետության համադրությունը բաց seL4 միկրոմիջուկի հետ կհասնի անվտանգության նոր մակարդակի, քանի որ ապարատային բաղադրիչները կարող են նաև լիովին ստուգվել ապագայում, ինչը անհնար է հասնել սեփական ապարատային ճարտարապետությունների համար:
seL4-ը ստուգելիս ենթադրվում է, որ սարքավորումն աշխատում է այնպես, ինչպես նշված է, և տեխնիկական բնութագրերը լիովին նկարագրում են համակարգի վարքագիծը, սակայն իրականում սարքավորումը զերծ չէ սխալներից, ինչը հստակորեն երևում է սպեկուլյատիվ կատարման մեխանիզմում պարբերաբար առաջացող խնդիրներով: հրահանգներ. Բաց ապարատային հարթակները հեշտացնում են անվտանգության հետ կապված փոփոխությունների ինտեգրումը, օրինակ՝ արգելափակել բոլոր հնարավոր կողմնակի ալիքների արտահոսքերը, որտեղ շատ ավելի արդյունավետ է ապարատային խնդրից ազատվելը, քան ծրագրային ապահովման մեջ լուծումներ գտնելը:
Հիշեցնենք, որ seL4 ճարտարապետությունը շարժվող մասեր՝ միջուկի ռեսուրսները օգտագործողի տարածություն կառավարելու և մուտքի վերահսկման նույն միջոցները կիրառելու համար այնպիսի ռեսուրսների համար, ինչ օգտագործողի ռեսուրսների համար: Միկրոմիջուկը չի տրամադրում պատրաստի բարձր մակարդակի աբստրակցիաներ ֆայլերի, պրոցեսների, ցանցային կապերի և այլնի կառավարման համար, փոխարենը տրամադրում է միայն նվազագույն մեխանիզմներ ֆիզիկական հասցեների տարածության, ընդհատումների և պրոցեսորի ռեսուրսների հասանելիությունը վերահսկելու համար: Բարձր մակարդակի աբստրակցիաները և սարքավորումների հետ փոխազդեցության դրայվերներն իրականացվում են առանձին միկրոմիջուկի վերևում՝ օգտագործողի մակարդակի առաջադրանքների տեսքով: Նման առաջադրանքների հասանելիությունը միկրոմիջուկին հասանելի ռեսուրսներին կազմակերպվում է կանոնների սահմանման միջոցով:
RISC-V-ն ապահովում է բաց և ճկուն մեքենաների հրահանգավորման համակարգ, որը թույլ է տալիս միկրոպրոցեսորներ կառուցել կամայական կիրառությունների համար՝ չպահանջելով օգտագործելու համար հոնորարներ կամ լարեր: RISC-V-ն թույլ է տալիս ստեղծել ամբողջովին բաց SoC-ներ և պրոցեսորներ: Ներկայումս հիմնված է տարբեր ընկերությունների և համայնքների RISC-V ճշգրտման վրա՝ տարբեր անվճար լիցենզիաների ներքո (BSD, MIT, Apache 2.0) միկրոպրոցեսորային միջուկների, SoC-ների և արդեն արտադրված չիպերի մի քանի տասնյակ տարբերակներ: RISC-V-ի աջակցությունն առկա է Glibc 2.27, binutils 2.30, gcc 7 և Linux միջուկի 4.15 թողարկումից ի վեր:
Source: opennet.ru