اولین هایپروایزر ابری که ریاضی اثباتش کرده
خلاصهٔ کاملتر
تو این پست از تیم Automated Reasoning آمازون اومده که همزمان با عرضهٔ اینستنسهای جدید M9g و M9gd روی Graviton5، یه مؤلفهٔ امنیتی تازه به اسم Nitro Isolation Engine هم فعال شده. این مؤلفه بخشی از Nitro Hypervisor هست و تنها کارش اینه که ماشینهای مجازی (VM) رو از هم جدا و ایزوله نگه داره. نکتهٔ مهم اینه که درستی رفتارش بهطور ریاضی اثبات شده.
نویسندهها توضیح میدن که این کار با یه «separation kernel» ممکن شده؛ ایدهای که جان رشبی سال ۱۹۸۱ مطرح کرد. منطقش جدا کردن سیاست از مکانیزم هست: این هسته تصمیم نمیگیره چی ایزوله بشه یا منابع چطور تقسیم بشن، فقط روی اعمال ایزولهسازی تمرکز میکنه. به گفتهٔ نویسندهها همین تمرکز باعث میشه بهمراتب سادهتر از یه هستهٔ کامل سیستمعامل باشه و بشه وارسیاش کرد. خود Nitro Hypervisor هنوز سیاستها رو مدیریت میکنه ولی حالا کمامتیاز شده و برای هر عملیاتی که به وضعیت مهمان دست میزنه باید از Isolation Engine اجازه بگیره.
برای اثبات، تیم از ابزار Isabelle/HOL استفاده کرده که گامهای استدلال رو از نظر منطقی ماشینی چک میکنه. حاصل کار ۳۳۰ هزار خط ریاضی ماشینچکشدهست که از نظر مقیاس با پروژهٔ مشهور seL4 قابل مقایسهست؛ با این تفاوت که این یکی روی سختافزار تولیدی و بهصورت همیشهفعال برای کاربرهای Graviton5 اجرا میشه.
قضیهها چهار نوع ویژگی رو پوشش میدن: محرمانگی و یکپارچگی (مثلاً حافظهٔ مهمان قبل از استفادهٔ دوباره همیشه پاکسازی میشه)، درستی عملکردی، نبود خطاهای زمان اجرا و ایمنی حافظه. سه مورد آخر با هم بهعنوان وارسی عملکردی هندل میشن و محرمانگی و یکپارچگی جدا، چون تکنیک اثباتشون فرق داره.
برای وارسی عملکردی، تیم یه زیرمجموعهٔ محدود از زبان Rust به اسم μRust تعریف کرده که ویژگیهای پیچیدهای مثل trait و dynamic dispatch توش حذف شده تا استدلال روش راحتتر باشه. مشخصات با Separation Logic نوشته میشن و اثبات با حساب «ضعیفترین پیششرط» (weakest-precondition) انجام میشه. همهٔ این زیرساخت بخشی از کتابخانهٔ AutoCorrode هست که آمازون سال ۲۰۲۵ اوپنسورسش کرده.
برای محرمانگی، ایدهٔ کلیدی noninterference یا «حفظ تمایزناپذیری» هست. منطقش اینه: اگه دو حالت از دید یه ناظر قبل از یه گام تفکیکناپذیر باشن، باید بعدش هم تفکیکناپذیر بمونن؛ چون اگه ناظر بتونه بعد از یه گام دو حالت رو از هم تشخیص بده، یعنی اطلاعات محرمانهای نشت کرده. نویسندهها میگن این تازه شروع کاره و قراره جنبههای دیگه مثل تست انطباق و استدلال دربارهٔ کد همزمان رو هم تو پستهای بعدی به اشتراک بذارن.
نکات کلیدی:
- Nitro Isolation Engine اولین هایپروایزر ابری تجاریه که بهطور رسمی و ریاضی وارسی شده
- اثبات با Isabelle/HOL انجام شده و ۳۳۰ هزار خط ریاضی ماشینچکشده داره
- روی پردازندههای Graviton5 (اینستنسهای M9g/M9gd) همیشه فعاله
- چهار ویژگی پوشش داده شده: محرمانگی، یکپارچگی، درستی عملکردی، نبود خطای زمان اجرا و ایمنی حافظه
- زیرساخت اثبات (μRust و AutoCorrode) اوپنسورس شده
