seL4 microkernel رياضياتي طور تي RISC-V فن تعمير لاءِ تصديق ٿيل آهي

RISC-V فائونڊيشن ٻڌايو microkernel جي آپريشن جي تصديق جي باري ۾ seL4 سسٽم تي RISC-V هدايتون سيٽ آرڪيٽيڪچر سان. تصديق هيٺ اچي ٿي رياضياتي ثبوت seL4 آپريشن جي قابل اعتماد، جيڪا رسمي ٻولي ۾ بيان ڪيل وضاحتن سان مڪمل تعميل کي ظاهر ڪري ٿي. اعتبار جو ثبوت توهان کي استعمال ڪرڻ جي اجازت ڏئي ٿو seL4 مشن-نازڪ سسٽم ۾ RISC-V RV64 پروسيسرز جي بنياد تي جيڪي اعتماد جي وڌايل سطح جي ضرورت هونديون آهن ۽ ناڪامين جي غير موجودگي جي ضمانت ڏين ٿيون. سافٽ ويئر جي ڊولپرز جيڪي seL4 ڪرنل جي چوٽي تي ھلندا آھن مڪمل طور تي يقين ڪري سگھن ٿا ته جيڪڏھن سسٽم جي ھڪڙي حصي ۾ ناڪامي آھي، اھو ناڪامي باقي سسٽم تائين پکڙيل نه آھي ۽ خاص طور تي، ان جي نازڪ حصن ۾.

seL4 microkernel شروعاتي طور تي 32-bit ARM پروسيسرز جي تصديق ڪئي وئي، ۽ بعد ۾ 64-bit x86 پروسيسرز لاء. اهو نوٽ ڪيو ويو آهي ته اوپن RISC-V هارڊويئر آرڪيٽيڪچر جو ميلاپ اوپن seL4 مائڪرو ڪنيل سان سيڪيورٽي جي نئين سطح کي حاصل ڪندو، ڇاڪاڻ ته هارڊويئر اجزاء پڻ مستقبل ۾ مڪمل طور تي تصديق ڪري سگھجن ٿيون، جيڪو مالڪي هارڊويئر آرڪيٽيڪچرز لاءِ حاصل ڪرڻ ناممڪن آهي.

جڏهن seL4 جي تصديق ڪندي، اهو فرض ڪيو ويو آهي ته سامان ڪم ڪري ٿو جيئن بيان ڪيو ويو آهي ۽ وضاحت مڪمل طور تي سسٽم جي رويي کي بيان ڪري ٿو، پر حقيقت ۾ اهو سامان غلطين کان خالي ناهي، جيڪو واضح طور تي واضح طور تي ظاهر ڪيو ويو آهي ته قياس آرائي جي عمل جي ميڪانيزم ۾ باقاعده طور تي پيدا ٿيندڙ مسئلا. هدايتون. اوپن هارڊويئر پليٽ فارمن کي سيڪيورٽي سان لاڳاپيل تبديلين کي ضم ڪرڻ آسان بڻائي ٿو - مثال طور، سڀني ممڪن سائڊ چينل ليڪس کي بلاڪ ڪرڻ، جتي سافٽ ويئر ۾ ڪم ڪار ڳولڻ جي ڪوشش ڪرڻ جي ڀيٽ ۾ هارڊويئر ۾ مسئلي کان نجات حاصل ڪرڻ وڌيڪ ڪارائتو آهي.

ياد رهي ته seL4 فن تعمير قابل ذڪر ڪنيل وسيلن کي يوزر اسپيس ۾ منظم ڪرڻ لاءِ حصن کي منتقل ڪرڻ ۽ ساڳئي رسائي ڪنٽرول کي لاڳو ڪرڻ جو مطلب اهڙن وسيلن لاءِ جيئن صارف وسيلن لاءِ. microkernel فائلن، پروسيس، نيٽ ورڪ ڪنيڪشن، وغيره کي منظم ڪرڻ لاء تيار ڪيل اعلي سطحي خلاصيون مهيا نه ڪندو آهي؛ ان جي بدران، اهو صرف فزيڪل ايڊريس اسپيس، مداخلت، ۽ پروسيسر وسيلن تائين رسائي کي ڪنٽرول ڪرڻ لاء صرف گهٽ ميکانيزم مهيا ڪري ٿو. هارڊويئر سان لهه وچڙ لاءِ اعليٰ سطح جا تجزيا ۽ ڊرائيور الڳ الڳ لاڳو ڪيا ويا آهن مائڪرو ڪنيل جي مٿان صارف جي سطح جي ڪمن جي صورت ۾. اهڙن ڪمن جي رسائي مائڪڪررنل وٽ موجود وسيلن تائين قاعدن جي تعريف ذريعي ترتيب ڏنل آهي.

RISC-V هڪ کليل ۽ لچڪدار مشين جي هدايتن جو نظام مهيا ڪري ٿو جيڪو مائڪرو پروسيسرز کي اجازت ڏئي ٿو بنا ڪنهن ارادي جي ايپليڪيشنن لاءِ تعمير ڪرڻ جي بغير رائلٽيز يا استعمال سان ڳنڍيل تارن جي. RISC-V توهان کي مڪمل طور تي کليل SoCs ۽ پروسيسرز ٺاهڻ جي اجازت ڏئي ٿو. في الحال RISC-V وضاحتن جي بنياد تي مختلف ڪمپنين ۽ برادرين پاران مختلف مفت لائسنس (BSD، MIT، Apache 2.0) ترقي ڪري ٿو مائڪرو پروسيسر ڪور، SoCs ۽ اڳ ۾ ئي تيار ڪيل چپس جا ڪيترائي درجن ورجن. RISC-V سپورٽ Glibc 2.27، binutils 2.30، gcc 7، ۽ Linux kernel 4.15 جي رليز کان وٺي موجود آهي.

جو ذريعو: opennet.ru

تبصرو شامل ڪريو