Tá an micrea-eithne seL4 fíoraithe go matamaiticiúil don ailtireacht RISC-V

Fondúireacht RISC-V tuairiscithe maidir le hoibriú an mhicri-eithne a fhíorú seL4 ar chórais le hailtireacht tacair teagaisc RISC-V. Tagann an fíorú síos go cruthúnas matamaitice iontaofacht oibríocht seL4, a léiríonn comhlíonadh iomlán na sonraíochtaí atá sonraithe sa teanga fhoirmiúil. Cruthúnas ar iontaofacht ligeann duit úsáid a bhaint as seL4 i gcórais misean-criticiúla bunaithe ar phróiseálaithe RISC-V RV64 a éilíonn leibhéal méadaithe iontaofachta agus a ráthaíonn easpa teipeanna. Is féidir le forbróirí bogearraí a ritheann ar bharr na heithne seL4 a bheith go hiomlán muiníneach, má tá teip i gcuid amháin den chóras, nach leathfaidh an teip seo chuig an gcuid eile den chóras agus, go háirithe, na codanna ríthábhachtacha aige.

Fíoraíodh an microkernel seL4 ar dtús le haghaidh próiseálaithe ARM 32-giotán, agus níos déanaí le haghaidh próiseálaithe 64-giotán x86. Tugtar faoi deara go mbainfidh an meascán d'ailtireacht crua-earraí RISC-V oscailte leis an microkernel seL4 oscailte leibhéal nua slándála amach, toisc gur féidir na comhpháirteanna crua-earraí a fhíorú go hiomlán sa todhchaí, rud nach féidir a bhaint amach d'ailtireachtaí crua-earraí dílseánaigh.

Nuair a dhéantar seL4 a fhíorú, glactar leis go n-oibríonn an trealamh mar atá luaite agus go ndéanann an tsonraíocht cur síos iomlán ar iompar an chórais, ach i ndáiríre níl an trealamh saor ó earráidí, rud a léirítear go soiléir trí fhadhbanna a thagann chun cinn go rialta sa mheicníocht forghníomhaithe amhantrach. treoracha. Déanann ardáin chrua-earraí oscailte sé níos éasca athruithe a bhaineann le slándáil a chomhtháthú - mar shampla, chun gach sceitheadh ​​​​taobh-chainéil a d'fhéadfadh a bheith ann a bhlocáil, áit a bhfuil sé i bhfad níos éifeachtaí fáil réidh leis an bhfadhb i gcrua-earraí ná iarracht a dhéanamh teacht ar réitigh oibre i mbogearraí.

Thabhairt chun cuimhne go bhfuil an ailtireacht seL4 suntasach páirteanna gluaisteacha chun acmhainní eithne a bhainistiú isteach sa spás úsáideora agus na modhanna rialaithe rochtana céanna a chur i bhfeidhm ar acmhainní den sórt sin agus atá i gcás acmhainní úsáideoirí. Ní sholáthraíonn an micrea-eithne astarraingtí ardleibhéil réamhdhéanta chun comhaid, próisis, naisc líonra, agus a leithéidí a bhainistiú; ina ionad sin, ní sholáthraíonn sé ach meicníochtaí íosta chun rochtain ar spás seoltaí fisiceach, idirbhristeacha agus acmhainní próiseálaithe a rialú. Déantar astarraingtí ardleibhéil agus tiománaithe chun idirghníomhú le crua-earraí a chur i bhfeidhm ar leithligh ar bharr an mhicri-eithne i bhfoirm tascanna ar leibhéal an úsáideora. Eagraítear rochtain ar chúraimí den sórt sin ar na hacmhainní atá ar fáil don mhicri-eithne trí rialacha a shainiú.

Soláthraíonn RISC-V córas teagaisc meaisín oscailte agus solúbtha a ligeann do mhicreaphróiseálaithe a thógáil le haghaidh feidhmeanna treallach gan ríchíosanna nó teaghráin a cheangal le húsáid. Ligeann RISC-V duit SoCanna agus próiseálaithe atá go hiomlán oscailte a chruthú. Bunaithe faoi láthair ar shonraíocht RISC-V ag cuideachtaí agus pobail éagsúla faoi cheadúnais éagsúla saor in aisce (BSD, MIT, Apache 2.0) ag forbairt cúpla dosaen malairtí de chroíthe micriphróiseálaí, SoCanna agus sceallóga a táirgeadh cheana féin. Tá tacaíocht RISC-V i láthair ó scaoileadh Glib 2.27, binutils 2.30, gcc 7, agus an eithne Linux 4.15.

Foinse: oscailtenet.ru

Add a comment