فيرف (نظام التشغيل)

📅 آخر تحديث: ٣١ يوليو ٢٠٢٦
✍️ نُشر في: ٣١ يوليو ٢٠٢٦
الموسوعة الحرة

فيرف هو نظام تشغيل بحثي طورته شركة مايكروسوفت للأبحاث . تم التحقق من سلامة أنواع البيانات وسلامة الذاكرة في فيرف بشكل شامل .

نظراً لتعقيدها، لطالما كان التحقق من خصائص أنظمة التشغيل هدفاً بالغ الأهمية في مجال التحقق من البرمجيات . عادةً ما تُكتب أنظمة التشغيل بلغات منخفضة المستوى، مثل لغة C ، التي لا توفر سوى ضمانات قليلة. اعتمد مشروع Singularity نهج كتابة نظام تشغيل بلغة C# ، وهي لغة آمنة من حيث النوع والذاكرة. من نقاط ضعف هذا النهج أن أنظمة التشغيل تحتاج بالضرورة إلى استدعاء شيفرة منخفضة المستوى، على سبيل المثال، لتحريك مؤشر المكدس. تعالج Verve هذه المشكلة بتقسيم نظام التشغيل إلى لغة تجميع مُدققة ، والتي يجب أن تكون منخفضة المستوى، وواجهة موثوقة لبقية نظام التشغيل، مكتوبة بلغة C#. يوجد معيار موثوق يضمن أن شيفرة التجميع منخفضة المستوى لا تُعدّل الذاكرة الديناميكية (heap)، وأن شيفرة C# عالية المستوى لا تُعدّل المكدسات.

يتألف نظام Verve من نواة صغيرة تعمل كطبقة تجريد برمجية بسيطة، ونواة تستخدم العناصر الأساسية التي توفرها النواة لعرض واجهة تقليدية للتطبيقات. جميع مكونات النظام، باستثناء النواة، مكتوبة بلغة C# المُدارة ، ويتم تجميعها بواسطة Bartok (الذي طُوّر في الأصل لمشروع Singularity ) إلى لغة تجميع مُنمّطة (TAL)، والتي يتم التحقق منها بواسطة مدقق TAL.

تُنفّذ النواة مُخصِّص ذاكرة وجمع بيانات مهملة، وتدعم تبديل المكدس، وتُدير معالجات المقاطعات. وهي مكتوبة بلغة BoogiePL، التي تُستخدم كمدخل لمُدقِّق Boogie الخاص بـ MSR ، والذي يُثبت صحة النواة باستخدام مُثبت النظريات الآلي Z3 Theorem Prover (SMT) . تعتمد النواة على النواة الرئيسية لتنفيذ الخيوط، والجدولة، والمزامنة، وتوفير معظم معالجات المقاطعات. على الرغم من أن النواة الرئيسية غير مُدقَّقة رسميًا، وبالتالي، على سبيل المثال، قد يتسبب خطأ في الجدولة في توقف النظام، إلا أنها لا تستطيع انتهاك سلامة النوع أو الذاكرة ، وبالتالي لا يُمكنها التسبب مباشرةً في سلوك غير مُعرَّف. إذا حاولت النواة الرئيسية إرسال طلبات غير صالحة إليها، فإن التحقق الرسمي يضمن أن النواة الرئيسية ستتعامل مع الموقف بطريقة مُتحكَّم بها .

تقتصر قاعدة الحوسبة الموثوقة (TCB) الخاصة بشركة Verve على: Boogie/Z3 للتحقق من صحة Nucleus؛ وBoogieASM لترجمتها إلى لغة التجميع x86؛ ومواصفات BoogiePL لكيفية عمل Nucleus؛ ومدقق TAL؛ والمجمع والرابط؛ ومحمل الإقلاع. والجدير بالذكر أن كلاً من مترجم/وقت تشغيل C# ومترجم Bartok ليسا جزءًا من قاعدة الحوسبة الموثوقة.

مراجع