Fondacioni RISC-V në lidhje me verifikimin e funksionimit të mikrokernelit në sistemet me arkitekturë të grupit të instruksioneve RISC-V. Verifikimi zbret në besueshmëria e funksionimit seL4, e cila tregon përputhshmëri të plotë me specifikimet e specifikuara në gjuhën zyrtare. Dëshmi e besueshmërisë seL4 në sistemet kritike për misionin e bazuar në procesorët RISC-V RV64 që kërkojnë një nivel më të lartë besueshmërie dhe garantojnë mungesën e dështimeve. Zhvilluesit e softuerit që funksionon në krye të kernelit seL4 mund të jenë plotësisht të sigurt se nëse ka një dështim në një pjesë të sistemit, ky dështim nuk do të përhapet në pjesën tjetër të sistemit dhe, veçanërisht, në pjesët e tij kritike.
Mikrokerneli seL4 fillimisht u verifikua për procesorët ARM 32-bit, dhe më vonë për procesorët 64-bit x86. Vihet re se kombinimi i arkitekturës së hapur të harduerit RISC-V me mikrokernelin e hapur seL4 do të arrijë një nivel të ri sigurie, pasi komponentët e harduerit gjithashtu mund të verifikohen plotësisht në të ardhmen, gjë që është e pamundur të arrihet për arkitekturat e pronarit të harduerit.
Gjatë verifikimit të seL4, supozohet se pajisja funksionon siç thuhet dhe specifikimi përshkruan plotësisht sjelljen e sistemit, por në realitet pajisja nuk është pa gabime, gjë që tregohet qartë nga problemet që shfaqen rregullisht në mekanizmin e ekzekutimit spekulativ të udhëzimet. Platformat e hapura të harduerit e bëjnë më të lehtë integrimin e ndryshimeve të lidhura me sigurinë - për shembull, bllokimin e të gjitha rrjedhjeve të mundshme të kanaleve anësore, ku është shumë më efikase të heqësh qafe problemin në harduer sesa të përpiqesh të gjesh zgjidhje në softuer.
Kujtojmë se arkitektura seL4 pjesë lëvizëse për menaxhimin e burimeve të kernelit në hapësirën e përdoruesit dhe aplikimin e mjeteve të njëjta të kontrollit të aksesit për burime të tilla si për burimet e përdoruesit. Mikrokerneli nuk ofron abstraksione të gatshme të nivelit të lartë për menaxhimin e skedarëve, proceseve, lidhjeve të rrjetit dhe të ngjashme; në vend të kësaj, ai siguron vetëm mekanizma minimalë për kontrollin e aksesit në hapësirën fizike të adresave, ndërprerjet dhe burimet e procesorit. Abstraksionet e nivelit të lartë dhe drejtuesit për ndërveprim me harduerin zbatohen veçmas në krye të mikrokernelit në formën e detyrave të nivelit të përdoruesit. Qasja e detyrave të tilla në burimet në dispozicion të mikrokernelit organizohet përmes përcaktimit të rregullave.
RISC-V ofron një sistem të hapur dhe fleksibël instruksioni makinerie që lejon që mikroprocesorët të ndërtohen për aplikime arbitrare pa kërkuar honorare ose vargje të bashkangjitura për t'u përdorur. RISC-V ju lejon të krijoni SoC dhe procesorë plotësisht të hapur. Aktualisht bazuar në specifikimet RISC-V nga kompani dhe komunitete të ndryshme nën licenca të ndryshme falas (BSD, MIT, Apache 2.0) disa dhjetëra variante të bërthamave të mikroprocesorëve, SoC dhe çipave të prodhuar tashmë. Mbështetja RISC-V ka qenë e pranishme që nga lëshimet e Glibc 2.27, binutils 2.30, gcc 7 dhe kernel Linux 4.15.
Burimi: opennet.ru