RISC-V pārbaudīja seL4 mikrokodeli savos RV64 procesoros

RISC-V fonds paziņoja, ka ir pārbaudījis kā darbojas mikrokodelis seL4 sistēmās ar instrukciju kopas arhitektūra RISC-V. Tajā verifikācijas process tiek samazināts līdz matemātiskam seL4 uzticamības pierādījumam, kas norāda uz pilnīgu atbilstību oficiālajā valodā norādītajām specifikācijām.

Uzticamības pārbaude ļauj seL4 izmantot misijai kritiskās sistēmās, kuru pamatā ir RISC-V procesori RV64, kas prasa augstāku uzticamības līmeni un negarantē neveiksmi.

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ērojams ar daļu noņemšanu, lai pārvaldītu kodola resursus lietotāja telpā un šādiem resursiem izmantojiet tādas pašas piekļuves kontroles metodes kā lietotāju resursiem.

Mikrokodels nenodrošina augsta līmeņa abstrakcijas jau gatavs pārvaldīt failus, procesus, tīkla savienojumus utt., bet tā vietā nodrošina tikai minimālus mehānismus, lai kontrolētu piekļuvi fiziskajai adreses vietai, pārtrauc un procesora resursus.

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 sistēmu mašīnu instrukcijas, 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 mikrokodels seL4 tika pārbaudīts 32 bitu ARM procesoriem, Un vēlāk x86 64 bitu procesoriem.

Tiek novērots, ka RISC-V atvērtās aparatūras arhitektūras un atvērtā mikrokoda kombinācija seL4 sasniegs jaunu drošības līmeni, jo arī aparatūras komponentus nākotnē var pilnībā pārbaudīt, ko nav iespējams sasniegt 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ērtas aparatūras platformas vienkāršo izmaiņu integrāciju kas saistīti ar drošību, piemēram, lai bloķētu visus iespējamos noplūdes kanālus, izmantojot trešo personu kanālus, kur daudz efektīvāk ir atbrīvoties no problēmas ar aparatūru, nevis mēģināt atrast risinājumus pēc programmatūras.

Visbeidzot, ja vēlaties uzzināt vairāk par to, varat iepazīties ar piezīmi šī saite.