RISC-V-k seL4 mikrokernela egiaztatu du bere RV64 prozesadoreetan

RISC-V Fundazioak jakinarazi duela egiaztatu du nola funtzionatzen duen mikrokernelak seL4 duten sistemetan instrukzio multzoaren arkitektura RISC-V. Egiaztapen prozesua seL4ren fidagarritasunaren froga matematikoetara murrizten da, hizkuntza formal batean zehaztutako zehaztapenak guztiz betetzen direla adierazten duena.

Fidagarritasun probak seL4 RISC-V prozesadoreetan oinarritutako misio kritiko sistemetan erabiltzeko aukera ematen du RV64, fidagarritasun maila handiagoa eskatzen duena eta porrota bermatzen ez duena.

SeL4 kernelaren gainean dabiltzan software garatzaileek ziur egon daitezke sistemaren zati batean hutsegite bat gertatuz gero, hutsegite hori ez dela gainerako sistemara eta, bereziki, bere atal kritikoetara hedatuko. .

SeL4-ri buruz

SeL4 arkitektura Nabarmentzekoa da kernelaren baliabideak erabiltzailearen espazioan kudeatzeko zatiak kentzeagatik eta sarbidea kontrolatzeko metodo berdinak erabili erabiltzaileen baliabideetarako.

Mikrokernela ez du goi mailako abstrakziorik ematen fitxategiak, prozesuak, sareko konexioak eta abar kudeatzeko prestatuta dagoeneko, baina horren ordez helbide espazio fisikorako sarbidea kontrolatzeko gutxieneko mekanismoak eskaintzen ditu, etenak eta prozesadorearen baliabideak.

Goi mailako abstrakzioak eta ordenagailuarekin elkarreragiteko kontrolagailuak bereizita inplementatzen dira mikrokernelaren gainean, erabiltzaile mailan egindako zereginen moduan.

Zeregin horiek mikrokernelean eskuragarri dauden baliabideetarako sarbidea arauen definizioaren bidez antolatzen da.

RISC-V-k sistema irekia eta malgua eskaintzen du makina argibide hori aplikazio arbitrarioetarako mikroprozesadoreak sortzeko aukera ematen du, kenketarik behar izan gabe eta erabilera baldintzak ezarri gabe.

RISC-V-k SoC eta prozesadore guztiz irekiak sortzeko aukera ematen du. Gaur egun, RISC-V zehaztapenean oinarrituta, hainbat enpresa eta komunitate lizentzia libre askorekin (BSD, MIT, Apache 2.0) jada sortutako mikroprozesadoreen nukleo, SoC eta txipen hainbat dozena aldaera garatzen ari dira.

RISC-V euskarria Glibc 2.27, binutils 2.30, gcc 7 eta Linux 4.15 kernel kaleratu zirenetik dago.

SeL4 mikrokernel probei buruz

Hasieran, mikrokernela seL4 32 biteko ARM prozesadoreentzat egiaztatu zen, Eta geroago x86 64 biteko prozesadoreentzat.

RISC-V hardware irekiaren arkitektura mikrokernel irekiarekin konbinatuta dagoela ikusten da seL4-k segurtasun maila berria lortuko duetorkizunean hardware osagaiak ere erabat egiaztatu baitaitezke, eta hori lortzea ezinezkoa da jabedun hardware arkitekturetan.

SeL4 egiaztatzen dugunean, hardwareak behar bezala funtzionatzen duela suposatu behar dugu (hau da, zehaztu bezala). Horrek suposatzen du lehenik eta behin zalantzarik gabeko zehaztapen bat dagoela, eta hori ez da hardware guztiaren kasua. 

Baina zehaztapen hori existitzen denean eta formala denean ere (hau da, bere propietateei buruzko arrazoibide matematikoa onartzen duen formalismo matematiko batean idatzita dago), nola jakin dezakegu benetan harrapatzen duela hardwarearen portaera? 

Errealitatea da ziur egon gaitezkeela ez dela. Hardwarea ez da softwarearekiko, biak buggy direlako.

ISA irekia izateak erregealderik gabeko izatetik haratago doazen abantailak ditu. Bat da kode irekiko hardwarearen inplementazioak ahalbidetzen dituela.

SeL4 egiaztatzerakoan, ekipoak adierazitako moduan funtzionatzen duela suposatzen da eta zehaztapenek sistemaren portaera guztiz deskribatzen dute, baina, egia esan, ekipamenduak ez du akatsik, eta hori ondo frogatzen da exekuzio espekulatiboaren mekanismoan aldizka sortzen diren arazoek. Argibideak.

Hardware irekiko plataformek aldaketen integrazioa errazten dute segurtasunarekin lotuta, adibidez, hirugarrenen kanalen bidez ihes kanal posible guztiak blokeatzeko, non hardwarearekin arazoa kentzea askoz ere eraginkorragoa den software bidez konponbideak aurkitzen saiatzea baino.

Azkenean, horri buruz gehiago jakin nahi baduzu, oharra kontsultatu dezakezu honako esteka.


Artikuluaren edukia gure printzipioekin bat dator etika editoriala. Akats baten berri emateko egin klik hemen.

2 iruzkin, utzi zurea

Utzi zure iruzkina

Zure helbide elektronikoa ez da argitaratuko. Beharrezko eremuak markatuta daude *

*

*

  1. Datuen arduraduna: Miguel Ángel Gatón
  2. Datuen xedea: SPAM kontrolatzea, iruzkinen kudeaketa.
  3. Legitimazioa: Zure baimena
  4. Datuen komunikazioa: datuak ez zaizkie hirugarrenei jakinaraziko legezko betebeharrez izan ezik.
  5. Datuak biltegiratzea: Occentus Networks-ek (EB) ostatatutako datu-basea
  6. Eskubideak: Edonoiz zure informazioa mugatu, berreskuratu eta ezabatu dezakezu.

  1.   batzuen bat esan zuen

    Niretzat prozesadore hau asko deitzen didan zerbait da. Ordenagailuko txakur lodi batzuek erosi dezakegun ordenagailua egitea baino ez da geratzen.

    ARMaren arazoa zirrara egiten didan zerbait da, dagoeneko ikusi zenuen Huawei-rekin zer gertatu zen zigorrekin. Argi daukat nire RISC-V-entzat irtenbide askoz hobea dela maila guztietan. Momentuz Huawei-k dagoeneko begirada jarri dio eta agian etorkizunean mikro honekin ekipamenduak izango dituzte. Bada, ziur aski enpresa gehiago egongo dira beraiek onartzen dutenak eta niretzat hori litzateke ideala eta batez ere distribuzioek onartzen dutena eta ez bakarrik ARMa gehienekin gertatzen den moduan.

    1.    Gregory ros esan zuen

      + 10