Organizata RISC-V Foundation për verifikimin e funksionimit të mikrojekës në sisteme me arkitekturën e setit të komandave RISC-V. Verifikimi përqendrohet në të besueshmërisë së seL4, i cili tregon për përputhshmërinë e plotë me specifikimet që janë përcaktuar në një gjuhë formale. Provimi i besueshmërisë seL4 në sisteme të rëndësishme në bazë të procesorëve RISC-V RV64, që kërkojnë një nivel më të lartë të besueshmërisë dhe garantojnë mungesën e defekteve. Zhvilluesit e softuerit, që punojnë mbi mikrojekën seL4, mund të jenë plotësisht të sigurt se në rastin e një defekti në një pjesë të sistemit, ky defekt nuk do të shpërndahet në pjesët e tjera të sistemit dhe, veçanërisht, në pjesët e tij kritike.
Fillimisht, mikrojekë seL4 u verifikua për procesorët 32-bit ARM, dhe më vonë për procesorët 64-bit x86. Vlen të theksohet se kombinimi i arkitekturës hapësinore të hardware-it RISC-V me mikrojekën e hapur seL4 do të mundësojë arritjen e një nivele të re sigurie, pasi komponentët hardware në perspektivë gjithashtu mund të verifikohen plotësisht, gjë që nuk është e mundur për arkitekturat hardware pronësore.
Gjatë verifikimit të seL4 supozohet se pajisja punon siç është deklaruar dhe specifikimi përshkruan plotësisht sjelljen e sistemit, por në të vërtetë pajisja nuk është e lirë nga defektet, që demonstrohet mirë nga problemet që shpërthejnë rregullisht në mekanizmin e ekzekutimit spekulativ të instrukcioneve. Platformat e hapura të hardware-it lehtësojnë integrimin e ndryshimeve që lidhen me sigurinë - për shembull, për bllokimin e të gjitha mundësive për daljen e të dhënave përmes kanaleve anësore, ku është shumë më efektive të zgjidhet problemi në mënyrë hardware sesa të kërkohen zgjidhje programore.
Le t'i kujtojmë se arkitektura seL4 ka nxjerrë pjesët për menaxhimin e burimeve të mikrojekës në hapësirën e përdoruesit dhe përdorimin e të njëjtave mjete të ndarjes për burimet si për burimet e përdoruesit. Mikrojekë nuk ofron abstraktore të gatshme të niveleve të larta për menaxhimin e skedarëve, proceseve, lidhjeve rrjetërore etj., përkundrazi ajo ofron vetëm mekanizma minimale për menaxhimin e qasjes në hapësirën fizike të adresave, ndërprerjet dhe burimet e procesorit. Abstraktoret e nivelit të lartë dhe drejtuesit për ndërveprimin me hardware-n realizohen veçmas mbi mikrojekë në formën e detyrave që ekzekutohen në nivelin e përdoruesit. Qasja e këtyre detyrave në burimet që ka mikrojekë organizohet përmes përcaktimit të rregullave.
RISC-V ofron një sistem të hapur dhe fleksibël të instruksioneve të makinerisë, që lejon krijimin e mikroproçesorëve për aplikacione të ndryshme, pa kërkuar të hyra dhe pa vendosur kushte për përdorimin. RISC-V lejon krijimin e SoC të hapura dhe procesorëve. Aktualisht, mbi bazën e specifikimit RISC-V, kompani dhe komunitete të ndryshme, duke përdorur licenca të lira të ndryshme (BSD, MIT, Apache 2.0) kanë krijuar disa dhjetëra variante të bërthamave të mikroproçesorëve, SoC dhe çipëve që janë tashmë në prodhim. Mbështetja për RISC-V është e pranishme që nga versionet Glibc 2.27, binutils 2.30, gcc 7 dhe bërthama Linux 4.15.
Burimi: opennet.ru
