Mikrokernel seL4 matematički je verificiran za RISC-V arhitekturu

Zaklada RISC-V izvijestio O provjeri rada mikropremotavanja seL4 Na sustavima s arhitekturom skupa naredbi RISC-V. Verifikacija se svodi na matematički dokazi pouzdanost rada seL4, što ukazuje na punu usklađenost sa specifikacijama navedenim u formalnom jeziku. Dokaz pouzdanosti omogućuje korištenje SEL4 u kritičnim sustavima baziranim na RISC-V RV64 procesorima, koji zahtijevaju povećanu razinu pouzdanosti i jamče nedostatak kvarova. Programeri softvera koji rade na jezgri SEL4 mogu biti potpuno sigurni da se u slučaju kvara u jednom dijelu sustava taj kvar neće proširiti na ostatak sustava, a posebno na njegove kritične dijelove.

U početku je mikro-oligro SEL4 verificiran za 32-bitne ARM procesore, a kasnije za 64-bitne procesore X86. Napominje se da će kombinacija otvorene hardverske arhitekture RISC-V s otvorenim mikroprinosom SEL4 postići novu razinu sigurnosti, budući da se hardverske komponente u budućnosti također mogu potpuno verificirati, što se ne može postići za vlasničke hardverske arhitekture .

Tijekom verifikacije SEL4 pretpostavlja se da oprema radi kako je navedeno i specifikacija u potpunosti opisuje ponašanje sustava, ali zapravo oprema nije eliminirana od grešaka, što dobro pokazuju problemi koji se redovito pojavljuju u mehanizam spekulativne provedbe instrukcija. Otvorene hardverske platforme pojednostavljuju integraciju promjena povezanih sa sigurnošću - na primjer, za blokiranje svih mogućih kanala curenja putem kanala trećih strana, u čemu je mnogo učinkovitije riješiti se problema hardvera nego pokušavati programski tražiti zaobilazne staze .

Podsjetimo se da seL4 arhitektura izvanredan pomicanje dijelova za upravljanje resursima jezgre u korisnički prostor i primjena istih sredstava kontrole pristupa za takve resurse kao i za korisničke resurse. Mikrojezgra ne pruža gotove apstrakcije visoke razine 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 resursima procesora. Apstrakcije visoke razine i upravljački programi za interakciju s hardverom implementirani su zasebno na vrhu mikrojezgre u obliku zadataka na razini korisnika. Pristup takvih zadataka resursima dostupnim mikrojezgri organiziran je kroz definiranje pravila.

RISC-V pruža otvoren i fleksibilan sustav strojnih instrukcija koji omogućuje izradu mikroprocesora za proizvoljne primjene bez potrebe za tantijemama ili vezanim ugovorima za korištenje. RISC-V vam omogućuje stvaranje potpuno otvorenih SoC-ova i procesora. Trenutno se temelji na RISC-V specifikaciji različitih tvrtki i zajednica pod različitim besplatnim licencama (BSD, MIT, Apache 2.0) razvija se nekoliko desetaka varijanti mikroprocesorskih jezgri, SoC-ova i već proizvedenih čipova. Podrška za RISC-V prisutna je od izdanja Glibc 2.27, binutils 2.30, gcc 7 i Linux kernela 4.15.

Izvor: opennet.ru