انتشار Muen 1.0، یک میکروکرنل منبع باز برای ساختن سیستم های بسیار قابل اعتماد

پس از هشت سال توسعه، پروژه Muen 1.0 منتشر شد و هسته جداسازی را توسعه داد که عدم وجود خطا در کد منبع آن با استفاده از روش های ریاضی تأیید اعتبار رسمی تأیید شد. هسته برای معماری x86_64 در دسترس است و می‌تواند در سیستم‌های حیاتی ماموریتی که نیاز به سطح بالاتری از قابلیت اطمینان و تضمین عدم خرابی دارند، استفاده شود. کد منبع پروژه به زبان Ada و گویش قابل تایید آن SPARK 2014 نوشته شده است. کد تحت مجوز GPLv3 توزیع شده است.

هسته جداسازی یک میکروکرنل است که محیطی را برای اجرای اجزای جدا شده از یکدیگر فراهم می کند که تعامل آنها به شدت توسط قوانین داده شده تنظیم می شود. جداسازی مبتنی بر استفاده از افزونه های مجازی سازی Intel VT-x است و شامل مکانیسم های امنیتی برای مسدود کردن سازماندهی کانال های ارتباطی مخفی است. هسته پارتیشن‌بندی نسبت به سایر میکروکرنل‌ها مینیمال و ثابت‌تر است، که تعداد موقعیت‌هایی را که می‌توانند باعث خرابی شوند را کاهش می‌دهد.

کرنل در حالت ریشه VMX، شبیه به هایپروایزر، اجرا می‌شود، و همه اجزای دیگر در حالت غیر ریشه VMX، مشابه سیستم‌های مهمان اجرا می‌شوند. دسترسی به تجهیزات با استفاده از پسوندهای Intel VT-d DMA و نقشه‌برداری مجدد وقفه انجام می‌شود، که امکان پیاده‌سازی ایمن اتصال دستگاه‌های PCI به اجزای در حال اجرا تحت Muen را فراهم می‌کند.

انتشار Muen 1.0، یک میکروکرنل منبع باز برای ساختن سیستم های بسیار قابل اعتماد

قابلیت‌های Muen شامل پشتیبانی از سیستم‌های چند هسته‌ای، صفحات حافظه تودرتو (EPT، جدول‌های صفحه توسعه‌یافته)، MSI (وقفه‌های پیام‌رسانی پیام)، و جداول ویژگی صفحه حافظه (PAT، جدول ویژگی‌های صفحه) است. Muen همچنین یک زمان‌بندی دور ثابت بر اساس تایمر پیش‌گیرانه VMX اینتل، یک زمان اجرا فشرده که بر عملکرد تأثیری ندارد، یک سیستم حسابرسی خرابی، یک مکانیسم تخصیص منابع استاتیک مبتنی بر قانون، یک سیستم مدیریت رویداد و کانال‌های حافظه مشترک ارائه می‌کند. ارتباط در اجزای در حال اجرا

از اجزای در حال اجرا با کد ماشین 64 بیتی، ماشین های مجازی 32 یا 64 بیتی، برنامه های کاربردی 64 بیتی در زبان های Ada و SPARK 2014، ماشین های مجازی لینوکس و "unikernels" مستقل مبتنی بر MirageOS در بالای Muen پشتیبانی می کند.

نوآوری های اصلی ارائه شده در انتشار Muen 1.0:

  • اسنادی با مشخصات هسته (دستگاه و معماری)، سیستم (خط مشی های سیستم، Tau0 و جعبه ابزار) و اجزا منتشر شده است که تمام جنبه های پروژه را مستند می کند.
  • جعبه ابزار Tau0 (Muen System Composer) اضافه شده است که شامل مجموعه ای از مؤلفه های تأیید شده آماده برای نوشتن تصاویر سیستم و توسعه خدمات استانداردی است که در بالای Muen اجرا می شوند. اجزای ارائه شده شامل درایور AHCI (SATA)، مدیر دستگاه (DM)، بوت لودر، مدیر سیستم، ترمینال مجازی و غیره است.
  • درایور لینوکس muenblock (پیاده سازی یک دستگاه بلوکی که در بالای حافظه مشترک Muen اجرا می شود) برای استفاده از blockdev 2.0 API تبدیل شده است.
  • ابزارهای پیاده سازی شده برای مدیریت چرخه حیات اجزای بومی.
  • تصاویر سیستم به استفاده از SBS (Signed Block Stream) و CSL (Command Stream Loader) برای محافظت از یکپارچگی تبدیل شده اند.
  • یک درایور تأیید شده AHCI-DRV پیاده سازی شده است که به زبان SPARK 2014 نوشته شده است و به شما امکان می دهد درایوهایی را که از رابط ATA یا پارتیشن های دیسک جداگانه پشتیبانی می کنند به مؤلفه ها متصل کنید.
  • پشتیبانی unikernel بهبود یافته از پروژه های MirageOS و Solo5.
  • جعبه ابزار زبان Ada برای نسخه GNAT Community 2021 به روز شده است.
  • سیستم یکپارچه سازی پیوسته از شبیه ساز Bochs به محیط های تو در تو QEMU/KVM منتقل شده است.
  • تصاویر اجزای لینوکس از هسته لینوکس 5.4.66 استفاده می کنند.

منبع: opennet.ru

اضافه کردن نظر