بنیاد RISC-V در مورد تأیید عملکرد میکروکرنل در سیستم هایی با معماری مجموعه دستورالعمل RISC-V. تأیید به پایین می آید قابلیت اطمینان عملیات seL4، که نشان دهنده انطباق کامل با مشخصات مشخص شده در زبان رسمی است. اثبات قابلیت اطمینان seL4 در سیستم‌های ماموریت حیاتی مبتنی بر پردازنده‌های RISC-V RV64 که به سطح بالایی از قابلیت اطمینان نیاز دارند و عدم وجود خرابی را تضمین می‌کنند. توسعه دهندگان نرم افزارهایی که در بالای هسته seL4 اجرا می شوند، می توانند کاملاً مطمئن باشند که اگر در یک قسمت از سیستم خرابی وجود داشته باشد، این خرابی به بقیه سیستم و به ویژه قسمت های مهم آن سرایت نمی کند.
میکروکرنل seL4 در ابتدا برای پردازنده های ARM 32 بیتی و بعداً برای پردازنده های 64 بیتی x86 تأیید شد. خاطرنشان می شود که ترکیب معماری سخت افزاری باز RISC-V با میکروکرنل باز 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 وجود داشته است.
منبع: opennet.ru