د seL4 مایکروکرنل د RISC-V معمارۍ لپاره په ریاضي ډول تایید شوی

RISC-V بنسټ راپور شوی د مایکروکرنل د عملیاتو تصدیق کولو په اړه seL4 په سیسټمونو کې د RISC-V لارښوونې ترتیب شوي جوړښت سره. تایید ته ښکته راځي د ریاضي ثبوت د seL4 عملیات اعتبار، کوم چې په رسمي ژبه کې مشخص شوي مشخصاتو سره بشپړ اطاعت په ګوته کوي. د اعتبار ثبوت تاسو ته د کارولو اجازه درکوي seL4 د ماموریت مهم سیسټمونو کې چې د RISC-V RV64 پروسیسرونو پراساس دی چې د اعتبار لوړې کچې ته اړتیا لري او د ناکامۍ نشتوالي تضمین کوي. د سافټویر جوړونکي چې د seL4 کرنل په پورتنۍ برخه کې روان دي په بشپړ ډول ډاډه کیدی شي چې که چیرې د سیسټم په یوه برخه کې ناکامي شتون ولري ، نو دا ناکامي به پاتې سیسټم ته نه خپریږي او په ځانګړي توګه د هغې مهمې برخې.

د seL4 مایکروکرنل په پیل کې د 32-bit ARM پروسیسرونو لپاره تصدیق شوی و، او وروسته د 64-bit x86 پروسیسرونو لپاره. د یادونې وړ ده چې د خلاص RISC-V هارډویر جوړښت ترکیب د خلاص seL4 مایکروکرنل سره به د امنیت نوې کچه ترلاسه کړي ، ځکه چې د هارډویر اجزا هم په راتلونکي کې په بشپړ ډول تایید کیدی شي ، کوم چې د ملکیت هارډویر جوړښتونو لپاره ترلاسه کول ناممکن دي.

کله چې د seL4 تصدیق کول ، داسې انګیرل کیږي چې تجهیزات لکه څنګه چې ویل شوي کار کوي او توضیحات په بشپړ ډول د سیسټم چلند تشریح کوي ، مګر په حقیقت کې تجهیزات له غلطیو څخه پاک ندي ، کوم چې په روښانه ډول د قیاس اجرا کولو میکانیزم کې په منظم ډول رامینځته کېدونکو ستونزو لخوا څرګندیږي. لارښوونې د خلاص هارډویر پلیټ فارمونه د امنیت پورې اړوند بدلونونو ادغام کول اسانه کوي - د مثال په توګه ، د ټولو ممکنه اړخ چینل لیکونو بندول ، چیرې چې په سافټویر کې د کاري لارو موندلو هڅه کولو په پرتله په هارډویر کې له ستونزې څخه خلاصون خورا مؤثر دی.

په یاد ولرئ چې د seL4 جوړښت د پام وړ د کارن په ځای کې د کرنل سرچینو اداره کولو لپاره د برخو حرکت کول او د ورته لاسرسي کنټرول وسیله پلي کول د ورته سرچینو لپاره لکه د کارونکي سرچینو لپاره. مایکروکرنل د فایلونو، پروسو، شبکې اتصالاتو، او داسې نورو اداره کولو لپاره چمتو شوي لوړې کچې خلاصې نه وړاندې کوي؛ پرځای یې، دا د فزیکي پتې ځای، مداخلو، او پروسیسر سرچینو ته د لاسرسي کنټرول لپاره یوازې لږترلږه میکانیزمونه وړاندې کوي. د هارډویر سره د تعامل لپاره د لوړې کچې خلاصون او ډرایورونه د کارونکي کچې دندو په شکل کې د مایکروکرنل په سر کې په جلا توګه پلي کیږي. مایکروکرنل ته موجود سرچینو ته د دې ډول دندو لاسرسی د قواعدو تعریف له لارې تنظیم شوی.

RISC-V یو خلاص او انعطاف منونکی ماشین لارښوونې سیسټم چمتو کوي چې مایکرو پروسیسرونو ته اجازه ورکوي چې د خپل سري غوښتنلیکونو لپاره رامینځته شي پرته لدې چې د کارولو لپاره راجع کیدو یا تارونو ته اړتیا ولري. RISC-V تاسو ته اجازه درکوي په بشپړ ډول خلاص SoCs او پروسیسرونه رامینځته کړئ. اوس مهال د مختلف شرکتونو او ټولنو لخوا د مختلف وړیا جوازونو لاندې د RISC-V توضیحاتو پراساس (BSD, MIT, Apache 2.0) وده کوي د مایکرو پروسیسر کورونو څو درجن ډولونه ، SoCs او دمخه تولید شوي چپس. د RISC-V ملاتړ د Glibc 2.27، binutils 2.30، gcc 7، او د لینکس کرنل 4.15 له خپریدو راهیسې شتون لري.

سرچینه: opennet.ru

Add a comment