RISC-V میکروکرنل seL4 را در پردازنده های RV64 خود تأیید کرد

بنیاد RISC-V اعلام کرد که تأیید کرده است نحوه کار میکرو هسته seL4 در سیستم های با معماری مجموعه دستورالعمل ها RISC-V که در آن روند تأیید به اثبات ریاضی قابلیت اطمینان seL4 کاهش می یابد ، که نشان دهنده انطباق کامل با مشخصات مشخص شده به زبان رسمی است.

آزمایش قابلیت اطمینان ، استفاده از seL4 را در سیستمهای مهم ماموریت مبتنی بر پردازنده های RISC-V امکان پذیر می سازد RV64، که به سطح بالاتری از قابلیت اطمینان نیاز دارد و عدم موفقیت را تضمین نمی کند.

توسعه دهندگان نرم افزاری که در بالای هسته seL4 در حال اجرا هستند می توانند کاملاً مطمئن باشند که در صورت خرابی در یک قسمت از سیستم ، این خرابی به بقیه سیستم و به ویژه در قسمت های مهم آن سرایت نمی کند. .

درباره seL4

معماری seL4 از بین بردن قطعات برای مدیریت منابع هسته در فضای کاربر قابل توجه است و برای چنین منابعی از روشهای کنترل دسترسی همانند منابع کاربر استفاده کنید.

میکرو هسته انتزاع در سطح بالا را فراهم نمی کند قبلاً آماده شده است تا پرونده ها ، پردازش ها ، اتصالات شبکه و غیره را مدیریت کنید ، اما در عوض حداقل مکانیسم هایی برای کنترل دسترسی به فضای آدرس فیزیکی فراهم می کند، وقفه ها و منابع پردازنده.

انتزاعات و كنترل كننده های سطح بالا برای تعامل با كامپیوتر بصورت جداگانه در بالای میکرو هسته در قالب وظایفی که در سطح کاربر انجام می شود ، اجرا می شوند.

دسترسی چنین وظایفی به منابع موجود در ریز هسته از طریق تعریف قوانین سازمان یافته است.

RISC-V یک سیستم باز و انعطاف پذیر ارائه می دهد از دستورالعمل های ماشین که اجازه می دهد تا ریزپردازنده برای برنامه های دلخواه ، بدون نیاز به کسر ایجاد کند و بدون تحمیل شرایط استفاده.

RISC-V به شما امکان می دهد SoC ها و پردازنده های کاملاً باز ایجاد کنید. در حال حاضر ، بر اساس مشخصات RISC-V ، چندین شرکت و جامعه تحت مجوزهای مختلف مختلف (BSD ، MIT ، Apache 2.0) در حال توسعه ده ها نوع هسته ریزپردازنده ، SoC و تراشه های تولید شده در حال حاضر هستند.

پشتیبانی RISC-V از زمان انتشار Glibc 2.27 ، binutils 2.30 ، gcc 7 و هسته لینوکس 4.15 وجود داشته است.

درباره آزمایش میکرو هسته seL4

در ابتدا ، میکرو هسته seL4 برای پردازنده های 32 بیتی ARM تأیید شد، و بعداً برای پردازنده های x86 64 بیتی.

مشاهده شده است که ترکیبی از ساختار سخت افزاری باز RISC-V با میکرو هسته باز است seL4 به سطح جدیدی از امنیت دست خواهد یافت، زیرا اجزای سخت افزاری آینده نیز می توانند به طور کامل تأیید شوند ، دستیابی به آن برای معماری های سخت افزاری اختصاصی غیرممکن است.

هنگام بررسی seL4 ، باید فرض کنیم که سخت افزار به درستی کار می کند (یعنی همانطور که مشخص شده است). فرض بر این است که در وهله اول مشخصات بدون ابهامی وجود دارد ، که در مورد همه سخت افزارها صدق نمی کند. 

اما حتی وقتی چنین مشخصاتی وجود داشته باشد و صوری باشد (یعنی در یک فرم گرایی ریاضی که از استدلال ریاضی در مورد ویژگی های آن پشتیبانی می کند) ، چگونه می توان فهمید که این رفتار سخت افزار را به تصویر می کشد؟ 

واقعیت این است که می توانیم کاملاً مطمئن باشیم که اینگونه نیست. سخت افزار با نرم افزار تفاوتی ندارد زیرا هر دو باگی هستند.

اما داشتن یک ISA باز مزایایی دارد که فراتر از داشتن حق امتیاز است. یکی این که امکان پیاده سازی سخت افزار منبع باز را فراهم می کند.

هنگام بررسی seL4 ، فرض بر این است که تجهیزات همانطور که نشان داده شده کار می کنند و مشخصات به طور کامل رفتار سیستم را توصیف می کند ، اما در واقع تجهیزات بدون خطا نیستند ، که به خوبی با مشکلاتی که به طور منظم در مکانیزم اجرای احتکار به وجود می آیند ، نشان داده می شود دستورالعمل ها.

سیستم عامل های سخت افزاری باز یکپارچه سازی تغییرات را ساده می کنند مربوط به امنیت ، به عنوان مثال ، برای مسدود کردن همه کانالهای نشتی احتمالی از طریق کانالهای شخص ثالث ، جایی که خلاص شدن از یک مشکل توسط سخت افزار بسیار کارآمدتر از تلاش برای یافتن راه حل توسط نرم افزار است.

سرانجام ، اگر می خواهید در مورد آن بیشتر بدانید ، می توانید با یادداشت موجود در آن مشورت کنید لینک زیر


محتوای مقاله به اصول ما پیوست اخلاق تحریریه. برای گزارش یک خطا کلیک کنید اینجا.

2 نظر ، نظر خود را بگذارید

نظر خود را بگذارید

نشانی ایمیل شما منتشر نخواهد شد. بخشهای موردنیاز علامتگذاری شدهاند با *

*

*

  1. مسئول داده ها: میگل آنخل گاتون
  2. هدف از داده ها: کنترل هرزنامه ، مدیریت نظرات.
  3. مشروعیت: رضایت شما
  4. ارتباط داده ها: داده ها به اشخاص ثالث منتقل نمی شوند مگر با تعهد قانونی.
  5. ذخیره سازی داده ها: پایگاه داده به میزبانی شبکه های Occentus (EU)
  6. حقوق: در هر زمان می توانید اطلاعات خود را محدود ، بازیابی و حذف کنید.

  1.   یکی از بعضی dijo

    از نظر من ، این پردازنده چیزی است که مرا زیاد صدا می کند. فقط برای برخی از سگهای چاق رایانه ای باقی مانده است که بتوانند رایانه ای بسازند که بتوانیم خریداری کنیم.

    مسئله ARM چیزی است که من را خسته می کند ، شما قبلاً دیدید که با تحریم ها چه اتفاقی برای هواوی افتاد. من واضح هستم که برای RISC-V من یک راه حل بسیار بهتر در تمام سطوح است. در حال حاضر هواوی نگاه خود را به آن معطوف کرده است و شاید در آینده آنها تجهیزاتی با این میکرو داشته باشند. در این صورت ، مطمئناً شرکت های بیشتری خواهند بود که آن را اتخاذ می کنند و برای من ایده آل ترین و بالاتر از همه حمایت کنندگان از آن هستند و نه تنها ARM همانطور که در بیشتر موارد اتفاق می افتد.

    1.    گریگوری روس dijo

      + 10