Fondacioni RISC-V njoftoi se ka verifikuar si funksionon mikrokerneli seL4 në sistemet me arkitektura e grupeve të udhëzimeve RISC-V. Në të cilin procesi i verifikimit zvogëlohet në provën matematikore të besueshmërisë së seL4, e cila tregon pajtueshmëri të plotë me specifikimet e specifikuara në një gjuhë zyrtare.
Testimi i besueshmërisë mundëson që seL4 të përdoret në sistemet kritike të misionit bazuar në procesorët RISC-V RV64, e cila kërkon një nivel më të lartë të besueshmërisë dhe nuk garanton dështimin.
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 shquhet për heqjen e pjesëve për të menaxhuar burimet e kernelit në hapësirën e përdoruesit dhe të përdorin të njëjtat metoda të kontrollit të hyrjes për burime të tilla si për burimet e përdoruesve.
Mikrokerneli nuk siguron abstraksione të nivelit të lartë tashmë të përgatitur për të menaxhuar skedarët, proceset, lidhjet e rrjetit, etj., por në vend të kësaj ofron vetëm mekanizma minimale për të kontrolluar hyrjen në hapësirën e adresave fizike, 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 të udhëzimeve të makinës 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, mikrokerneli seL4 u verifikua për procesorët 32-bit ARM, Dhe më vonë për procesorët x86 64-bit.
Shtë vërejtur se kombinimi i arkitekturës së harduerit të hapur RISC-V me mikrokernelën e hapur seL4 do të arrijë një nivel të ri siguriepasi përbërësit e harduerit në të ardhmen mund të verifikohen plotësisht, gjë që është e pamundur të arrihet për arkitekturat e pajisjeve 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 harduer thjeshtësojnë integrimin e ndryshimeve lidhur 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ë heqësh qafe një problem nga hardueri sesa të përpiqesh të gjesh zgjidhje me softuer.
Së fundmi, nëse doni të dini më shumë rreth kësaj, mund të konsultoheni me shënimin në lidhja vijuese.
Për mua, ky procesor është diçka që më thërret shumë. Mbetet vetëm për një qen kompjuteri të shëndoshë të bëjë një kompjuter që mund ta blejmë.
Çështja e ARM-së është diçka që më çirret, ju tashmë e patë se çfarë ndodhi me Huawei me sanksionet. Unë e kam të qartë se për RISC-V timen është një zgjidhje shumë më e mirë në të gjitha nivelet. Për momentin Huawei tashmë ia ka vënë syrin dhe mbase në të ardhmen ata do të kenë pajisje me këtë mikro. Nëse është kështu, me siguri do të ketë më shumë kompani që e adoptojnë atë dhe për mua kjo do të ishte ideale dhe mbi të gjitha që distros e mbështesin atë dhe jo vetëm ARM siç ndodh me shumicën.
+10