RISC-V Fundazioa mikrokernelaren funtzionamendua egiaztatzeari buruz RISC-V instrukzio multzoen arkitektura duten sistemetan. Egiaztapena da seL4 funtzionamenduaren fidagarritasuna, hizkuntza formalean zehaztutako zehaztapenak guztiz betetzen direla adierazten duena. Fidagarritasunaren froga seL4 misio kritikoko sistemetan, RISC-V RV64 prozesadoreetan oinarrituta, fidagarritasun-maila handiagoa eskatzen dutenak eta hutsegiterik ez dagoela bermatzen dutenak. SeL4 nukleoaren gainean exekutatzen den softwarearen garatzaileek erabat ziur egon daiteke sistemaren zati batean hutsegiterik badago, hutsegite hori ez dela sistemaren gainerakoetara eta, bereziki, zati kritikoetara zabalduko.
seL4 mikrokernel-a 32 biteko ARM prozesadoreetarako egiaztatu zen hasieran, eta gero 64 biteko x86 prozesadoreetarako. Kontuan izan da RISC-V hardware-arkitektura irekia eta seL4 mikrokernel irekia konbinatzeak segurtasun-maila berri bat lortuko duela, hardware-osagaiak ere guztiz egiaztatu ahal izango baitira etorkizunean, eta hori ezinezkoa da jabedun hardware-arkitekturarentzat.
SeL4 egiaztatzean, suposatzen da ekipoak esan bezala funtzionatzen duela eta zehaztapenak sistemaren portaera guztiz deskribatzen duela, baina, egia esan, ekipamendua ez dago akatsik gabe, eta hori argi eta garbi frogatzen da aldian-aldian sortzen diren arazoek exekuzio espekulatiboaren mekanismoan. argibideak. Hardware plataforma irekiek errazten dute segurtasunarekin lotutako aldaketak integratzea; adibidez, alboko kanalen ihes posible guztiak blokeatzea, non askoz eraginkorragoa den hardwarean arazoa kentzea softwarean konponbideak bilatzen saiatzea baino.
Gogoratu seL4 arkitektura nukleoko baliabideak kudeatzeko piezak erabiltzaileen espaziora mugitzea eta sarbide-kontrolerako baliabide berdinak aplikatzea erabiltzaileen baliabideetarako. Mikrokernelak ez du prestatutako goi-mailako abstrakziorik eskaintzen fitxategiak, prozesuak, sare-konexioak eta antzekoak kudeatzeko; horren ordez, helbide-espazio fisikorako, etenetarako eta prozesadore-baliabideetarako sarbidea kontrolatzeko mekanismo minimoak eskaintzen ditu. Hardwarearekin elkarreragiteko goi-mailako abstrakzioak eta kontrolatzaileak mikrokernelaren gainean bereizita inplementatzen dira erabiltzaile-mailako zereginen moduan. Mikrokernelak eskura dituen baliabideetara horrelako zereginen sarbidea arauen definizioaren bidez antolatzen da.
RISC-V-k makinen instrukzio-sistema ireki eta malgu bat eskaintzen du, mikroprozesadoreak aplikazio arbitrarioetarako eraikitzeko aukera ematen duena, erabiltzeko eskubiderik edo katerik gabe. RISC-V-k SoC eta prozesadore guztiz irekiak sortzeko aukera ematen du. Gaur egun, enpresa eta komunitate ezberdinek RISC-V zehaztapenean oinarritutako lizentzia libre ezberdinekin (BSD, MIT, Apache 2.0) Mikroprozesadoreen nukleoen, SoCen eta dagoeneko ekoiztutako txipen dozena bat aldaera. RISC-V euskarria Glibc 2.27, binutils 2.30, gcc 7 eta Linux kernel 4.15 kaleratu zirenetik egon da.
Iturria: opennet.ru