RISC-V fonds paziņoja, ka ir pārbaudījis seL4 mikrokodola funkcionalitāti sistēmās ar RISC-V instrukciju kopas arhitektūru . Pārbaudes process ir reducēts līdz seL4 uzticamības matemātiskam pierādījumam, kas norāda uz pilnīgu atbilstību formālā valodā definētajām specifikācijām.
Uzticamības tests ļauj izmantot seL4 kritiski svarīgās sistēmās, kuru pamatā ir RV64 RISC-V procesori , kurām nepieciešams augstāks uzticamības līmenis un kuras negarantē kļūmes.
Programmatūras izstrādātāji, kas darbojas virs seL4 kodola, var būt pilnīgi pārliecināti, ka vienas sistēmas daļas kļūmes gadījumā šī kļūda netiks izplatīta pārējā sistēmā un it īpaši tās kritiskajās daļās.
Par seL4
seL4 arhitektūra ir ievērojama ar to, ka no lietotāja telpas tiek noņemtas daļas kodola resursu pārvaldībai un šiem resursiem tiek izmantotas tās pašas piekļuves kontroles metodes kā lietotāju resursiem.
Mikrokodols nenodrošina gatavas augsta līmeņa abstrakcijas failu, procesu, tīkla savienojumu u. c. pārvaldībai, bet gan tikai minimālus mehānismus piekļuves kontrolei fiziskajai adrešu telpai , pārtraukumiem un procesora resursiem.
Augsta līmeņa abstrakcijas un draiveri mijiedarbībai ar datoru tiek atsevišķi ieviesti mikrokoda augšpusē lietotāja līmenī veiktu uzdevumu veidā.
Šādu uzdevumu piekļuve mikrokodelē pieejamajiem resursiem tiek organizēta, definējot noteikumus.
RISC-V nodrošina atvērtu un elastīgu mašīninstrukciju sistēmu, kas ļauj izveidot mikroprocesorus patvaļīgām lietojumprogrammām, neprasot atskaitījumus un neuzliekot lietošanas nosacījumus.
RISC-V ļauj jums izveidot pilnīgi atvērtus procesorus un SoC. Pašlaik, pamatojoties uz RISC-V specifikāciju, dažādi uzņēmumi un kopienas ar dažādām bezmaksas licencēm (BSD, MIT, Apache 2.0) izstrādā vairākus desmitus jau ražotu mikroprocesoru kodolu, SoC un mikroshēmu variantu.
RISC-V atbalsts ir bijis kopš Glibc 2.27, binutils 2.30, gcc 7 un Linux 4.15 kodola izlaišanas.
Par seL4 mikrokoda testēšanu
Sākotnēji seL4 mikrokodols tika pārbaudīts 32 bitu ARM procesoriem , bet vēlāk - 64 bitu x86 procesoriem.
Tiek novērots, ka atvērtās RISC-V aparatūras arhitektūras apvienojums ar atvērto seL4 mikrokodolu sasniegs jaunu drošības līmeni , jo nākotnē aparatūras komponentus varēs pilnībā pārbaudīt, ko nav iespējams panākt patentētām aparatūras arhitektūrām.
Pārbaudot seL4, mums jāpieņem, ka aparatūra darbojas pareizi (tas ir, kā norādīts). Tas pieņem, ka vispirms ir nepārprotama specifikācija, kas nav attiecināma uz visu aparatūru.
Bet pat tad, ja šāda specifikācija pastāv un tā ir formāla (tas ir, iekļauta matemātiskā formālismā, kas atbalsta matemātisko pamatojumu par tā īpašībām), kā mēs zinām, ka tā faktiski uztver aparatūras uzvedību?
Realitāte ir tāda, ka mēs varam būt diezgan droši, ka tā nav. Aparatūra neatšķiras no programmatūras, jo abi ir bagāti.
Bet atvērta ISA pieejamībai ir priekšrocības, kas pārsniedz bez atlīdzības. Viens ir tas, ka tas ļauj atvērtā koda aparatūras ieviešanu.
Pārbaudot seL4, tiek pieņemts, ka iekārta darbojas tā, kā norādīts, un specifikācija pilnībā apraksta sistēmas darbību, taču faktiski iekārta nav bez kļūdām, ko labi parāda problēmas, kas regulāri rodas spekulatīvajā izpildes mehānismā. .
Atvērtās aparatūras platformas vienkāršo ar drošību saistītu izmaiņu integrāciju , piemēram, lai bloķētu visus iespējamos noplūdes kanālus caur trešo pušu kanāliem, kur ir daudz efektīvāk atbrīvoties no problēmas ar aparatūras palīdzību, nekā mēģināt rast risinājumus ar programmatūras palīdzību.
Visbeidzot, ja vēlaties uzzināt vairāk par to, varat iepazīties ar rakstu, izmantojot šo saiti.