Fondasyon RISC-V sou verifye operasyon mikrokernel la sou sistèm ak achitekti seri enstriksyon RISC-V. Verifikasyon vini desann nan fyab nan operasyon seL4, ki endike konfòmite konplè ak espesifikasyon yo espesifye nan langaj fòmèl la. Prèv fyab seL4 nan sistèm misyon kritik ki baze sou processeurs RISC-V RV64 ki mande pou yon nivo ogmante fyab ak garanti absans echèk. Devlopè nan lojisyèl ki kouri sou tèt nwayo seL4 la ka konplètman gen konfyans ke si gen yon echèk nan yon pati nan sistèm nan, echèk sa a pa pral gaye nan rès la nan sistèm nan ak, an patikilye, pati kritik li yo.
Microkernel seL4 te okòmansman verifye pou processeurs ARM 32-bit, epi pita pou processeur x64 86-bit. Li te note ke konbinezon an nan achitekti pyès ki nan konpitè louvri RISC-V ak microkernel seL4 louvri pral reyalize yon nouvo nivo sekirite, depi konpozan pyès ki nan konpitè yo kapab tou konplètman verifye nan lavni an, ki se enposib reyalize pou achitekti pyès ki nan konpitè propriétaires.
Lè verifye seL4, li sipoze ke ekipman an ap travay jan sa di ak spesifikasyon la konplètman dekri konpòtman an nan sistèm nan, men an reyalite ekipman an pa gratis nan erè, ki se klèman demontre pa regilyèman émergentes pwoblèm nan mekanis nan ekzekisyon spéculatif nan. enstriksyon yo. Louvri platfòm pyès ki nan konpitè yo fè li pi fasil pou entegre chanjman ki gen rapò ak sekirite - pou egzanp, bloke tout posib koule bò-chanèl, kote li pi efikas debarase m de pwoblèm nan nan pyès ki nan konpitè pase pou eseye jwenn solisyon nan lojisyèl.
Sonje byen, achitekti seL4 la deplase pati pou jere resous nwayo nan espas itilizatè yo epi aplike menm mwayen kontwòl aksè pou resous sa yo tankou pou resous itilizatè yo. Mikrokernel la pa bay abstraksyon wo nivo pare pou jere fichye, pwosesis, koneksyon rezo, ak lòt bagay; olye de sa, li bay sèlman mekanis minim pou kontwole aksè nan espas adrès fizik, entèwonp, ak resous processeur. Abstraksyon wo nivo ak chofè pou kominike avèk pyès ki nan konpitè yo aplike separeman sou tèt mikrokernel la nan fòm travay nan nivo itilizatè. Aksè travay sa yo nan resous ki disponib nan mikrokernel la òganize atravè definisyon règ yo.
RISC-V bay yon sistèm ansèyman machin ouvè ak fleksib ki pèmèt mikwo-pwosesè yo dwe bati pou aplikasyon abitrè san yo pa egzije redevans oswa fisèl tache pou itilize. RISC-V pèmèt ou kreye SoCs ak processeurs konplètman louvri. Kounye a ki baze sou spesifikasyon RISC-V pa diferan konpayi ak kominote anba plizyè lisans gratis (BSD, MIT, Apache 2.0) plizyè douzèn varyant nan nwayo mikwoprosesè, SoCs ak deja pwodwi chips. Sipò RISC-V te prezan depi degaje Glibc 2.27, binutils 2.30, gcc 7, ak Linux Kernel 4.15.
Sous: opennet.ru