Organizata RISC-V Foundation për verifikimin e funksionimit të mikrojehës në sisteme me arkitekturën e grupit të komandave RISC-V. Verifikimi përfshin të qëndrueshmërisë së mikrojehës seL4, e cila dëshmon për përputhshmërinë e plotë me specifikimet e caktuara në një gjuhë formale. Provimi i qëndrueshmërisë seL4 në sisteme kritikisht të rëndësishme të bazuara në procesorët RISC-V RV64, që kërkojnë një nivel të lartë të qëndrueshmërisë dhe garantimin e mungesës së dështimeve. Zhvilluesit e softuerit, që funksionojnë mbi mikrojehën seL4, mund të jenë plotësisht të sigurt se, në rast se një pjesë e sistemit dështojnë, kjo dështim nuk do të përhapej në pjesën tjetër të sistemit dhe, veçanërisht, në pjesët e tij kritike.
Fillimisht, mikrojehë seL4 u verifikua për procesorët ARM 32-bitë dhe më vonë për procesorët x86 64-bitë. Shënohet se kombinimi i arkitekturës hapur RISC-V me mikrojehën e hapur seL4 do të lejojë arritjen e një niveli të ri të sigurisë, pasi komponentët harduerikë gjithashtu në të ardhmen mund të verifikohen plotësisht, gjë që nuk është e mundur për arkitekturat harduerike proprietarë.
GjatĂ« verifikimit tĂ« seL4 supozohet se pajisja funksionon siç Ă«shtĂ« deklaruar dhe specifikimi pĂ«rshkruan plotĂ«sisht sjelljen e sistemit, por nĂ« praktikĂ« pajisja nuk Ă«shtĂ« e lirĂ« nga gabimet, e cila demonstrohet mirĂ« nga problemet qĂ« shfaqen rregullisht nĂ« mekanizmin e ekzekutimit spekulativ tĂ« instruktimeve. Platforma tĂ« hapura harduerike lehtĂ«sojnĂ« integrimin e ndryshimeve tĂ« lidhura me sigurinĂ« â pĂ«r shembull, pĂ«r tĂ« bllokuar tĂ« gjitha rrugĂ«t e mundshme tĂ« rrjedhjes pĂ«rmes kanaleve tĂ« jashtme, ku Ă«shtĂ« shumĂ« mĂ« efektive tĂ« largohet nga problemi nĂ« mĂ«nyrĂ« harduerike sesa tĂ« pĂ«rpiqemi tĂ« gjejmĂ« zgjidhje programore.
Kujtojmë se arkitektura seL4 shkëputja e pjesëve për menaxhimin e burimeve të bërthamës në hapësirën e përdoruesit dhe aplikimi për këto burime të njëjtat mjete ndarjeje të aksesit, si për burimet e përdoruesit. Mikro-bërthama nuk ofron abstraksione të larta gati për menaxhimin e skedarëve, proceseve, lidhjeve rrjetërore etj., por vetëm mekanizma minimalë për menaxhimin e aksesit në hapësirën fizike të adresave, ndërprerjet dhe burimet e procesorit. Abstraksionet e larta dhe drejtuesit për ndërveprimin me pajisjet realizohen veçmas mbi mikro-bërthamën në formën e detyrave që kryhen në nivelin e përdoruesit. Qasja e këtyre detyrave në burimet e disponueshme të mikro-bërthamës organizohet përmes përcaktimit të rregullave.
RISC-V ofron një sistem të hapur dhe fleksibël të instrukcioneve të makinës, që lejon krijimin e mikroprocesorëve për aplikime të ndryshme, pa kërkuar përfitime dhe pa vendosur kushte për përdorim. RISC-V mundëson krijimin e SoC dhe mikroprocesorëve tërësisht të hapur. Aktualisht, në bazë të specifikimit RISC-V, kompani dhe komunitete të ndryshme nën licenca të ndryshme të lira (BSD, MIT, Apache 2.0) janë duke zhvilluar disa dhjetëra variante bërthamash mikroprocesorësh, SoC dhe çipa që tashmë janë në prodhim. Mbështetja për RISC-V është e pranishme që nga publikimet e Glibc 2.27, binutils 2.30, gcc 7 dhe bërthama Linux 4.15.
Burimi: opennet.ru
