Fondacioni RISC-V njoftoi se ka verifikuar funksionalitetin e mikrobërthamës seL4 në sisteme me arkitekturën e grupit të udhëzimeve RISC-V . Procesi i verifikimit reduktohet në një provë matematikore të besueshmërisë së seL4, duke treguar përputhshmëri të plotë me specifikimet e përcaktuara në një gjuhë formale.
Testi i besueshmërisë lejon përdorimin e seL4 në sisteme kritike për misionin bazuar në procesorët RV64 RISC-V , të cilët kërkojnë një nivel më të lartë besueshmërie dhe nuk garantojnë dështime.
Zhvilluesit e softuerëve që ekzekutohen në krye të kernelit seL4 mund të jenë plotësisht të sigurt se në rast të një dështimi në një pjesë të sistemit, ky dështim nuk do të përhapet në pjesën tjetër të sistemit dhe, në veçanti, në pjesët kritike të tij. .
Rreth seL4
Arkitektura seL4 është e njohur për heqjen e pjesëve për menaxhimin e burimeve të bërthamës nga hapësira e përdoruesit dhe përdorimin e të njëjtave metodave të kontrollit të aksesit për burime të tilla si për burimet e përdoruesit.
Mikrobërthama nuk ofron abstraksione të gatshme të nivelit të lartë për menaxhimin e skedarëve, proceseve, lidhjeve të rrjetit, etj., por ofron vetëm mekanizma minimalë për kontrollin e aksesit në hapësirën fizike të adresave , ndërprerjet dhe burimet e procesorit.
Abstraksionet dhe kontrolluesit e nivelit të lartë për bashkëveprimin me kompjuterin zbatohen veçmas në krye të mikrokernelit në formën e detyrave të kryera në nivelin e përdoruesit.
Hyrja e detyrave të tilla në burimet e disponueshme në mikrokernel organizohet përmes përcaktimit të rregullave.
RISC-V ofron një sistem të hapur dhe fleksibël udhëzimesh makinerike që lejon krijimin e mikroprocesorëve për aplikime arbitrare, pa kërkuar zbritje dhe pa imponuar kushte përdorimi.
RISC-V ju lejon të krijoni SoC dhe procesorë plotësisht të hapur. Aktualisht, në bazë të specifikimit RISC-V, disa kompani dhe komunitete nën licenca të ndryshme falas (BSD, MIT, Apache 2.0) po zhvillojnë disa dhjetëra variante të bërthamave të mikroprocesorit, SoC dhe çipave tashmë të prodhuar.
Mbështetja RISC-V ka ekzistuar që nga lëshimi i Glibc 2.27, binutils 2.30, gcc 7 dhe Linux 4.15 kernel.
Rreth testimit të mikrokernelit seL4
Fillimisht, mikrobërthama seL4 u verifikua për procesorët ARM 32-bit , dhe më vonë për procesorët x86 64-bit.
Është vërejtur se kombinimi i arkitekturës së hapur harduerike RISC-V me mikrobërthamën e hapur seL4 do të arrijë një nivel të ri sigurie , pasi komponentët harduerikë në të ardhmen mund të verifikohen plotësisht, gjë që është e pamundur të arrihet për arkitekturat harduerike pronësore.
Kur kontrollojmë seL4, duhet të supozojmë se hardueri po punon si duhet (d.m.th. siç është specifikuar). Kjo supozon se ka një specifikim të qartë, në radhë të parë, i cili nuk është rasti për të gjithë pajisjet.
Por edhe kur një specifikim i tillë ekziston, dhe është zyrtar (domethënë, i veshur në një formalizëm matematikor që mbështet arsyetimin matematik për vetitë e tij), nga e dimë që ai kap sjelljen e harduerit?
Realiteti është që ne mund të jemi shumë të sigurt se nuk është kështu. Hardware nuk ndryshon nga softueri në atë që të dy janë me bug.
Por të kesh një ISA të hapur ka përparësi që shkojnë përtej të qenit pa të drejta mbretërore. Njëra është që lejon zbatime të pajisjeve me burim të hapur.
Kur kontrolloni seL4, supozohet se pajisjet funksionojnë siç tregohet dhe specifikimi përshkruan plotësisht sjelljen e sistemit, por në fakt pajisjet nuk janë pa gabime, gjë që demonstrohet mirë nga problemet që dalin rregullisht në mekanizmin spekulativ të ekzekutimit Udhëzimet
Platformat e hapura të harduerit thjeshtojnë integrimin e ndryshimeve që lidhen me sigurinë, për shembull, për të bllokuar të gjitha kanalet e mundshme të rrjedhjeve përmes kanaleve të palëve të treta, ku është shumë më efikase të zgjidhësh një problem me anë të harduerit sesa të përpiqesh të gjesh zgjidhje me anë të softuerit.
Së fundmi, nëse doni të dini më shumë rreth kësaj, mund ta lexoni artikullin në lidhjen e mëposhtme.