موتور «ایزولیشن» رسمی‌ً تأییدشدهٔ EC2، تضمین ریاضیاتی جداسازی ماشین‌های مجازی را فراهم می‌کند.

اصل ماجرا

AWS اعلام کرد که نمونه‌های M9g و M9gd مبتنی بر پردازنده Graviton5، اولین سرورهای EC2 با Nitro Isolation Engine هستند؛ این مؤلفه به‌صورت رسمی با Isabelle/HOL اثبات شده که ایزوله‌سازی بین ماشین‌های مجازی را به‌درستی اعمال می‌کند. این اولین هیپرویزور تجاری است که به‌صورت ریاضیاتی تأیید شده و بر پایه Rust و μRust ساخته شده است.

متن کامل ترجمه‌شده

امروز ما اعلام کردیم که نسخه های جدید M9g و M9gd از Cloud Compute Elastic (EC2) از Amazon Web Services (AWS) ، اولین نوع نسخه ای که توسط Graviton5 ، آخرین نسل CPU عمده ما استفاده می شود ، در دسترس هستند. Graviton5 تعداد هسته های نسل قبلی را از 96 به 192 دو برابر می کند. آنها همچنین اولین نمونه هایی هستند که از Nitro Isolation Engine استفاده می کنند که بخشی از Nitro Hypervisor است که تنها وظیفه آن است که دستگاه های مجازی (VMs) را از یکدیگر جدا کند. در این پست، ما توضیح می دهیم که چگونه از Isabelle / HOL (Logic Higher Order) Proof Assistant استفاده کردیم - نرم افزار که به طور مکانیسم اقدامات منطقی برای اطمینان با قوانین منطقی را بررسی می کند - نشان می دهد که Nitro Isolation Engine به طور درست رفتار می کند ومدل و اثبات Isabelle/HOL ما شامل 330،000 خط از ریاضیات مورد بررسی ماشین است. این در مقیاس قابل مقایسه با seL4 است، پروژه مهمی که برای اولین بار نشان داد که تایید سیستم عامل واقعی قابل اجرا است و یک الهام برای کار خود ما بود. با این حال، بر خلاف seL4, Nitro Isolation Engine برای محیط های تجاری ابر و کشتی ها بر روی نرم افزار تولید به عنوان یک ویژگی همیشه در حال حاضر برای کاربران Graviton5 طراحی شده است. سخنرانی ما در کنفرانس re:Invent 2025 آمازون، روش رسمی ما را معرفی می کند. این پست وبلاگ یک نظرسنجی غیر رسمی از جنبه های اصلی کار تایید رسمی ما را ارائه می دهد و چگونه آنها را با هم ترکیب می کنند. چه چیزی یک هسته جداگانه است؟ جان راشبی در سال 1981 به اصطلاح “نموده جداگانه” اشاره کرد تا بخشی ازیک هسته جداگانه تصمیم نمی گیرد که چه چیزی را جدا کند، چگونه منابع را اختصاص دهد، یا چه VM ها را برنامه ریزی کند: این تصمیمات در جای دیگری گرفته می شود. به جای آن، تنها بر اجرای جداگانه تمرکز می کند، و این شفافیت هدف باعث می شود که kernels جداگانه را بسیار ساده تر از kernels کامل OS اجرا شود. از زمان معرفی آن در سال 2017، Nitro Hypervisor مسئول اجرای جداگانه در EC2 است، اما همچنین با منطق کسب و کار، رانندگان دستگاه، و ویژگی های خاص AWS کار می کند. این پیچیدگی باعث می شود ثابت کردن درست بودن بسیار دشوارتر است. علاوه بر این، Nitro Hypervisor برای تایید از ابتدا طراحی نشده است. جداگانه شدن منطق جداگانه های جداگانه در یک عنصر حداقل، Nitro Isolation Engine، آن را به اندازه کافی کوچک برای بررسی و بررسی، به مشتNitro Hypervisor هنوز هم با سیاست ها - ایجاد VM، تخصیص منابع، مهاجرت، برنامه ریزی - کار می کند، اما در حال حاضر منحصر به فرد است و باید از Nitro Isolation Engine درخواست کند که هر عملیات را در حالت مهمان انجام دهد. Nitro Isolation Engine هر درخواست را قبل از انجام عمل بررسی می کند. مشخصات و اثبات دو بخش کلیدی کار ما مشخصات و اثبات هستند. مشخصات رسمی به طور دقیق رفتار سیستم را ضبط می کنند و اثبات می کنند که اجرای آن مطابق با این مشخصات است. نظریه های ما در مورد Nitro Isolation Engine چهار نوع خصوصیات را بررسی می کند: - حفظ حریم خصوصی و integrity. تنها جریان اطلاعات مجاز می تواند رخ دهد. به عنوان مثال، توزیع حافظه مهمان همیشه قبل از استفاده مجدد پاک می شود. - درست بودن عملکرد.- امنیت حافظه. هیچ مشکلی مانند سوخت های برجسته و نمره های نشانگر NULL وجود ندارد. در عملی، ما سه ویژگی آخر را به طور جمعی به عنوان یک نتیجه تصدیق عملکردی، با حفظ حریم خصوصی و integrity به صورت جداگانه مورد بررسی قرار می دهیم، زیرا ما تکنیک های شواهدی مختلفی برای هر یک از آنها استفاده می کنیم. تصدیق عملکردی برای تصدیق عملکردی، قسمت های کلیدی این است که یک زیر مجموعه هسته ای از زبان Rust نامیده می شود μRust (“micro Rust”)؛ یک زبان مشخصات بیانگر با استفاده از منطق جداگانه برای ضبط دقیق مشخصات؛ و یک تکنیک تصدیق، ضعیف ترین محاسبه پیش شرط، با اتوماتیک شواهد شخصی برای ثابت کردن یک برنامه درست با توجه به مشخصات آن. هر یک از اینها بخشی از یک زیرسادر جزئیات بیشتر، μRust یک زیر مجموعه محدود از زبان برنامه نویسی Rust است که به اندازه کافی بیانگر برای نوشتن Nitro Isolation Engine است اما قابل تفسیر رسمی است زیرا ما به طور عمدی ویژگی های پیشرفته Rust، مانند ویژگی ها و فرستندهای دموکراتیک را خارج کردیم. سمیاتیک رسمی μRust به عنوان یک انطباق فرش در Isabelle/HOL تعریف می شود، به این معنی که معنای μRust به لحاظ منطق درجه بالا، زبان میزبان Isabelle/HOL تعریف می شود. مشخصات برای یک برنامه μRust به عنوان یک قرارداد با پیش و پس شرایط تعریف می شود، که ادعاهای مربوط به وضعیت سیستم قبل و بعد از اجرا برنامه است. قرارداد های ما “تصاویر کامل” را مشخص می کنند، که به این معنی است که در تمام شرایطی که شرایط پیش راضی هستند، برنامهمشخصات ما با استفاده از منطق جدا شدن نوشته شده اند، یک منطق طراحی شده است که در مورد برنامه های دستکاری نشانگر سطح پایین منطق می کند. با وجود ساده بودن نسبتا از هسته های جدا شدن، با تصدیق دستگاه Nitro Isolation Engine ما هنوز هم در کنار آنچه ممکن است با تصدیق رسمی کار می کنیم، و هر دو مشخصات و شواهد ما بسیار بزرگ می شوند. به عنوان مثال، مشخصات زیر تصدیق می کند که چه اتفاقی می افتد هنگامی که یک CPU مجازی مهمان اجرا می کند سعی می کند خود را فعال کند ( یک درخواست اشتباه): در حالی که مشخصات بالا پیچیده است، آنچه را که آن را تصدیق می کند به صورت بصیرت ساده است: در این شرایط، Nitro Isolation Engine می بیند که، برای عمل به عنوان دعوت کننده، CPU مجازی باید در حال حاضر فعال شود و بنابراین یک کد اشتباه تعیین شده راپیچیدگی در مشخصات نشان دهنده عمق مدل سازی ما و این واقعیت است که تعدادی از بررسی های اشتباه دیگر باید برای ما انجام شده باشد تا در این نقطه در اجرای Nitro Isolation Engine برسیم. برای ثابت کردن یک برنامه μRust در مورد مشخصات آن درست است، ما از یک محاسبه استاندارد ضعیف ترین شرایط استفاده می کنیم. محاسبه ضعیف ترین شرایط یک راه سیستماتیک برای شناسایی ضعیف ترین محدودیت است که می تواند اطمینان حاصل کند که وضعیت یک برنامه پس از یک عملیات خاص خارج از برخی از شرایط مشخص نشده است. به عنوان مثال، ضعیف ترین شرایطی از بیان “x + y” وضعیتی است که در آن ارزش های x و y نمی تواند اضافه شود.حریم خصوصی و حریم خصوصی برای حریم خصوصی و حریم خصوصی، قسمت کلیدی اول یک مشخصات سطح بالا است که رفتار موتور تخلیه نیترو را به عنوان یک رابطه انتقال، که در آن هر مرحله “در سطح بالا” از سیستم (به عنوان مثال، hypercall) یک انتقال اتمی است، جمع آوری می کند. این مشخصات به سختی با مشخصات منطقی جدا شدن دقیق تر استفاده می شود در نتایج تایید عملکرد ما، که از یک ایده شواهد دیگری به نام تمیز استفاده می کند. قسمت کلیدی دوم ایده عدم تداخل است. عدم تداخل ایده حفظ عدم تفاوتی است که ما از آن استفاده می کنیم تا حریم خصوصی و حریم خصوصی به طور ریاضی دقیق. ایده این است که اگر دو وضعیت قابل تفاوتی برای یک تماشاگر قبل از یک مرحله، آنها باید غیر قابل تفاوتی بعد از آن باقی بمانند. دلیل عاطفی است کهدرک چرا حفظ عدم تخصیص ضمانت حفظ حریم خصوصی پیچیده است. در نظر بگیرید دو دستگاه ساده، A و B، هر یک با یک ثبت عمومی و یک ثبت خصوصی. یک تماشاگر آنها را غیر قابل تخصیص می داند اگر ثبت های عمومی آنها یکسان است: ثبت خصوصی پنهان است. در گرافیک زیر، A و B غیر قابل تخصیص هستند: در حال حاضر در نظر بگیرید که چه اتفاقی می افتد اگر ما یک برنامه را اجرا کنیم که شاخه ها را در ثبت خصوصی برای اختصاص 1 به ثبت عمومی. دستگاه های تولید شده A’ و B’ اکنون ثبت های عمومی مختلف دارند - آنها قابل تخصیص هستند! یک تماشاگر هوشمند می تواند این را برای از دست دادن ارزش های خصوصی اصلی استفاده کند، و این عدم حفظ غیر قابل تخصیص به جریان اطلاعات غیرقانونی به تماشاگران مطابقت دارد. و بیشتر برای رسیدن ما امیدواریمبسیاری از جنبه های دیگر در کار ما وجود دارد، مانند تست سازگاری و چگونگی مقابله با استدلالات در مورد کد همزمان، که ما هیجان زده ایم که در پست های آینده به اشتراک بگذاریم.

چرا مهمه؟

این گام، تضمین امنیت و پایداری زیرساخت‌های ابری را به سطحی می‌برد که قبلاً فقط در پروژه‌های تحقیقاتی ممکن بود.

به درد کی می‌خوره؟

security_professionals, devops, tech_leads, developers

تو عمل چی کار کنیم؟

توسعه‌دهندگان می‌توانند با اطمینان بیشتری از ایزوله‌سازی VMها استفاده کنند و تمرکز خود را بر ویژگی‌های تجاری بگذارند، نه روی باگ‌های امنیتی زیرساخت.

نظر Blue IT News

تأیید ریاضی‌محور ایزوله‌سازی در ابرهای عمومی، نقطه عطفی برای اعتماد به زیرساخت‌های ابری است.

<div class=“disclosure”> این صفحه ترجمه و تفسیر کاملی از گزارش اصلی Amazon است که توسط تیم تحریریه بلو آی تی نیوز به فارسی ترجمه و تحلیل شده. برای مشاهده نسخه اصلی، به منبع مراجعه کنید. </div>