Fondacija RISC-V o verifikaciji rada mikrokernela na sistemima sa RISC-V arhitekturom skupa instrukcija. Verifikacija se svodi na pouzdanost rada seL4, što ukazuje na potpunu usklađenost sa specifikacijama navedenim u formalnom jeziku. Dokaz o pouzdanosti seL4 u kritičnim sistemima zasnovanim na RISC-V RV64 procesorima koji zahtevaju povećan nivo pouzdanosti i garantuju odsustvo kvarova. Programeri softvera koji radi na vrhu seL4 kernela mogu biti potpuno sigurni da ako dođe do kvara u jednom dijelu sistema, ovaj kvar se neće proširiti na ostatak sistema, a posebno na njegove kritične dijelove.
Mikrokernel seL4 je prvobitno verifikovan za 32-bitne ARM procesore, a kasnije za 64-bitne x86 procesore. Napominje se da će se kombinacijom otvorene RISC-V hardverske arhitekture sa otvorenim mikrokernelom seL4 postići novi nivo sigurnosti, budući da se hardverske komponente u budućnosti mogu u potpunosti verificirati, što je nemoguće postići za vlasničke hardverske arhitekture.
Prilikom verifikacije seL4 pretpostavlja se da oprema radi kako je navedeno i specifikacija u potpunosti opisuje ponašanje sistema, ali u stvarnosti oprema nije bez grešaka, što se jasno pokazuje kroz redovno pojavljivanje problema u mehanizmu spekulativnog izvršenja instrukcije. Otvorene hardverske platforme olakšavaju integraciju sigurnosnih promjena - na primjer, blokiranje svih mogućih curenja bočnih kanala, gdje je mnogo efikasnije riješiti se problema u hardveru nego pokušati pronaći rješenja u softveru.
Podsjetimo da je seL4 arhitektura pokretni dijelovi za upravljanje resursima kernela u korisnički prostor i primjenu istih sredstava kontrole pristupa za takve resurse kao i za korisničke resurse. Mikrokernel ne pruža gotove apstrakcije visokog nivoa za upravljanje datotekama, procesima, mrežnim vezama i slično; umjesto toga, pruža samo minimalne mehanizme za kontrolu pristupa fizičkom adresnom prostoru, prekidima i procesorskim resursima. Apstrakcije visokog nivoa i drajveri za interakciju sa hardverom implementirani su odvojeno na vrhu mikrokernela u obliku zadataka na nivou korisnika. Pristup takvih zadataka resursima dostupnim mikrokernelu je organizovan kroz definiciju pravila.
RISC-V pruža otvoren i fleksibilan sistem mašinskih instrukcija koji omogućava da se mikroprocesori grade za proizvoljne aplikacije bez potrebe za autorskim honorarima ili vezama za upotrebu. RISC-V vam omogućava da kreirate potpuno otvorene SoC-ove i procesore. Trenutno baziran na RISC-V specifikaciji različitih kompanija i zajednica pod različitim besplatnim licencama (BSD, MIT, Apache 2.0) nekoliko desetina varijanti mikroprocesorskih jezgara, SoC-a i već proizvedenih čipova. RISC-V podrška je prisutna od izdanja Glibc 2.27, binutils 2.30, gcc 7 i Linux kernela 4.15.
izvor: opennet.ru